Abstract
Hierarchical state machines is a popular visual formalism for software specifications. To apply automated analysis to such specifications, the traditional approach is to compile them to existing model checkers. Aimed at exploiting the modular structure more effectively, our approach is to develop algorithms that work directly on the hierarchical structure. First, we report on an implementation of a visual hierarchical language with modular features such as nested modes, variable scoping, mode reuse, exceptions, group transitions, and history. Then, we identify a variety of heuristics to exploit these modular features during reachability analysis. We report on an enumerative as well as a symbolic checker, and case studies.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Alur, R., Grosu, R.: Modular refinement of hierarchic reactive machines. In: Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, pp. 390–402 (2000)
Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design 15(1), 7–48 (1999)
Alur, R., Henzinger, T., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS (LNAI), vol. 1427, pp. 516–520. Springer, Heidelberg (1998)
Aggarwal, S., Kurshan, R.P., Sharma, D.: A language for the specification and analysis of protocols. In: IFIP Protocol Specification, Testing, and Verification III, pp. 35–50 (1983)
Alur, R., Kannan, S., Yannakakis, M.: Communicating hierarchical state machines. In: Automata, Languages and Programming, 26th International Colloquium, pp. 169–178 (1999)
Alur, R., Yannakakis, M.: Model checking of hierarchical state ma- chines. In: Proceedings of the Sixth ACM Symposium on Foundations of Software Engineering, pp. 175–188 (1998)
Brayton, R., Hachtel, G., Sangiovanni-Vincentell, A., Somenzi, F., Aziz, A., Cheng, S., Edwards, S., Khatri, S., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R., Sarwary, S., Shiple, T., Swamy, G., Villa, T.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)
Booch, G., Jacobson, I., Rumbaugh, J.: Unified Modeling Language User Guide. Addison-Wesley, Reading (1997)
Behrmann, G., Larsen, K., Andersen, H., Hulgaard, H., Lind-Nielsen, J.: Verification of hierarchical state/event systems using reusability and compositionality. In: TACAS 1999: Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Software (1999)
Chan, W., Anderson, R., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.: Model checking large software specifications. IEEE Transactions on Software Engineering 24(7), 498–519 (1998)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. Workshop on Logic of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)
Clarke, E.M., Kurshan, R.P.: Computer-aided verification. IEEE Spectrum 33(6), 61–67 (1996)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 231–274 (1987)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Jahanian, F., Mok, A.K.: A graph-theoretic approach for timing analysis and its implementation. IEEE Transactions on Computers C-36(8), 961–975 (1987)
Leveson, N.G., Heimdahl, M., Hildreth, H., Reese, J.D.: Requirements specification for process control systems. IEEE Transactions on Software Engineerings 20(9) (1994)
McMillan, K.: Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, Dordrecht (1993)
Peterson, L., Davie, B.: Computer Networks: A Systems Approach. Morgan Kaufmann, San Francisco (1996)
Peterson, G.: Myths about the mutual exclusion problem. Information Processing Letters 12(3) (1981)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent programs in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 195–220. Springer, Heidelberg (1982)
Selic, B., Gullekson, G., Ward, P.T.: Real-time object oriented modeling and design. J. Wiley, Chichester (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Grosu, R., McDougall, M. (2000). Efficient Reachability Analysis of Hierarchical Reactive Machines. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_23
Download citation
DOI: https://doi.org/10.1007/10722167_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive