Space Reductions for Model Checking Quasi-Cyclic Systems

  • Matthew B. Dwyer
  • Non Robby
  • Xianghua Deng
  • John Hatcliff
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2855)


Despite significant research on state-space reductions, the poor scalability of model checking for reasoning about behavioral models of large, complex systems remains the chief obstacle to its broad acceptance. One strategy for making further progress is to exploit characteristics of classes of systems to develop domain-specific reductions.

In this paper, we identify a structural property of system state-spaces, which we call quasi-cyclic structure, that can be leveraged to significantly reduce the space requirements of model checking. We give a formal characterization of quasi-cyclic state-spaces and describe a state-space exploration algorithm for exploiting that structure. In addition, we describe a class of real-time embedded systems that are quasi-cyclic, we outline how we customized an existing model checking framework to implement space-efficient search of quasi-cyclic systems, and we present experimental data that demonstrate multiple orders of magnitude reductions in space consumption.


Model Check Modal Component Program Counter Space Reduction Space Consumption 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. International Journal on Software Tools for Technology Transfer. Springer (2002)Google Scholar
  3. 3.
    Chan, W., Anderson, R.J., Beame, P., Notkin, D., Jones, D.H., Warner, W.E.: Optimizing symbolic model checking for statecharts. IEEE Transactions on Software Engineering 27(2), 170–190 (2001)CrossRefGoogle Scholar
  4. 4.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  5. 5.
    Deng, W., Dwyer, M., Hatcliff, J., Jung, G., Robby, X.D.: Model-checking middlewarebased event-driven real-time embedded software. In: Proceedings of the 1st International Symposium on Formal Methods for Component and Objects (2002)Google Scholar
  6. 6.
    Dyer, M.: The Cleanroom Approach to Quality Software Development. Wiley, Chichester (1992)zbMATHGoogle Scholar
  7. 7.
    Godefroid, P.: Model-checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL 1997), January 1997, pp. 174–186 (1997)Google Scholar
  8. 8.
    Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 178–191. Springer, Heidelberg (1993)Google Scholar
  9. 9.
    Hatcliff, J., Deng, W., Dwyer, M., Jung, G., Prasad, V.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: Proceedings of the 25th International Conference on Software Engineering (2003)Google Scholar
  10. 10.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, January 2002, pp. 58–70 (2002)Google Scholar
  11. 11.
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–294 (1997)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Iosif, R.: Symmetry reduction criteria for software model checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 22–41. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Robby, X.D., Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)Google Scholar
  14. 14.
    Sharp, D.: Reducing avionics software cost through component based product line development. In: Proceedings of the Software Technology Conference (April 1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Matthew B. Dwyer
    • 1
  • Non Robby
    • 1
  • Xianghua Deng
    • 1
  • John Hatcliff
    • 1
  1. 1.Department of Computing and Information SciencesKansas State UniversityManhattanUSA

Personalised recommendations