A case study in verification of UML statecharts: The PROFIsafe protocol

被引：0
|
作者：
Malik, R [1 ]
Muhlfeld, R
机构：
[1] Univ Waikato, Dept Comp Sci, Hamilton, New Zealand
[2] Siemens Corp Technol, D-91050 Erlangen, Germany
来源：
JOURNAL OF UNIVERSAL COMPUTER SCIENCE | 2003年 / 9卷 / 02期
关键词：
reliability; verification;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We discuss our experience obtained during the PROFIsafe verification and test case generation project at Siemens Corporate Technology. In this project, a formal analysis of the PROFIsafe protocol for failsafe communication has been carried out. A formal model based on finite-state machines has been obtained from the UML specification of the protocol. This model has been analysed with formal verification techniques, and several important properties have been proven. Based on the verified model, a set of test cases for the automatic execution of conformance tests has been derived. The paper explains how the UML statecharts defining the PROFIsafe protocol are translated into finite-state machines, and points out important aspects and problems occurring during the modelling and verification of industrial applications.
引用
收藏
页码：138 / 151
页数：14
相关论文
共 50 条
  • [1] Transforming UML 'collaborating' statecharts for verification and simulation
    Bobbie, PO
    Ji, YM
    Liang, LS
    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XVIII, PROCEEDINGS: INFORMATION SYSTEMS, CONCEPTS AND APPLICATIONS OF SYSTEMICS, CYBERNETICS AND INFORMATICS, 2002, : 61 - 66
  • [2] Design and verification of industrial logic controllers with UML and statecharts
    Bonfè, M
    Fantuzzi, C
    CCA 2003: PROCEEDINGS OF 2003 IEEE CONFERENCE ON CONTROL APPLICATIONS, VOLS 1 AND 2, 2003, : 1029 - 1034
  • [3] Test case generation for UML statecharts
    Seifert, D
    Helke, S
    Santen, T
    PERSPECTIVES OF SYSTEM INFORMATICS, 2003, 2890 : 462 - 468
  • [4] Formal verification of UML statecharts with real-time extensions
    David, A
    Möller, MO
    Yi, W
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2306 : 218 - 232
  • [5] Using a process algebra interface for verification and validation of UML statecharts
    Doostali, Saeed
    Babamir, Seyed Morteza
    Javani, Mohammad
    COMPUTER STANDARDS & INTERFACES, 2023, 86
  • [6] Formal Verification of UML Statecharts using the LOTOS Formal Language
    Javani, Mohamad
    Neysiani, Behzad Soleimani
    Babamir, Seyed Morteza
    2015 2ND INTERNATIONAL CONFERENCE ON KNOWLEDGE-BASED ENGINEERING AND INNOVATION (KBEI), 2015, : 754 - 760
  • [7] A transformation approach for modeling and analysis of complex UML statecharts: A case study
    Hu, ZX
    Shatz, SM
    SERP '05: PROCEEDINGS OF THE 2005 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH AND PRACTICE, VOLS 1 AND 2, 2005, : 361 - 367
  • [8] On testing UML statecharts
    Massink, Mieke
    Latella, Diego
    Gnesi, Stefania
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2006, 69 (1-2): : 1 - 74
  • [9] Formal test-case generation for UML statecharts
    Gnesi, S
    Latella, D
    Massink, M
    NINTH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING COMPLEX COMPUTER SYSTEMS, PROCEEDINGS: NAVIGATING COMPLEXITY IN THE E-ENGINEERING AGE, 2004, : 75 - 84
  • [10] A Dynamic Assertion-based verification platform for UML Statecharts over Rhapsody
    Banerjee, A.
    Ray, S.
    Dasgupta, P.
    Chakrabarti, P. P.
    Ramesh, S.
    Vignesh, P.
    Ganesan, V.
    2008 IEEE REGION 10 CONFERENCE: TENCON 2008, VOLS 1-4, 2008, : 473 - +
12345