Symbolic Bounded Model Checking of Abstract State Machines
Received:February 06, 2009  Revised:July 15, 2009  Download PDF
Margus Veanes,Nikolaj Bjφrner,Yuri Gurevich,Wolfram Schulte. Symbolic Bounded Model Checking of Abstract State Machines. International Journal of Software and Informatics, 2009,3(2):149~170
Hits: 4344
Download times: 3013
Abstract:Abstract State Machines (ASMs) allow modeling system behaviors at any desired level of abstraction, including a level with rich data types, such as sets, sequences, maps, and user-de.ned data types. The availability of high-level data types allow state elements to be represented both abstractly and faithfully at the same time. In this paper we look at symbolic analysis of ASMs. We consider ASMs over a .xed state background T that includes linear arithmetic, sets, tuples, and maps. For symbolic analysis, ASMs are translated into guarded update systems called model programs. We formulate the problem of bounded path exploration of model programs, or the problem of Bounded Model Program Checking (BMPC) as a satis.ability problem modulo T . Then we investigate the boundaries of decidable and undecidable cases for BMPC. In a general setting, BMPC is shown to be highly undecidable (Σ11 -complete); and even when restricting to .nite sets the problem remains re-hard (Σ01-hard). On the other hand, BMPC is shown to be decidable for a class of basic model programs that are common in practice. We use Satis.ability Modulo Theories (SMT) for solving BMPC; an instance of the BMPC problem is mapped to a formula, the formula is modulo T if and only if the corresponding BMPC problem instance has a solution. The recent SMT advances allow us to directly analyze speci.cations using sets and maps with specialized decision procedures for expressive fragments of these theories. Our approach is extensible; background theories need in fact only be partially solved by the SMT solver; we use simulation of ASMs to support additional theories that are beyond the scope of available decision procedures.
keywords:model programs  abstract state machines  satisability modulo theories  model checking
View Full Text  View/Add Comment  Download reader



Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号