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 条
  • [1] Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata
    Zhou, Yu
    Baresi, Luciano
    Rossi, Matteo
    JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2013, 28 (01) : 188 - 202
  • [2] Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata
    Yu Zhou
    Luciano Baresi
    Matteo Rossi
    Journal of Computer Science and Technology, 2013, 28 : 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
    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
    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
    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
    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
    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
    IEEE SYMPOSIA ON HUMAN-CENTRIC COMPUTING LANGUAGES AND ENVIRONMENTS, PROCEEDINGS, 2001, : 88 - 95
  • [9] A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods Verification
    Ferreira, Diego
    Lima, Lucas
    FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2024, 2025, 15403 : 49 - 67
  • [10] A formal semantics of UML StateCharts by means of timed Petri Nets
    Hammal, Y
    FORMAL TECHNIQUES FOR NEWTOWRKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 38 - 52
12345