Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

Verifying correctness properties of parameterized systems is a long-standing problem. The challenge lies in the lack of guarantee that the property is satisfied for all instances of the parameterized system. Existing work on addressing this challenge aims to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the cut-off. A property satisfied on the system with the cut-off ensures that it is satisfied for systems with any larger parameter. The major problem with these techniques is that they only work for certain classes of systems with specific communication topology such as ring topology, thus leaving other interesting classes of systems unverified. We contribute an automated technique for finding the cut-off of the parameterized system that works for systems defined with any topology. Given the specification and the topology of the system, our technique is able to automatically generate the cut-off specific to this system. We prove the soundness of our technique and demonstrate its effectiveness and practicality by applying it to several canonical examples where in some cases, our technique obtains smaller cut-off values than those presented in the existing literature.

REFERENCES

• 1: P. A. Abdulla, G. Delzanno, N. B. Henda, and A. Rezine. Regular model checking without transducers (on efficient verification of parameterized systems). In TACAS, pages 721-736, 2007.
• 2: Parosh Aziz Abdulla , Bengt Jonsson , Marcus Nilsson , Julien d'Orso, Regular Model Checking Made Simple and Efficient, Proceedings of the 13th International Conference on Concurrency Theory, p.116-130, August 20-23, 2002
• 3: T. E. Anderson, The Performance of Spin Lock Alternatives for Shared-Memory Multiprocessors, IEEE Transactions on Parallel and Distributed Systems, v.1 n.1, p.6-16, January 1990 [doi>10.1109/71.80120]
• 4: 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]
• 5: Tamarah Arons , Amir Pnueli , Sitvanit Ruah , Jiazhao Xu , Lenore D. Zuck, Parameterized Verification with Automatically Computed Inductive Assertions, Proceedings of the 13th International Conference on Computer Aided Verification, p.221-234, July 18-22, 2001
• 6: Paolo Baldan , Andrea Corradini , Barbara König, A framework for the verification of infinite-state graph transformation systems, Information and Computation, v.206 n.7, p.869-907, July, 2008 [doi>10.1016/j.ic.2008.04.002]
• 7: P. Baldan, B. König, and A. Rensink. Graph grammar verification through abstraction. In Dagstuhl Seminar Proceedings 04241, 2005.
• 8: Thomas Ball , Sagar Chaki , Sriram K. Rajamani, Parameterized Verification of Multithreaded Software Libraries, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.158-173, April 02-06, 2001
• 9: Samik Basu , C. R. Ramakrishnan, Compositional analysis for verification of parameterized systems, Theoretical Computer Science, v.354 n.2, p.211-229, 28 March 2006 [doi>10.1016/j.tcs.2005.11.016]
• 10: Ahmed Bouajjani , Bengt Jonsson , Marcus Nilsson , Tayssir Touili, Regular Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, p.403-418, July 15-19, 2000
• 11: A. Bouajjani, Y. Jurski, and M. Sighireanu. Reasoning about dynamic networks of infinite-state processes with global synchronization. HAL - CCSD, 2006.
• 12: A. Bouajjani, Y. Jurski, and M. Sighireanu. A generic framework for reasoning about dynamic networks of infinite-state processes. In TACAS, pages 690--705, 2007.
• 13: E. Clarke, M. Talupur, and H. Veith. Environment abstraction for parameterized verification. In VMCAI, 126--141, 2006.
• 14: Edmund M. Clarke , Orna Grumberg , Somesh Jha, Veryfying Parameterized Networks using Abstraction and Regular Languages, Proceedings of the 6th International Conference on Concurrency Theory, p.395-407, August 21-24, 1995
• 15: E. M. Clarke, M. Talupur, and H. Veith. Proving ptolemy right: The environment abstraction framework for model checking concurrent systems. In TACAS, pages 33--47, 2008.
• 16: E. Dijkstra. Two starvation free solutions to a general exclusion problem. EWD 625, Plataanstraat 5, 5671 AL Neunen, The Netherlands.
• 17: E. Allen Emerson , Vineet Kahlon, Model Checking Large-Scale and Parameterized Resource Allocation Systems, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.251-265, April 08-12, 2002
• 18: E. A. Emerson and V. Kahlon. Exact and efficient verification of parameterized cache coherence protocols. In CHARME, pages 247--262, 2003.
• 19: 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]
• 20: E. Allen Emerson , Kedar S. Namjoshi, Automatic Verification of Parameterized Synchronous Systems (Extended Abstract), Proceedings of the 8th International Conference on Computer Aided Verification, p.87-98, August 03, 1996
• 21: E. A. Emerson, R. J. Trefler, and T. Wahl. Reducing model checking of the few to the one. In ICFEM, pp. 94--113, 2006.
• 22: D. Fisman, O. Kupferman, and Y. Lustig. On verifying fault tolerance of distributed protocols. In TACAS, 315-331, 2008.
• 23: 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]
• 24: Y. Hanna, S. Basu, and H. Rajan. Behavioral automata composition for automatic topology independent verification of parameterized systems. Technical Report 09-17, Computer Sc., Iowa State U., 2009.
• 25: C. Norris Ip , David L. Dill, Verifying Systems with Replicated Components in Murphi, Proceedings of the 8th International Conference on Computer Aided Verification, p.147-158, August 03, 1996
• 26: M. Llorens and J. Oliver. Introducing structural dynamic changes in petri nets: Marked-controlled reconfigurable nets. In ATVA, pages 310--323, 2004.
• 27: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 28: Amir Pnueli , Sitvanit Ruah , Lenore D. Zuck, Automatic Deductive Verification with Invisible Invariants, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.82-97, April 02-06, 2001
• 29: Amir Pnueli , Jessie Xu , Lenore D. Zuck, Liveness with (0, 1, infty)-Counter Abstraction, Proceedings of the 14th International Conference on Computer Aided Verification, p.107-122, July 27-31, 2002
• 30: M. Saksena, O. Wibling, and B. Jonsson. Graph grammar modeling and verification of ad hoc routing protocols. In TACAS, pages 18--32, 2008.
• 31: Pierre Wolper , Vinciane 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, June 12-14, 1989

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Verification

Keywords:
parameterized model checking