On-the-Fly Conformance Testing using Spin

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.