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
相关论文
共 50 条
  • [41] Automatic Dimension Inference and Checking for Object-Oriented Programs
    Hangal, Sudheendra
    Lam, Monica S.
    2009 31ST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 155 - 165
  • [42] Method restructuring and consistency checking for object-oriented schemas
    Tari, Z
    Li, X
    ENTITY-RELATIONSHIP APPROACH - ER '94, 1994, 881 : 152 - 170
  • [43] Hierarchical object-oriented software requirements model and its mechanical support
    Nanjing Univ, Nanjing, China
    Ruan Jian Xue Bao, 6 (414-418):
  • [44] Software Requirements Translation from Natural Language to Object-Oriented Model
    Fatwanto, Agung
    2012 IEEE CONFERENCE ON CONTROL, SYSTEMS & INDUSTRIAL INFORMATICS (ICCSII), 2012, : 191 - +
  • [45] DEVELOPING FORMAL OBJECT-ORIENTED REQUIREMENTS SPECIFICATIONS - A MODEL, TOOL AND TECHNIQUE
    JACKSON, RB
    EMBLEY, DW
    WOODFIELD, SN
    INFORMATION SYSTEMS, 1995, 20 (04) : 273 - 289
  • [46] A weakest precondition semantics for refinement of object-oriented programs
    Cavalcanti, A
    Naumann, DA
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2000, 26 (08) : 713 - 728
  • [47] A weakest precondition semantics for an object-oriented language of refinement
    Cavalcanti, A
    Naumann, DA
    FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1439 - 1459
  • [48] OBJECT-ORIENTED PROGRAMMING ENVIRONMENTS - REQUIREMENTS AND APPROACHES
    BISCHOFBERGER, WR
    KOFLER, T
    SCHAFFER, B
    SOFTWARE-CONCEPTS AND TOOLS, 1994, 15 (02): : 49 - 60
  • [49] Tracing object-oriented code into functional requirements
    Antoniol, G
    Canfora, G
    Casazza, G
    De Lucia, A
    Merlo, E
    8TH INTERNATIONAL WORKSHOP ON PROGRAM COMPREHENSION (IWPC 2000), PROCEEDINGS, 2000, : 79 - 86
  • [50] Requirements for object-oriented systems modeling with STEAMS
    Peterson, GD
    Wilsey, P
    BMAS 2001: PROCEEDINGS OF THE FIFTH IEEE INTERNATIONAL WORKSHOP ON BEHAVIORAL MODELING AND SIMULATION, 2001, : 45 - 52
12345