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

Eshuis, Rik and Jansen, David N. and Wieringa, Roel (2002) Requirements-level semantics and model checking of object-oriented statecharts. Requirements engineering, 7 (4). pp. 243-263. ISSN 09473602

PDF
Restricted to UT campus only: Request a copy
419Kb

Abstract:	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.
Item Type:	Article
Copyright:	© 2002 Springer-Verlag London Limited
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Information Systems (IS)
Link to this item:	http://purl.utwente.nl/publications/38256
Official URL:	http://dx.doi.org/10.1007/s007660200019
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 209492