Please use this identifier to cite or link to this item:
Title: Inductively verifying invariant properties of parameterized systems
Authors: Roychoudhury, A. 
Ramakrishnan, I.V.
Keywords: Concurrent systems
Induction proofs
Logic programming
Parameterized systems
Program transformations
Issue Date: 2004
Citation: Roychoudhury, A.,Ramakrishnan, I.V. (2004). Inductively verifying invariant properties of parameterized systems. Automated Software Engineering 11 (2) : 101-139. ScholarBank@NUS Repository.
Abstract: Verification of distributed algorithms can be naturally cast as verifying parameterized systems, the pa- rameter being the number of processes. In general, a parameterized concurrent system represents an infinite family (of finite state systems) parameterized by a recursively defined type such as chains, trees. It is therefore natural to verify parameterized systems by inducting over this type. However, construction of such proofs require combination of model checking with deductive capability. In this paper, we develop a logic program transformation based proof methodology which achieves this combination. One of our transformations (unfolding) represents a single resolution step. Thus model checking can be achieved by repeated application of unfolding. Other transformations (such as folding) represent deductive reasoning and help recognize the induction hypothesis in an inductive proof. Moreover the unfolding and folding transformations can be arbitrarily interleaved in a proof, resulting in a tight integration of decision procedures (such as model checking) with deductive verification. Based on this technique, we have designed and implemented an invariant prover for parameterized systems. Our proof technique is geared to automate nested induction proofs which do not involve strengthening of induction hypothesis. The prover has been used to automatically verify invariant properties of parameterized cache coherence protocols, including broadcast protocols and protocols with global conditions. Furthermore, we have employed the prover for automatic verification of mutual exclusion in the Java Meta-Locking Algorithm. Meta-Locking is a distributed algorithm developed recently by designers in Sun Microsystems for ensuring secure access of Java objects by an arbitrary number of Java threads.
Source Title: Automated Software Engineering
ISSN: 09288910
DOI: 10.1023/B:AUSE.0000017740.35552.88
Appears in Collections:Staff Publications

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


checked on Feb 21, 2020

Page view(s)

checked on Feb 19, 2020

Google ScholarTM



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