Requirements-Level Semantics and Model Checking of Object-Oriented Statecharts

摘要

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. State-charts 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.