Abstract
We investigate techniques for verifying hierarchical systems, i.e., finite state systems with a nesting capability. The straightforward way of analysing a hierarchical system is to first flatten it into an equivalent non-hierarchical system and then apply existing finite state system verification techniques. Though conceptually simple, flattening is severely punished by the hierarchical depth of a system. To alleviate this problem, we develop a technique that exploits the hierarchical structure to reuse earlier reachability checks of superstates to conclude reachability of substates. We combine the reusability technique with the successful compositional technique of [13] and investigate the combination experimentally on industrial systems and hierarchical systems generated according to our expectations to real systems. The experimental results are very encouraging: whereas a flattening approach degrades in performance with an increase in the hierarchical depth (even when applying the technique of [13]), the new approach proves not only insensitive to the hierarchical depth, but even leads to improved performance as the depth increases.
Supported by CIT, The Danish National Center of IT Research.
BRICS: Basic Research in Computer Science, Center of the Danish National Research Foundation
Chapter PDF
References
Baan VisualState A/S. http://www.visualstate.com.
I-Logix Inc. http://www.ilogix.com.
ObjecTime Limited. http://www.objectime.on.ca.
Rational Software Corporation. http://www.rational.com.
Rajeev Alur and Mihalis Yannakakis. Model Checking of Hierarchical State Machines. Proceedings of the 6th ACM Symposium on Foundations, 1998.
Steffen Braa Andersen, Gerd Behrmann, Claus Krogholm Pedersen, and Peter Smed Vestergaard. Reuseability and Compositionality applied to Verification of Hierarchical Systems. Master’s thesis, Aalborg University, June 1998.
Gerd Behrmann, Kim G. Larsen, Henrik R. Andersen, Henrik Hulgaard, and Jørn Lind-Nielsen. Verification of Hierarchical State/Event Systems. To appear as a BRICS report (http://www.brics.dk), 1999.
G. Booch, I. Jacobsen, and J. Rumbaugh. Unified Modelling Language User Guide. Addison Wesley, 1997.
Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35:677–691, August 1986.
David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
F. Jahanian and A. K. Mok. A graphtheoretic approach for timing analysis and its implementation. IEEE Transactions on Computers, C-36(8):961–975, 1987.
N. G. Leveson, M. P. E. Heimdahl, H. Hildreth, and J. D. Reese. Requiremets specification for process control systems. IEEE Transactions on Software Engineering, 20(9):694–707, September 1994.
Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre Kristoffersen, and Kim G. Larsen. Verification of Large State/Event Systems using Compositionality and Dependency Analysis. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 201–216. Springer, March/April 1998.
David Y. W. Park, Jens U. Skakkebæk, and David L. Dill. Static Analysis to Identify Invariants in RSML Specifications. In Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of Lecture Notes in Computer Science, pages 133–142. Springer, September 1998.
J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-oriented modeling and design. Prentice-Hall, 1991.
B. Selic, G. Gullekson, and P. T. Ward. Real-time object oriented modeling and design. J. Wiley, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Behrmann, G., Larsen, K.G., Andersen, H.R., Hulgaard, H., Lind-Nielsen, J. (1999). Verification of Hierarchical State/Event Systems Using Reusability and Compositionality. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_12
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive