Abstract
In this paper we introduce an algorithm to automatically encode an ASM specification in PROMELA, the language of the model
checker Spin. Exploiting the counter example generation feature of Spin, we present a method 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 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.
[read the copyright and download the pdf file] [DOI]