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 条
  • [41] THE REAL-TIME VERIFICATION
    PELTOLA, S
    [J]. MEDICAL PHYSICS, 1988, 15 (05) : 799 - 799
  • [42] Hazard Analysis of Real-time Safety Critical Systems using Hierarchical Communication Real-Time State Machines Formal Model
    Bakr, Ahmed M.
    Fouda, Mostafa M.
    Salama, May
    Alsammak, Abdelwahab K.
    Yahia, Hossam
    [J]. 2017 12TH INTERNATIONAL CONFERENCE ON COMPUTER ENGINEERING AND SYSTEMS (ICCES), 2017, : 628 - 634
  • [43] Verification of well-formed communicating recursive state machines
    Bozzelli, L
    La Torre, S
    Peron, A
    [J]. VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 412 - 426
  • [44] Verification of well-formed communicating recursive state machines
    Bozzelli, Laura
    La Torre, Salvatore
    Peron, Adriano
    [J]. THEORETICAL COMPUTER SCIENCE, 2008, 403 (2-3) : 382 - 405
  • [45] REAL-TIME STATE IDENTIFICATION OF BOILING WATER REACTORS USING RELEVANCE VECTOR MACHINES
    Alamaniotis, Miltiadis
    Cappelli, Mauro
    [J]. PROCEEDINGS OF THE 24TH INTERNATIONAL CONFERENCE ON NUCLEAR ENGINEERING, 2016, VOL 1, 2016,
  • [46] Stability of Real-Time Abstract State Machines under Desynchronization
    Cohen, J.
    Slissenko, A.
    [J]. ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, 2008, 5238 : 341 - 341
  • [47] Temporal Properties Verification of Real-Time Systems Using UML/MARTE/OCL-RT
    Louati, Aymen
    Barkaoui, Kamel
    Jerad, Chadlia
    [J]. FORMALISMS FOR REUSE AND SYSTEMS INTEGRATION, 2015, 346 : 133 - 147
  • [48] State structures for verification and real-time control of hybrid automata
    OYoung, S
    Raisch, J
    [J]. 1997 CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, CONFERENCE PROCEEDINGS, VOLS I AND II: ENGINEERING INNOVATION: VOYAGE OF DISCOVERY, 1997, : 395 - 398
  • [49] Towards the Verification of Temporal Data Consistency in Real-Time Data Management
    Cai, Simin
    Gallina, Barbara
    Nystrom, Dag
    Seceleanu, Cristina
    [J]. 2016 2ND INTERNATIONAL WORKSHOP ON MODELLING, ANALYSIS, AND CONTROL OF COMPLEX CPS (CPS DATA), 2016,
  • [50] Real-time hardware specification and verification by using MVC
    Li, XS
    Wang, JA
    [J]. NEW TECHNOLOGIES ON COMPUTER SOFTWARE, 1997, : 18 - 23
12345