Abstract
We show how the problem of verifying parameterized systems can be reduced to the problem of determining the equivalence of goals in a logic program. We further show how goal equivalences can be established using induction-based proofs. Such proofs rely on a powerful new theory of logic program transformations (encompassing unfold, fold and goal replacement over multiple recursive clauses), can be highly automated, and are applicable to a variety of network topologies, including uni- and bi-directional chains, rings, and trees of processes. Unfold transformations in our system correspond to algorithmic model-checking steps, fold and goal replacement correspond to deductive steps, and all three types of transformations can be arbitrarily interleaved within a proof. Our framework thus provides a seamless integration of algorithmic and deductive verification at fine levels of granularity.
This work was partially supported by NSF grants CCR-9711386, CCR-9876242, CDA-9805735 and EIA-9705998.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and T. A. Henzinger, editors. Computer Aided Verification (CAV’ 96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996. Springer-Verlag. 186
K. Apt and D. Kozen. Limits for automatic verification of finite-state systems. Information Processing Letters, 15:307–309, 1986. 178
M. Browne, E. Clarke, and O. Grumberg. Reasoning about networks with many identical finite-state processes. Information and Computation, 81(1):13–31, 1989. 174
S. Basu, S.A. Smolka, and O.R. Ward. Model checking the Java meta-locking algorithm. In IEEE International Conference on the Engineering of Computer Based Systems. IEEE Press, April 2000. 185
E. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In CONCUR, LNCS 962, 1995. 174
D. L. Dill. The Murϕ verification system. In T. A. Henzinger, editors. Computer Aided Verification (CAV’ 96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996 Alur and Henzinger [AH96], pages 390–393. 172
G. Delzanno and A. Podelski. Model checking in CLP. In TACAS’99, volume LNCS 1579, pages 74–88. Springer-Verlag, March 1999. 172
X. Du, C.R. Ramakrishnan, and S.A. Smolka. Tabled resolution + constraints: A recipe for model checking real-time systems. Technical report, Dept. of Computer Science, SUNY Stony Brook, http://www.cs.sunysb.edu/~vicdu/papers, 1999. 173
X. Du, S. A. Smolka, and R. Cleaveland. Local model checking and protocol analysis. Software Tools for Technology Transfer, 1999. 185
E. Emerson and K.S. Namjoshi. Reasoning about rings. In POPL, pages 85–94, 1995. 174
S. Graf and H. Saidi. Verifying invariants using theorem proving. In T. A. Henzinger, editors. Computer Aided Verification (CAV’ 96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996 Alur and Henzinger [AH96]. 174
G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997. 172
C. N. Ip and D. L. Dill. Verifying systems with replicated components in Murϕ. Formal Methods in System Design, 14(3), May 1999. 174
R.P. Kurshan and K. Mcmillan. A structural induction theorem for processes. Information and Computation, 117:1–11, 1995. 174
KMM+97._Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model-checking with rich assertional languages. In CAV, LNCS 1254, 1997. 174
D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parametrized linear networks of processes. In POPL, pages 346–357, 1997. 174
J.W. Lloyd. Foundations of Logic Programming, Second Edition. Springer-Verlag, 1993. 176
K. L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993. 174
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. 176
S. Owre, N. Shankar, and J. Rushby. PVS: A Prototype Verification System. Proceedings of CADE, 1992. 174
A. Pettorossi and M. Proietti. Synthesis and transformation of logic programs using unfold/fold proofs. Journal of Logic Programming, 41, 1999. 174
A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, and I.V. Ramakrishnan. Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. In ASIAN, LNCS 1742, pages 322–333, 1999. 176
A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, and I.V. Ramakrishnan. A parameterized unfold/fold transformation framework for definite logic programs. In PPDP, LNCS 1702, pages 396–413, 1999. 173, 178, 179
A. Roychoudhury. Program transformations for automated verification of parameterized concurrent systems. Technical report, Department of Computer Science, State University of New York at Stony Brook, http://www.cs.sunysb.edu/~abhik/papers, 1999. Dissertation proposal. 179, 182
RRR+97._Y.S. Ramakrishna, C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, T. Swift, and D.S. Warren. Efficient model checking using tabled resolution. In CAV, LNCS 1254, 1997. 172, 176
S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In CAV, LNCS 939, 1995. 174
L. Urbina. Analysis of hybrid systems in CLP(R). In Constraint Programming (CP’96), volume LNCS 1102. Springer-Verlag, 1996. 172
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Automatic Verification Methods for Finite State Systems, LNCS 407, 1989. 174
The XSB logic programming system v2.01, 1999. Available by anonymous ftp from http://www.cs.sunysb.edu/~sbprolog. 185
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roychoudhury, A., Kumar, K.N., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A. (2000). Verification of Parameterized Systems Using Logic Program Transformations. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_13
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive