Abstract
We study how to exploit symmetry induced by identical processes or data structures when systematically exploring the state spaces of concurrent software applications such as implementations of communication protocols. Existing model-checking symmetry reduction methods are based on equivalence classes of states, and assume that every system state can easily be encoded by a unique string of bits. When dealing with processes described by software programs written in full-fledged programming languages such as C, C++ or Java, this assumption is not valid anymore. Indeed, the state of each process is determined by the values of all the memory locations that can be accessed by the process and influence its behavior (including activation records associated to procedure calls). This amount of information is typically far too large and complex to be efficiently computed at each step of a state-space exploration.
We develop in this paper a simple theory based on equivalence classes of sequences of transitions for representing symmetries in a system. We then present a state-space exploration algorithm for exploiting symmetries on transitions which does not rely on explicit encodings of system states. This algorithm can be used to dynamically prune the state spaces of implementations of concurrent reactive software systems in a reliable way.
Chapter PDF
Similar content being viewed by others
References
R.E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24 (3): 293–318, 1992.
E. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. In Proc. 5th Conference on Computer Aided Verification,volume 697 of Lecture Notes in Computer Science,pages 450–462, Elounda, June 1993. Springer-Verlag.
E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.
E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla. Symmetry Reductions in Model Checking. In Proc. 10th Conference on Computer Aided Verification,volume 1427 of Lecture Notes in Computer Science,pages 147–158, Vancouver, June/July 1998. Springer-Verlag.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 1 (15): 36–72, 1993.
S. Duri, U. Buy, R. Devarapalli, and S. M. Shatz. Application and Experimental Evaluation of State Space Reduction Methods for Deadlock Analysis in Ada. ACM Transactions on Software Engineering and Methodology, 3 (4): 340–380, October 1994.
E. A. Emerson, S. Jha, and D. Peled. Combining Partial Order and Symmetry Reductions. In Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97),volume 1217 of Lecture Notes in Computer Science,pages 19–34, Twente, April 1997. Springer-Verlag.
E. A. Emerson and A. P. Sistla. Symmetry and model checking. In Proc. 5th Conference on Computer Aided Verification,volume 697 of Lecture Notes in Computer Science,pages 463–478, Elounda, June 1993. Springer-Verlag.
A. R. Flora-Holmquist and M. Staskauskas. Formal validation of virtual finite state machines. In Proc. Workshop on Industrial-Strength Formal Specification Techniques (WIFT’95), pages 122–129, Boca Raton, April 1995.
P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996.
P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 174–186, Paris, January 1997.
P. Godefroid, R. S. Hanmer, and L. J. Jagadeesan. Model Checking Without a Model: An Analysis of the Heart-Beat Monitor of a Telephone Switch using VeriSoft. In Proceedings of ACM SIGSOFT ISSTA’98 (International Symposium on Software Testing and Analysis), pages 124–133, Clearwater Beach, March 1998.
J. A. Green. Sets and Groups - A First Course in Algebra. Routledge and Kegan Paul, 1965.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and con-currency. Journal of the ACM, 32 (1): 137–161, 1985.
G. J. Holzmann. Design and Validation-of Computer Protocols. Prentice Hall, 1991.
G. J. Holzmann and J. Patti. Validating sdl specifications: An experiment. In Proc. 9th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification. North-Holland, 1989.
C. N. Ip and D. L. Dill. Better verification through symmetry. In D. Agnew, L. Claesen, and R. Camposano, editors, Proceedings of the 1993 Conference on Computer Hardware Description Languages and their Applications, April 1993.
S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101: 337–359, 1992.
D. Kozen. Results on the Propositional Mu-Calculus. Theoretical Computer Science, 27: 333–354, 1983.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
A. Mazurkiewicz. Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course,volume 255 of Lecture Notes in Computer Science,pages 279–324. Springer-Verlag, 1986.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
A. Valmari. Stubborn sets for of colored petri nets. In Proceedings of the 12th International Conference on Apllications and Theory of Petri Nets, pages 102–121, Gjern, 1991.
M.Y. Vardi. Why is modal logic so robustly decidable? In Proceedings of DIMACS Workshop on Descriptive Complexity and Finite Models. AMS, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Godefroid, P. (1999). Exploiting Symmetry When Model-Checking Software. In: Wu, J., Chanson, S.T., Gao, Q. (eds) Formal Methods for Protocol Engineering and Distributed Systems. PSTV FORTE 1999 1999. IFIP Advances in Information and Communication Technology, vol 28. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35578-8_15
Download citation
DOI: https://doi.org/10.1007/978-0-387-35578-8_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5270-0
Online ISBN: 978-0-387-35578-8
eBook Packages: Springer Book Archive