SMC: a symmetry-based model checker for verification of safety and liveness properties

ABSTRACT

The article presents the SMC system. SMC can be used for checking safety and liveness properties of concurrent programs under different fairness assumptions. It is based on explicit state enumeration. It combats the state explosion by exploiting symmetries of the input concurrent program, usually present in the form of identical processes, in two different ways. Firstly, it reduces the number of explored states by identifying those states that are equivalent under the symmetries of the system; this is called process symmetry. Secondly, it reduces the number of edges explored from each state, in0 the reduced state graph, by exploiting the symmetry of a single state; this is called state symmetry. SMC works in an on-the-fly manner; it constructs the reduced state graph as and when it is needed. This method facilitates early termination, speeds up model checking, and reduces memory requirements. We employed SMC to check the correctness of, among other standard examples, the Link Layer part of the IEEE Standard 1394 “Firewire” high-speed serial bus protocol. SMC found deadlocks in the protocol. SMC was also to check certain liveness properties. A report on the case study is included in the article.

REFERENCES

• 1: AGGARWAL, S., KURSHAN, R. P., AND SABNANI, K. K. 1983. A calculus for protocol specification and validation. In Proceedings of the Conference on Protocol Specification, Testing and Verification III, H. Ruden and C. West, Eds. North-Holland Publishing Co., Amsterdam, The Netherlands, 19-34.
• 2: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 3: ALUR, R., HENZINGER, T., AND HO, P. H. 1993. Autmatic symbolic verification of embedded systems. In Proceedings of the 14th Annual Real-Time Systems Symposium, IEEE Press, Piscataway, NJ, 2-11.
• 4: Girish Bhat , Rance Cleaveland , Orna Grumberg, Efficient On-the-Fly Model Checking for CTL, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.388, June 26-29, 1995
• 5: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 6: Edmund M. Clarke , Thomas Filkorn , Somesh Jha, Exploiting Symmetry In Temporal Logic Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.450-462, June 28-July 01, 1993
• 7: E. Allen Emerson , Chin-Laung Lei, Modalities for model checking: branching time logic strikes back, Science of Computer Programming, v.8 n.3, p.275-306, June 1, 1987 [doi>10.1016/0167-6423(87)90036-0 ]
• 8: E. Allen Emerson , A. Prasad Sistla, Symmetry and Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.463-478, June 28-July 01, 1993
• 9: E. Allen Emerson , A. Prasad Sistla, Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach, Proceedings of the 7th International Conference on Computer Aided Verification, p.309-324, July 03-05, 1995
• 10: Nissim Francez, Fairness, Springer-Verlag New York, Inc., New York, NY, 1986
• 11: GODEFROID, P. 1996. Partial-Order Methods for the Verificaiton of Concurrent Systems. Springer Lecture Notes in Computer Science, vol. 1032. Springer-Verlag, New York.
• 12: R. L. Graham , M. Grötschel , L. Lovász, Handbook of combinatorics (vol. 1), MIT Press, Cambridge, MA, 1996
• 13: R. L. Graham , M. Grötschel , L. Lovász, Handbook of combinatorics (vol. 2), MIT Press, Cambridge, MA, 1996
• 14: Viktor Gyuris , A. Prasad Sistla, On-the-Fly Model Checking Under Fairness That Exploits Symmetry, Proceedings of the 9th International Conference on Computer Aided Verification, p.232-243, June 22-25, 1997
• 15: Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045 ]
• 16: HOLZMANN, G. J. AND PELED, D. 1984. An improvement in formal verification. In Proceedings of the FORTE 1984 Conference (Bern, Switzerland),
• 17: Gerard J. Holzmann , Doron Peled, The State of SPIN, Proceedings of the 8th International Conference on Computer Aided Verification, p.385-389, August 03, 1996
• 18: IEEE. 1995. IEEE Standard 1394 for High Performance Serial Bus. IEEE Press, Piscataway, NJ.
• 19: C. Norris Ip , David L. Dill, Better verification through symmetry, Formal Methods in System Design, v.9 n.1-2, p.41-75, Aug. 1996 [doi>10.1007/BF00625968]
• 20: Kurt Jensen, Coloured Petri nets: basic concepts, analysis methods and practical use, vol. 2, Springer-Verlag, London, 1995
• 21: Kurt Jensen , Grzegorz Rozenberg, High-level Petri nets: theory and application, Springer-Verlag, London, 1991
• 22: JHA, S. 1996. Symmetry and induction in model checking. Ph.D. Dissertation.
• 23: KUHNE, L., HOOMAN, J., AND DE ROEVER, W. 1997. Towards mechanical verification of parts of the IEEE p1394 serial bus. In Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia, June (1997)),
• 24: KURSHAN, R. P. 1986. Testing containment of omega-regular languages. Tech. Rep. 1121-861010-33. AT&T Bell Laboratories, Inc., Murray Hill, NJ.
• 25: KURSHAN, R. P. 1987. Testing containment of omega-regular languages. In Reducibility in Analysis of Coordination, R. P. Kurshan Springer-Verlag, New York, 19-39.
• 26: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 27: LUTTIK, B. 1997. Description and formal specification of the link layer of p1394. In Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia, June (1997)),
• 28: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 29: MCMILLAN, K. L. 1992. The smv system, draft. Computer Science Department, Carnegie Mellon University, Pittsburgh, PA. http://www.cs.cmu.edu/afs/cs/project/modck/pub/www/smv.html.
• 30: SIGHIREANU, M. AND MATEESCU, R. 1997. Validation of the link layer protocol of the IEEE-1394 serial bus ("firewire"), an experiment with e-lotos.
• 31: TARJAN, R. E. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2 (1972), 146-160.
• 32: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 33: VARDI, M. AND WOLPER, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the First Annual Symposium on Logic in Computer Science (Cambridge, MA, June16-18), IEEE Computer Society Press, Los Alamitos, CA, 322-331.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Algorithms, Performance, Standardization, Verification

Keywords:
automata, model checking