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
