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 条
  • [41] Formal Verification of Python']Python Software Transactional Memory Based on Timed Automata
    Kordic, Branislav
    Popovic, Miroslav
    Ghilezan, Silvia
    ACTA POLYTECHNICA HUNGARICA, 2019, 16 (07) : 197 - 216
  • [42] Towards formal verification of UML diagrams based on graph transformation
    Zhao, Y
    Fan, YS
    Bai, XM
    Wang, Y
    Cai, H
    Ding, W
    PROCEEDINGS OF THE IEEE INTERNATIONAL CONFERENCE ON E-COMMERCE TECHNOLOGY FOR DYNAMIC E-BUSINESS, 2004, : 180 - 187
  • [43] A software development process based on UML state machines
    Cariou, Eric
    Brunschwig, Lea
    Le Goaer, Olivier
    Barbier, Franck
    2020 4TH INTERNATIONAL CONFERENCE ON ADVANCED ASPECTS OF SOFTWARE ENGINEERING (ICAASE'2020): 4TH INTERNATIONAL CONFERENCE ON ADVANCED ASPECTS OF SOFTWARE ENGINEERING, 2020, : 23 - 30
  • [44] A UML validation toolset based on Abstract State Machines
    Shen, WW
    Compton, K
    Huggins, J
    16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 315 - 318
  • [45] Formal Modeling and analysis of scientific workflows using hierarchical state machines
    Yang, Ping
    Yang, Zijiang
    Lu, Shiyong
    E-SCIENCE 2007: THIRD IEEE INTERNATIONAL CONFERENCE ON E-SCIENCE AND GRID COMPUTING, PROCEEDINGS, 2007, : 619 - +
  • [46] Formal Validation for Natural Language Programming using Hierarchical Finite State Automata
    Zhan, Yue
    Hsiao, Michael S.
    ICAART: PROCEEDINGS OF THE 13TH INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE - VOL 1, 2021, : 506 - 515
  • [47] A formal semantics of extended hierarchical state transition matrices using CSP#
    Yamagata, Yoriyuki
    Kong, Weiqiang
    Fukuda, Akira
    Nguyen Van Tang
    Ohsaki, Hitoshi
    Taguchi, Kenji
    FORMAL ASPECTS OF COMPUTING, 2014, 26 (05) : 943 - 962
  • [48] Formal Verification of ROS-based Robotic Applications using Timed-Automata
    Halder, Raju
    Proenca, Jose
    Macedo, Nuno
    Santos, Andre
    2017 IEEE/ACM 5TH INTERNATIONAL FME WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE) PROCEEDINGS, 2017, : 44 - 50
  • [49] Formal Analysis of Security Properties of Cyber-physical System Based on Timed Automata
    Wang, Ting
    Su, Qi
    Chen, Tieming
    2017 IEEE SECOND INTERNATIONAL CONFERENCE ON DATA SCIENCE IN CYBERSPACE (DSC), 2017, : 534 - 540
  • [50] Towards a Formal Semantics-Based Technique for Interprocedural Slicing
    Asavoae, Irina Mariuca
    Asavoae, Mihail
    Riesco, Adrian
    INTEGRATED FORMAL METHODS, IFM 2014, 2014, 8739 : 291 - 306
12345