Kirsten Winter:
Towards a Methodology for Model Checking ASM:
Lessons learned from the FLASH Case Study.
Abstract
Gurevich's Abstract State Machines (ASM) constitute a high-level specification language for a wide range of applications. The existing tool support for ASM was extended, in a previous work, to support computer-aided verification, in particular by model checking. In this paper we discuss the applicability of the model checking approach in general and describe the steps that are necessary to fit different kinds of ASM models for the model checking process. Along the example of the FLASH cache coherence protocol we show how model checking can support development and debugging of ASM models. We show the necessary refinement for the message passing behaviour in the protocol and give examples for errors found by model checking the resulting model. We conclude with some general remarks on the existing transformation algorithm.
compressed postscript
