Using Spin to generate tests from ASM specifications

In this paper we introduce an algorithm to automatically encode an ASM specification in PROMELA, the language of the model checker Spin, and we present a method exploiting the counter example generation feature of Spin, to automatically generate from ASM specifications test sequences which accomplish a desired coverage. ASMs are used as test oracles to predict the expected outputs of units under test. A prototype tool that implements the proposed method is also presented. Experimental results in evaluating the method are reported. The experiments include test sequence generation, tests execution, code coverage measurement for a case study implemented in Java, and comparison with random tests generation. Benefits and limitations in using model checking are discussed.