Verifying parameterized networks

ABSTRACT

This article describes a technique based on network grammars and abstraction to verify families of state-transition systems. The family of state-transition systems is represented by a context-free network grammar. Using the structure of the network grammar our technique constructs a process invariant that simulates all the state-transition systems in the family. A novel idea introduced in this article is the use of regular languages to express state properties. We have implemented our techniques and verified two nontrivial examples.

REFERENCES

• 1: K R Apt , D C Kozen, Limits for automatic verification of finite-state concurrent systems, Information Processing Letters, v.22 n.6, p.307-309, May 30,1986 [doi>10.1016/0020-0190(86)90071-2]
• 2: M. C. Browne , E. M. Clarke , O. Grumberg, Reasoning about networks with many identical finite state processes, Information and Computation, v.81 n.1, p.13-31, April 1989 [doi>10.1016/0890-5401(89)90026-6]
• 3: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 4: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 5: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 6: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
• 7: DAMS, D., GRUMBERG, O., AND GERTH, R. 1994. Abstract interpretation of reactive systems: Abstractions preserving ACTL*,ECTL*, and CTL*. In IFIP Working Conference and Programming Concepts, Methods and Calculi (PROCOMET'9~), (San Miniato, Italy).
• 8: E. W. Dijkstra, Invariance and non-determinacy, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.157-165, June 1985, London, United Kingdom
• 9: Samuel Eilenberg, Automata, Languages, and Machines, Academic Press, Inc., Orlando, FL, 1974
• 10: E. Allen Emerson , Kedar S. Namjoshi, Reasoning about rings, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-94, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199468]
• 11: Steven M. German , A. Prasad Sistla, Reasoning about systems with many processes, Journal of the ACM (JACM), v.39 n.3, p.675-735, July 1992 [doi>10.1145/146637.146681]
• 12: Orna Grumberg , David E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.843-871, May 1994 [doi>10.1145/177492.177725]
• 13: R. P. Kurshan , K. McMillan, A structural induction theorem for processes, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.239-247, June 1989, Edmonton, Alberta, Canada [doi>10.1145/72981.72998]
• 14: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 15: MARELLY, R. AND GRUMBERG, O. 1991. GORMEL--Grammar ORiented ModEL checker. Tech. Rep. 697, The Technion, Haifa, Israel. Oct.
• 16: MILNER, R. 1971. An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence.
• 17: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 18: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 19: Z. Shtadler , O. Grumberg, Network grammars, communication behaviors and automatic verification, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.151-165, February 1990, Grenoble, France
• 20: Jeffrey D Ullma, Computational Aspects of VLSI, W. H. Freeman & Co., New York, NY, 1984
• 21: VERNIER, I. 1994. Parameterized evaluation of CTL-X formulae. In Workshop Accompanying the International Conference on Temporal Logic (ICTL'9~).
• 22: P. Wolper , V. Lovinfosse, Verifying properties of large sets of processes with network invariants, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.68-80, February 1990, Grenoble, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Theory, Verification

Keywords:
model checking, parameterized systems, process invariants, temporal logic