ASM2003 Gargantini, Angelo Riccobene, Elvinia Rinzivillo, Salvatore

Using Spin to Generate Tests from ASM Specifications

in ASM 2003 - Taormina, Italy, March 2003. Proceedings, LNCS 2589 (Eds. Boerger, Egon and Gargantini, Angelo and Riccobene, Elvinia) Springer Berlin Heidelberg, Lecture Notes in Computer Science, vol. 2589 (2003): 263-277 ISBN 978-3-540-00624-4

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] [url]

My sw links