Model checking hierarchical communicating Real-Time State Machines

被引：0
|
作者：
Furfaro, Angelo [1 ]
Nigro, Libero [1 ]
机构：
[1] Univ Calabria, Dipartimento Elettron Informat & Sistemist, I-87036 Arcavacata Di Rende, CS, Italy
来源：
ETFA 2005: 10th IEEE International Conference on Emerging Technologies and Factory Automation, Vol 1, Pts 1 and 2, Proceedings | 2005年
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Hierarchical Communicating Real-Time State Machines (H-CRSM) is a formal modelling language for the modular development of distributed real-time systems. The formalism is characterized by the rise of state transitions with guarded commands and timing constraints, the adoption of a few distilled statecharts constructs, and the modular specification of timing constraints along a state hierarchy. This paper proposes a translation of H-CRSM into UPPAAL which enables model checking. Translation rests on unfolding a hierarchical model on a flat representation.
引用
收藏
页码：365 / 370
页数：6
相关论文
共 50 条
  • [1] Timed verification of hierarchical communicating real-time state machines
    Furfaro, Angelo
    Nigro, Libero
    [J]. COMPUTER STANDARDS & INTERFACES, 2007, 29 (06) : 635 - 646
  • [2] COMMUNICATING REAL-TIME STATE MACHINES
    SHAW, AC
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1992, 18 (09) : 805 - 816
  • [3] Modular design of real-time systems using hierarchical communicating real-time state machines
    Furfaro, A
    Nigro, L
    Pupo, F
    [J]. REAL-TIME SYSTEMS, 2006, 32 (1-2) : 105 - 123
  • [4] Modular Design of Real-Time Systems Using Hierarchical Communicating Real-time State Machines
    Angelo Furfaro
    Libero Nigro
    Francesco Pupo
    [J]. Real-Time Systems, 2006, 32 : 105 - 123
  • [5] A PROTOTYPING ENVIRONMENT FOR SPECIFYING, EXECUTING AND CHECKING COMMUNICATING REAL-TIME STATE MACHINES
    RAJU, SCV
    SHAW, AC
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 1994, 24 (02): : 175 - 195
  • [6] Structural model checking for communicating hierarchical machines
    Lanotte, R
    Maggiolo-Schettini, A
    Peron, A
    [J]. MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2004, PROCEEDINGS, 2004, 3153 : 525 - 536
  • [7] Model checking of hierarchical state machines
    Alur, R
    Yannakakis, M
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001, 23 (03): : 273 - 303
  • [8] Model Checking Process Algebra of Communicating Resources for Real-time Systems
    Boudjadar, A. Jalil
    Kim, Jin Hyun
    Larsen, Kim G.
    Nyman, Ulrik
    [J]. 2014 26TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS (ECRTS 2014), 2014, : 51 - 60
  • [9] Supporting communicating real-time state machines by a customisable actor kernel
    Fortino, G
    Nigro, L
    Pupo, F
    [J]. REAL TIME PROGRAMMING 1999 (WRTP'99), 1999, : 117 - 122
  • [10] Model checking of unrestricted hierarchical state machines
    Benedikt, M
    Godefroid, P
    Reps, T
    [J]. AUTOMATA LANGUAGES AND PROGRAMMING, PROCEEDING, 2001, 2076 : 652 - 666
12345