In this paper we report about the construction of a tool for conformance testing based
on Spin. The Spin tool has been adapted such it can derive test primitives from systems
described in Promela. These primitives support the on-the-fly conformance testing process.
Traditional derivation of tests from formal specifications suffers from the state-space explosion
problem and from complexity. Spin is one of the most advanced model checkers with
respect to handling large state spaces. This advantage of Spin has been used for the derivation
of test primitives from a Promela description.
To reduce the state space, we introduce the on-the-fly testing framework. Within this
framework the Primer is distinguished. This Primer derives test primitives from a model of
a system according to a well defined and complete testing theory. Algorithms are presented
which enable us to derive test primitives from a Promela description. These algorithms have
been implemented in the adapted version of the Spin tool which acts as the Primer in the
framework. As a result of this prototype study it is concluded that it is in principle possible
to derive these primitives automatically from Promela descriptions, and to perform testing.
|Publisher||Ecole Nationale Supérieure des Télécommunications|
|Workshop||Fourth Workshop on Automata Theoretic Verification with the Spin Model Checker|
|Period||2/11/98 → 2/11/98|
|Other||November 2, 1998|