ASM-based testing: Coverage criteria and automatic test sequence generation
This paper tackles some aspect concerning the exploitation of Ab tract State Machine (ASM) for testing purposes. We define for ASM specifications a et of adequacy criteria measuring the coverage achieved by a test suite, and determining whether sufficient testing ha been performed. We introduce a method to automatically generate from ASM specification test sequences which accomplish a desired coverage. This method exploits the counter example generation of the model checker SMV. We use ASM a test oracle to predict the expected outputs of units under test.
testing test sequence generation formal methods abstract state machines