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
Kirsten Winter
|