Efficient Formal Verification of Hierarchical Descriptions

  • Rajeev Alur
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1530)


Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. We investigate the model checking of hierarchical (nested) systems, i.e. finite state machines whose states themselves can be other machines. This nesting ability is common in various software design methodologies and is available in several commercial modeling tools. The straightforward way to analyze a hierarchical machine is to flatten it (thus, incurring an exponential blow up) and apply a model checking tool on the resulting ordinary FSM.


  1. 1.
    Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. In: Proceedings of the Sixth ACM SIGSOFT Symposium on Foundations of Software Engineering (November 1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Rajeev Alur
    • 1
  1. 1.Department of Computer & Information ScienceUniversity of PennsylvaniaPhiladelphiaUSA

Personalised recommendations