Requirements-Level Semantics and Model Checking of Object-Oriented Statecharts |
| |
Authors: | Eshuis Rik Jansen David N Wieringa Roel |
| |
Affiliation: | (1) Department of Computer Science, University of Twente, Enschede, The Netherlands, NL |
| |
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.
Correspondence and offprint requests to: Rik Eshuis, Department of Computer Science, University of Twente, PO Box 217, 7500 AE Enschede, The Netherlands. Email: eshuis@cs.utwente.nl |
| |
Keywords: | :Execution semantics – Model checking – Statecharts |
本文献已被 SpringerLink 等数据库收录! |
|