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 条
  • [1] Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata
    Yu Zhou
    Luciano Baresi
    Matteo Rossi
    [J]. Journal of Computer Science and Technology, 2013, 28 : 188 - 202
  • [2] Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata
    周宇
    Luciano Baresi
    Matteo Rossi
    [J]. Journal of Computer Science & Technology, 2013, 28 (01) : 188 - 202
  • [3] TOWARDS A TRANSFORMATION APPROACH OF TIMED UML MARTE SPECIFICATIONS FOR OBSERVER-BASED FORMAL VERIFICATION
    Menad, Nadia
    Dhaussy, Philippe
    Drey, Zoe
    Mekki, Rachida
    [J]. COMPUTING AND INFORMATICS, 2016, 35 (02) : 338 - 368
  • [4] UML 2.0 state machines:: Complete formal semantics via core state machines
    Fecher, Harald
    Schoenborn, Jens
    [J]. FORMAL METHODS: APPLICATIONS AND TECHNOLOGY, 2007, 4346 : 244 - +
  • [5] Towards a new formal SDL semantics based on abstract state machines
    Glässer, U
    Gotzhein, R
    Prinz, A
    [J]. SDL'99: THE NEXT MILLENNIUM, 1999, : 171 - 190
  • [6] Dependability analysis of DES based on MARTE and UML state machines models
    José Merseguer
    Simona Bernardi
    [J]. Discrete Event Dynamic Systems, 2012, 22 : 163 - 178
  • [7] Dependability analysis of DES based on MARTE and UML state machines models
    Merseguer, Jose
    Bernardi, Simona
    [J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2012, 22 (02): : 163 - 178
  • [8] A timed automata semantics for real-time UML specifications
    Toetenel, H
    Roubtsova, E
    van Katwijk, J
    [J]. IEEE SYMPOSIA ON HUMAN-CENTRIC COMPUTING LANGUAGES AND ENVIRONMENTS, PROCEEDINGS, 2001, : 88 - 95
  • [9] A formal semantics of UML StateCharts by means of timed Petri Nets
    Hammal, Y
    [J]. FORMAL TECHNIQUES FOR NEWTOWRKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 38 - 52
  • [10] Timed-automata semantics and analysis of UML/SPT models with coneurrency
    Gherbi, Abdelouahed
    Khendek, Ferhat
    [J]. 10TH IEEE INTERNATIONAL SYMPOSIUM ON OBJECT AND COMPONENT-ORIENTED REAL-TIME DISTRIBUTED COMPUTING, PROCEEDINGS, 2007, : 412 - +
12345