Methods of checking general safety criteria in UML statechart specifications

被引:15
|
作者
Pap, Z [1 ]
Majzik, I [1 ]
Pataricza, A [1 ]
Szegi, A [1 ]
机构
[1] Tech Univ Budapest, Dept Measurement & Informat Syst, H-1117 Budapest, Hungary
关键词
system safety; software specification; safety criteria; UML statecharts; OCL; graph transformation; reachability analysis;
D O I
10.1016/j.ress.2004.04.011
中图分类号
T [工业技术];
学科分类号
08 ;
摘要
This paper describes methods and tools for safety analysis of UML statechart specifications. A comprehensive set of general safety criteria including completeness and consistency is applied in automated analysis. Analysis techniques are based on OCL expressions, graph transformations and reachability analysis. Two canonical intermediate representations of the statechart specification are introduced. They are suitable for straightforward implementation of checker methods and for the support of the proof of the correctness and soundness of the applied analysis. One of them also serves as a basis of the metamodel of a variant of UML statecharts proposed for the specification of safety-critical control systems. The analysis is extended to object-oriented specifications. Examples illustrate the application of the checker methods implemented by an automated tool-set. (C) 2004 Elsevier Ltd. All rights reserved.
引用
收藏
页码:89 / 107
页数:19
相关论文
共 50 条
  • [21] Towards a Wide Acceptance of Formal Methods to the Design of Safety Critical Software: An Approach Based on UML and Model Checking
    Eras, Eduardo Rohde
    Rebelo dos Santos, Luciana Brasil
    de Santiago Junior, Valdivino Alexandre
    Vijaykumar, Nandamudi Lankalapalli
    COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2015, PT IV, 2015, 9158 : 612 - 627
  • [22] Using abstraction and model checking to detect safety violations in requirements specifications
    Heitmeyer, C
    Kirby, J
    Labaw, B
    Archer, M
    Bharadwaj, R
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (11) : 927 - 948
  • [23] A safety shell for UML-RT projects structure and methods of the corresponding UML pattern
    Gumzej, Roman
    Halang, Wolfgang A.
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2009, 5 (02) : 97 - 105
  • [24] General safety criteria for the Korean next generation reactor
    Lee, JH
    Kim, WS
    Yune, YG
    Lee, JS
    NUCLEAR TECHNOLOGY, 2002, 139 (01) : 36 - 41
  • [25] UTILIZATION OF STATISTICAL CRITERIA FOR STANDARDIZING METHODS OF CHECKING METAL-TESTING MACHINES
    ZOTEEV, VS
    SMUSHKOV.BL
    MEASUREMENT TECHNIQUES-USSR, 1968, (11): : 1462 - &
  • [26] Suggested Methods for Rock Failure Criteria: General Introduction
    Ulusay, R.
    Hudson, J. A.
    ROCK MECHANICS AND ROCK ENGINEERING, 2012, 45 (06) : 971 - 971
  • [27] Suggested Methods for Rock Failure Criteria: General Introduction
    R. Ulusay
    J. A. Hudson
    Rock Mechanics and Rock Engineering, 2012, 45 : 971 - 971
  • [28] Lifing methods and safety criteria in aero gas turbines
    Corran, R. S. J.
    Williams, S. J.
    ENGINEERING FAILURE ANALYSIS, 2007, 14 (03) : 518 - 528
  • [29] Applying infinite state model checking and other analysis techniques to tabular requirements specifications of safety-critical systems
    Tevfik Bultan
    Constance Heitmeyer
    Design Automation for Embedded Systems, 2008, 12 : 97 - 137
  • [30] Applying infinite state model checking and other analysis techniques to tabular requirements specifications of safety-critical systems
    Bultan, Tevfik
    Heitmeyer, Constance
    DESIGN AUTOMATION FOR EMBEDDED SYSTEMS, 2008, 12 (1-2) : 97 - 137