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

被引：9
|
作者：
Zhou, Yu [1 ,2 ]
Baresi, Luciano [3 ]
Rossi, Matteo [3 ]
机构：
[1] Nanjing Univ Aeronaut & Astronaut, Coll Comp Sci, Nanjing 210016, Peoples R China
[2] Nanjing Univ, State Key Lab Novel Software Technol, Nanjing 210093, Jiangsu, Peoples R China
[3] Politecn Milan, Dept Elect & Informat, I-20133 Milan, Italy
来源：
JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY | 2013年 / 28卷 / 01期
基金：
中国国家自然科学基金;
关键词：
timed automata; state machine diagram; formal semantics;
D O I：
10.1007/s11390-013-1322-8
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
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 条
  • [31] Trace-based semantics for probabilistic timed I/O automata
    Mitra, Sayan
    Lynch, Nancy
    [J]. HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2007, 4416 : 718 - +
  • [32] Towards an integrated graph-based semantics for UML
    Kuske, Sabine
    Gogolla, Martin
    Kreowski, Hans-Joerg
    Ziemann, Paul
    [J]. SOFTWARE AND SYSTEMS MODELING, 2009, 8 (03): : 403 - 422
  • [33] Towards an integrated graph-based semantics for UML
    Sabine Kuske
    Martin Gogolla
    Hans-Jörg Kreowski
    Paul Ziemann
    [J]. Software & Systems Modeling, 2009, 8 : 403 - 422
  • [34] To Do or Not to Do: Semantics and Patterns for Do Activities in UML PSSM State Machines
    Elekes, Marton
    Molnar, Vince
    Micskei, Zoltan
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2024, 50 (08) : 2124 - 2141
  • [35] Towards Formal Verification of Behaviour-Driven Development Scenarios using Timed Automata
    Kang, Eun-Young
    Silva, Thiago Rocha
    [J]. PROCEEDINGS OF THE 2023 30TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, APSEC 2023, 2023, : 612 - 616
  • [36] Design of Reconfigurable Logic Controllers from Hierarchical UML State Machines
    Adamski, Marian
    [J]. ICIEA: 2009 4TH IEEE CONFERENCE ON INDUSTRIAL ELECTRONICS AND APPLICATIONS, VOLS 1-6, 2009, : 82 - +
  • [37] Timed verification of hierarchical communicating real-time state machines
    Furfaro, Angelo
    Nigro, Libero
    [J]. COMPUTER STANDARDS & INTERFACES, 2007, 29 (06) : 635 - 646
  • [38] SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata
    Malinowski, Janusz
    Niebert, Peter
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 405 - 419
  • [39] Analysing UML active classes and associated state machines - A lightweight formal approach
    Reggio, G
    Astesiano, E
    Choppy, C
    Hussmann, H
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 2000, 1783 : 127 - 146
  • [40] Formal Verification of Python']Python Software Transactional Memory Based on Timed Automata
    Kordic, Branislav
    Popovic, Miroslav
    Ghilezan, Silvia
    [J]. ACTA POLYTECHNICA HUNGARICA, 2019, 16 (07) : 197 - 216
12345