Model checking support for CoreASM: model checking distributed abstract state machines using Spin

摘要

We present an approach to model checking Abstract State Machines, in the context of a larger project called CoreASM, which aims to provide a comprehensive and extensible tool environment for the design, validation, and verification of systems using the Abstract State Machine (ASM) formal methodology. Model checking is an automated and efficient formal verification technique that allows us to algorithmically prove properties about state transition systems. This thesis describes the design and implementation of model checking support for CoreASM, thereby enabling formal verification of ASMs. We specify extensions to CoreASM required to support model checking, as well as present a novel procedure for transforming CoreASM specifications into Promela models, which can be checked by the Spin model checker. We also present the results of applying our ASM model checking tool to several non-trivial software specifications.