Model Checking Abstract State Machines with Answer Set Programming

Issue title: This is a SPECIAL ISSUE ON ASM'05

Article type: Research Article

Authors: Tang, Calvin Kai Fan | Ternovska, Eugenia

Affiliations: School of Computing Science, Simon Fraser University, Burnaby, BC, Canada. E-mail: {ctang,ter}@cs.sfu.ca

Abstract: The quality of a computer system can be enhanced by modelling its design and verifying the correctness of the design before implementation is done. Abstract State Machines (ASMs) provide a mathematical framework for system modelling, while Model Checking is a technology for verification of system properties. Together, they form a powerful tool for checking systems. Bounded Model Checking (BMC) based on Answer Set Programming (ASP) is a competitive model checking approach due to its ability to compactly encode BMC problems. In this paper, we present a method of applying ASP to BMC of ASMs. Given an ASM and a temporal property, we show how to efficiently translate the BMC problem for the ASM into a problem of answer set computation. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.

Journal: Fundamenta Informaticae, vol. 77, no. 1-2, pp. 105-141, 2007