Please use this identifier to cite or link to this item:
|Title:||Inductively verifying invariant properties of parameterized systems|
|Authors:||Roychoudhury, A. |
|Source:||Roychoudhury, A.,Ramakrishnan, I.V. (2004). Inductively verifying invariant properties of parameterized systems. Automated Software Engineering 11 (2) : 101-139. ScholarBank@NUS Repository. https://doi.org/10.1023/B:AUSE.0000017740.35552.88|
|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|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 12, 2017
checked on Dec 8, 2017
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.