Skip to main content
SpringerLink
Log in

Formal Analysis of Hierarchical State Machines

Dedicated to Zohar Manna on His 26th Birthday

  • Chapter
Book cover Verification: Theory and Practice

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2772))

Abstract

In hierarchical state machines, the states can be ordinary states or superstates which are state machines themselves. The notion of hierarchical state machines was popularized by the introduction of Statecharts, and exists in various object-oriented software development methodologies. This paper surveys results concerning the impact of hierarchy for formal specification and verification. We present a systematic study of the complexity of model checking problems in presence of hierarchy, the succinctness afforded by hierarchy from a language-theoretic perspective, and heuristics for exploiting hierarchy in model checking tools.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. In Proc. of the 13th International Conference on Computer Aided Verification, LNCS 2102, pages 207-220. Springer, 2001.

    Google Scholar 

  2. R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. In Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, pages 390-402, 2000.

    Google Scholar 

  3. R. Alur, R. Grosu, and M. McDougall. Efficient reachability analysis of hierarchical reactive machines. In Computer Aided Verification, 12th International Conference, LNCS 1855, pages 280-295. Springer, 2000.

    Google Scholar 

  4. R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In Automata, Languages and Programming, 26th International Colloquium, pages 169-178. Springer, 1999.

    Google Scholar 

  5. R. Alur, S. La Torre, and P. Madhusudan. Modular strategies for recursive game graphs. In TACAS’03: Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Software, LNCS 2619, pages 363-378, 2003.

    Google Scholar 

  6. R. Alur, M. McDougall, and Z. Yang. Exploiting behavioral hierarchy for efficient model checking. In Computer Aided Verification, 14th International Conference, LNCS 2404, pages 338-342. Springer, 2002.

    Google Scholar 

  7. R. Alur and M. Yannakakis. Model checking of hierarchical state machines. ACM Transactions on Programming Languages and Systems, 23(3):1–31, 2001.

    Article  Google Scholar 

  8. T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, pages 113-130. Springer, 2000.

    Google Scholar 

  9. T. Ball and S. Rajamani. The SLAM toolkit. In Computer Aided Verification, 13th International Conference, 2001.

    Google Scholar 

  10. G. Behrmann, K. Larsen, H. Andersen, H. Hulgaard, and J. Lind-Nielsen. Verification of hierarchical state/event systems using reusability and compositionality. In TACAS’ 99: Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Software, LNCS 1579, pages 163-177. Springer, 1999.

    Google Scholar 

  11. M. Benedikt, P. Godefroid, and T. Reps. Model checking of unrestricted hierarchical state machines. In Automata, Languages and Programming, 28th International Colloquium, volume LNCS 2076, pages 652-666. Springer, 2001.

    Google Scholar 

  12. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 193-207, 1999.

    Google Scholar 

  13. G. Booch, I. Jacobson, and J. Rumbaugh. Unified Modeling Language User Guide. Addison Wesley, 1997.

    Google Scholar 

  14. A. Boujjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR’97: Concurrency Theory, Eighth International Conference, LNCS 1243, pages 135-150. Springer, 1997.

    Google Scholar 

  15. R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In Proceedings of the Eighth International Conference on Computer Aided Verification, LNCS 1102, pages 428-432. Springer-Verlag, 1996.

    Google Scholar 

  16. R. Bryant. Graph-based algorithms for boolean-function manipulation. IEEE Transactions on Computers, C-35(8), 1986.

    Google Scholar 

  17. J. Burch, E. Clarke, D. Dill, L. Hwang, and K. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  18. O. Burkart and B. Steffen. Model checking for context-free processes. In CONCUR’92: Concurrency Theory, Third International Conference, LNCS 630, pages 123-137. Springer, 1992.

    Google Scholar 

  19. A. Chakrabarti, L. de Alfaro, T. Henzinger, M. Jurdzinski, and F. Mang. Interface compatibility checking for software modules. In Proceedings of the 14th International Conference on Computer-Aided Verification, LNCS 2404, pages 428-441. Springer, 2002.

    Google Scholar 

  20. W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498–519, 1998.

    Article  Google Scholar 

  21. E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pages 52-71. Springer-Verlag, 1981.

    Google Scholar 

  22. E. Clarke, O. Grumberg, and D. Peled. Model checking. MIT Press, 2000.

    Google Scholar 

  23. E. Clarke and R. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61–67, 1996.

    Article  Google Scholar 

  24. C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.

    Article  Google Scholar 

  25. D. Drusinsky and D. Harel. On the power of bounded concurrency I: finite automata. Journal of the ACM, 41(3):517–539, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  26. J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Computer Aided Verification, 12th International Conference, LNCS 1855, pages 232-247. Springer, 2000.

    Google Scholar 

  27. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  28. T. Henzinger, R. Jhala, R. Majumdar, G. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In CAV 02: Proc. of 14th Conf. on Computer Aided Verification, LNCS 2404, pages 526-538. Springer, 2002.

    Google Scholar 

  29. G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.

    Google Scholar 

  30. G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.

    Article  MathSciNet  Google Scholar 

  31. J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

    Google Scholar 

  32. O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, 2000.

    Article  MATH  MathSciNet  Google Scholar 

  33. R. Kurshan. Computer-aided Verification of Coordinating Processes: the automata-theoretic approach. Princeton University Press, 1994.

    Google Scholar 

  34. S. La Torre, M. Napoli, M. Parento, and G. Parlato. Hierarchical and recursive state machines with context dependent properties. In Automata, Languages and Programming, 30th International Colloquium, LNCS 2719, pages 776-789, 2003.

    Google Scholar 

  35. N. Leveson, M. Heimdahl, H. Hildreth, and J. Reese. Requirements specification for process control systems. IEEE Transactions on Software Engineering, 20(9):684–707, 1994.

    Article  Google Scholar 

  36. O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 97-107, 1985.

    Google Scholar 

  37. Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems: Specification. Springer-verlag, 1991.

    Google Scholar 

  38. K. McMillan. Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, 1993.

    Google Scholar 

  39. A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46-77, 1977.

    Google Scholar 

  40. B. Selic, G. Gullekson, and P. Ward. Real-time object oriented modeling and design. J. Wiley, 1994.

    Google Scholar 

  41. W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133-191. Elsevier Science Publishers, 1990.

    Google Scholar 

  42. M. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  43. I. Walukiewicz. Pushdown processes: Games and model-checking. Information and Computation, 164(2):234–263, 2001.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer and Information Science, University of Pennsylvania, 3330 Walnut Street, Philadelphia, PA, 19104, USA

    Rajeev Alur

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science, Tel Aviv University, Ramat Aviv, Tel Aviv, 69978, Israel

    Nachum Dershowitz

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Alur, R. (2003). Formal Analysis of Hierarchical State Machines. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39910-0_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21002-3

  • Online ISBN: 978-3-540-39910-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation