Requirements-level semantics and model checking of object-oriented statecharts

被引：21
作者：
Eshuis R. [1 ,2 ]
Jansen D.N. [1 ]
Wieringa R. [1 ]
机构：
[1] Department of Computer Science, University of Twente, Enschede
[2] Department of Computer Science, University of Twente, 7500 AE Enschede
来源：
Requirements Engineering | 2002年 / 7卷 / 4期
关键词：
Execution semantics; Model checking; Statecharts;
D O I：
10.1007/s007660200019
中图分类号：
学科分类号：
摘要：
In this paper we define a requirements-level execution semantics for object-oriented statecharts and show how properties of a system specified by these statecharts can be model checked using tool support for model checkers. Our execution semantics is requirements-level because it uses the perfect technology assumption, which abstracts from limitations imposed by an implementation. Statecharts describe object life cycles. Our semantics includes synchronous and asynchronous communication between objects and creation and deletion of objects. Our tool support presents a graphical front-end to model checkers, making these tools usable to people who are not specialists in model checking. The model-checking approach presented in this paper is embedded in an informal but precise method for software requirements and design. We discuss some of our experiences with model checking. © 2002 Springer-Verlag London Limited.
引用
收藏
页码：243 / 263
页数：20
相关论文
共 60 条
[1]  
Harel D., Statecharts: A visual formalism for complex systems, Sci Comput Program, 8, 3, pp. 231-274, (1987)
[2]  
Harel D., Pnueli A., On the development of reactive systems, Logics and Models of Concurrent Systems, pp. 477-498, (1985)
[3]  
Rumbaugh J., Blaha M., Premerlani W., Eddy F., Lorensen W., Object-oriented Modeling and Design, (1991)
[4]  
Rumbaugh J., Jacobson I., Booch G., The Unified Modeling Language Reference Manual, (1999)
[5]  
Von Der Beeck M., A comparison of Statecharts variants, Lecture Notes in Computer Science, 863, pp. 128-148, (1994)
[6]  
Action Semantics for the UML (OMG Ad/2001-03-01), (2001)
[7]  
Dehne F., Wieringa R., Van De Zandschulp H., Toolkit for Conceptual Modeling (TCM): User's Guide and Reference, (2000)
[8]  
McMillan K.L., Symbolic Model Checking, (1993)
[9]  
Cimatti A., Clarke E., Giunchiglia F., Roveri M., NuSMV: A new symbolic model checker, Int J Software Tools Technol Transfer, 2, 4, pp. 410-425, (2000)
[10]  
Yovine S., KRONOS: A verification tool for real-time systems, Int J Software Tools Technol Transfer, 1, 1-2, pp. 123-133, (1997)
123456