2003 | OriginalPaper | Buchkapitel
Using Spin to Generate Tests from ASM Specifications
verfasst von : Angelo Gargantini, Elvinia Riccobene, Salvatore Rinzivillo
Erschienen in: Abstract State Machines 2003
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 exploitingthe 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 evaluatingthe 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 checkingare discussed.