Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata

被引：7
|
作者：
周宇
Luciano Baresi
Matteo Rossi
机构：
[1] College of Computer Science,Nanjing University of Aeronautics and Astronautics
[2] State Key Laboratory for Novel Software Technology,Nanjing University
[3] Department of Electronics and Information,Politecnico di Milano
来源：
Journal of Computer Science & Technology | 2013年 / 28卷 / 01期
基金：
中国国家自然科学基金;
关键词：
timed automata; state machine diagram; formal semantics;
D O I：
暂无
中图分类号：
TP391.1 [文字信息处理];
学科分类号：
摘要：
UML is a widely-used,general purpose modeling language.But its lack of a rigorous semantics forbids the thorough analysis of designed solution,and thus precludes the discovery of significant problems at design time.To bridge the gap,the paper investigates the underlying semantics of UML state machine diagrams,along with the time-related modeling elements of MARTE,the profile for modeling and analysis of real-time embedded systems,and proposes a formal operational semantics based on extended hierarchical timed automata.The approach is exemplified on a simple example taken from the automotive domain.Verification is accomplished by translating designed models into the input language of the UPPAAL model checker.
引用
收藏
页码：188 / 202
页数：15
相关论文
共 50 条
  • [21] Formal Verification of Sequence Diagram with State Invariants Using Timed Automata
    Thitareedechakul, Supapitch S.
    Vatanawood, Wiwat
    PROCEEDINGS OF THE 20TH INTERNATIONAL CONFERENCE ON COMPUTING AND INFORMATION TECHNOLOGY, IC2IT 2024, 2024, 973 : 43 - 54
  • [22] Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model
    Chabbat N.
    Saidouni D.E.
    Boukharrou R.
    Ghanemi S.
    Computing and Informatics, 2021, 39 (05) : 1022 - 1060
  • [23] FORMAL VERIFICATION OF UML MARTE SPECIFICATIONS BASED ON A TRUE CONCURRENCY REAL TIME MODEL
    Chabbat, Nadia
    Saidouni, Djamel Eddine
    Boukharrou, Radja
    Ghanemi, Salim
    COMPUTING AND INFORMATICS, 2020, 39 (05) : 1022 - 1060
  • [24] Formal verification of multitasking applications based on timed automata model
    Libor Waszniowski
    Zdeněk Hanzálek
    Real-Time Systems, 2008, 38 : 39 - 65
  • [25] Formal verification of multitasking applications based on timed automata model
    Waszniowski, Libor
    Hanzalek, Zdenek
    REAL-TIME SYSTEMS, 2008, 38 (01) : 39 - 65
  • [26] Mappings, maps and tables: Towards formal semantics for associations in UML2
    Diskin, Zinovy
    Dingel, Juergen
    MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2006, 4199 : 230 - 244
  • [27] Towards Checking Parametric Reachability for UML State Machines
    Niewiadomski, Artur
    Penczek, Wojciech
    Szreter, Maciej
    PERSPECTIVES OF SYSTEMS INFORMATICS, 2010, 5947 : 319 - +
  • [28] Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata
    Alves, Gleifer Vaz
    Schwammberger, Maike
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (371): : 77 - 85
  • [29] Refinement Sensitive Formal Semantics of State Machines With Persistent Choice
    Fecher, Harald
    Huth, Michael
    Schmidt, Heiko
    Schoenborn, Jens
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 250 (01) : 71 - 86
  • [30] Towards Early Performance Assessment Based on UML MARTE Models for Distributed Systems
    Chise, C.
    Jurca, I.
    SACI: 2009 5TH INTERNATIONAL SYMPOSIUM ON APPLIED COMPUTATIONAL INTELLIGENCE AND INFORMATICS, 2009, : 511 - 516
12345