Efficient Formal Verification of Hierarchical Descriptions
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.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