| Model checking of systems employing commutative functions (2005) | |||||||||||||||||
Abstract | |||||||||||||||||
| Abstract. The paper presents methods for model checking a class of possibly infinite state concurrent programs using various types of bi-simulation reductions. The proposed methods work for the class of programs in which the functions that update the variables are mutually commutative. A number of bi-simulation relations are presented for such systems. Explicit state model checking methods that employ on-the-fly reductions with respect to these bisimulations are given. Some of these methods have been implemented and have been used to verify some well known protocols that employ integer variables. Various applications of the methods and optimization techniques for special cases are also given in appendix. 1 Introduction Two of the bottlenecks that hinder wider applicability of model checking approach is the state explosion problem and its less effectiveness in handling infinite state systems. In this paper, we present an approach for model checking that works for certain classes of infinite state systems and that can also be used to contain the state explosion problem. One standard model checking method, employed often, is to construct the reachability graph of the given program and then check the correctness property against this graph. One way of reducing the size of the explored graph is to employ a reduction with respect to a bi-simulation relation U on the states of the reachability graph. Such a relation U is either known a priori through an implicit representation or has been computed by other means. | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||