Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/38939
Title: Unfold/fold transformations for automated verification of parameterized concurrent systems
Authors: Roychoudhury, A. 
Ramakrishnan, C.R.
Issue Date: 2004
Source: Roychoudhury, A.,Ramakrishnan, C.R. (2004). Unfold/fold transformations for automated verification of parameterized concurrent systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3049 : 261-290. ScholarBank@NUS Repository.
Abstract: Formal verification of reactive concurrent systems is important since many hardware and software components of our computing environment can be modeled as reactive concurrent systems. Algorithmic techniques for verifying concurrent systems such as model checking can be applied to finite state systems only. This chapter investigates the verification of a common class of infinite state systems, namely parameterized systems. Such systems are parameterized by the number of component processes, for example an n-process token ring for any n. Verifying the entire infinite family represented by a parameterized system lies beyond the reach of traditional model checking. On the other hand, deductive techniques to verify infinite state systems often require substantial user guidance. The goal of this work is to integrate algorithmic and deductive techniques for automating proofs of temporal properties of parameterized concurrent systems. Here, the parameterized system to be verified and the temporal property are encoded together as a logic program. The problem of verifying the temporal property is then reduced to the problem of determining equivalence of predicates in this logic program. These predicate equivalences are established by transforming the program such that the semantic equivalence of the predicates can be inferred from the structure of their clauses in the transformed program. For transforming the predicates, we use the well-established unfold/fold transformations of logic programs. Unfolding represents a step of resolution and can be used to evaluate the base case and the finite part of the induction step in an induction proof. Folding and other transformations represent deductive reasoning and can be used to recognize the induction hypothesis. Together these transformations are used to construct induction proofs of temporal properties. Strategies are developed to help guide the application of the transformation rules. The transformation rules and strategies have been implemented to yield an automatic and programmable first order theorem prover for parameterized systems. Case studies include multi-processor cache coherence protocols and the Java Meta-Locking protocol from Sun Microsystems. The program transformation based prover has been used to automatically prove various safety properties of these protocols. © Springer-Verlag 2004.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/38939
ISSN: 03029743
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

37
checked on Dec 8, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.