Abstract
Inspired by the success of model checking in hardware and protocol verification, model checking techniques for software have been the focus of a lot of research in the last few years [5,3,2,6]. Model checking can be applied only to relatively small models due to its inherently high computational requirements, and there are two complementary trends to address scalability. The model extraction approach, exemplified by projects such as Bandera [6] and SLAM [3], involves constructing inputs to model checkers by abstracting programs written in languages such as C and Java. The model-based design approach, exemplified by modeling notations such as Statecharts [7], promotes design using high-level models that are compiled into code. Our research agenda is to develop model checking techniques for model-based design of software.
Chapter PDF
Similar content being viewed by others
References
R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. In Proc. 27th POPL, pages 390–402, 2000.
R. Alur, R. Grosu, and M. McDougall. Efficient reachability analysis of hierarchical reactive machines. In Proc. 12th CAV, LNCS 1855, pages 280–295, 2000.
T. Ball and S. Rajamani. The SLAM toolkit. In Proc. 13th CAV, 2001.
R. Brayton, G. Hachtel, A. Sangiovanni-Vincentell, F. Somenzi, et. al. VIS: A system for verification and synthesis. In Proc. 8th CAV, LNCS 1102, pages 428–432, 1996.
W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. IEEE Trans. on Software Engg., 24(7):498–519, 1998.
J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. 22nd ICSE, pages 439–448. 2000.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
G. Holzmann. The model checker SPIN. IEEE Trans. on Software Engg., 23(5):279–295, 1997.
K. McMillan. Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., McDougall, M., Yang, Z. (2002). Exploiting Behavioral Hierarchy for Efficient Model Checking. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_25
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive