Temporal verification of Communicating Real-Time State Machines using Uppaal

被引：0
|
作者：
Furfaro, A [1 ]
Nigro, L [1 ]
机构：
[1] Univ Calabria, Lab Ingn Software, Dipartimento Elettron Informat & Sistemist, I-87036 Arcavacata Di Rende, CS, Italy
来源：
2003 IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL TECHNOLOGY, VOLS 1 AND 2, PROCEEDINGS | 2003年
关键词：
D O I：
暂无
中图分类号：
T [工业技术];
学科分类号：
08 ;
摘要：
Communicating Real-Time State Machines (CRSM) are a formal modelling language for the development of distributed real-time systems. This paper proposes a mapping from CRSM to Timed Automata in the context of the Uppaal tool, with the purpose of enabling temporal validation and verification activities respectively based on simulation and model checking of a CRSM system. Usefulness and limitations of the mapping process are demonstrated through the verification of a real-time modelling example.
引用
收藏
页码：399 / 404
页数：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] Using Uppaal for Verification of Priority Assignment in Real-Time Databases
    Kot, Martin
    [J]. DIGITAL INFORMATION PROCESSING AND COMMUNICATIONS, PT 2, 2011, 189 : 385 - 399
  • [6] Scenario-based verification of real-time systems using Uppaal
    Li, Shuhao
    Balaguer, Sandie
    David, Alexandre
    Larsen, Kim G.
    Nielsen, Brian
    Pusinskas, Saulius
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2010, 37 (2-3) : 200 - 264
  • [7] Scenario-based verification of real-time systems using Uppaal
    Shuhao Li
    Sandie Balaguer
    Alexandre David
    Kim G. Larsen
    Brian Nielsen
    Saulius Pusinskas
    [J]. Formal Methods in System Design, 2010, 37 : 200 - 264
  • [8] Prototyping distributed multimedia systems using communicating real-time state machines
    Fortino, G
    Nigro, L
    [J]. EUROMICRO RTS 2000: 12TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS, PROCEEDINGS, 2000, : 273 - 280
  • [9] Model checking hierarchical communicating Real-Time State Machines
    Furfaro, Angelo
    Nigro, Libero
    [J]. ETFA 2005: 10th IEEE International Conference on Emerging Technologies and Factory Automation, Vol 1, Pts 1 and 2, Proceedings, 2005, : 365 - 370
  • [10] MULTICAST CONGESTION CONTROL SRMSH APPROACH USING COMMUNICATING REAL-TIME STATE MACHINES
    Bonastre, O. M.
    Neville, S.
    Palau, C. E.
    [J]. INTERNATIONAL JOURNAL OF BIFURCATION AND CHAOS, 2010, 20 (09): : 2965 - 2973
12345