Timed-automata semantics and analysis of UML/SPT models with coneurrency

被引:0
|
作者
Gherbi, Abdelouahed [1 ]
Khendek, Ferhat [1 ]
机构
[1] Concordia Univ, Dept Elect & Comp Engn, 1455 Maisonneuve Blvd W, Montreal, PQ H3G 1M8, Canada
基金
加拿大自然科学与工程研究理事会;
关键词
D O I
10.1109/ISORC.2007.57
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
UML can be effectively used for the design and analysis of real-time systems. UML profiles for real-time, like the current OMG's standard UML/SPT enable the modeling of quantitative requirements such as time constraints as well as behavioral features such as concurrency. Because of the multitude of diagrams and their complexity, UML/SPT models face the challenging issue of consistency. In this paper we look into the behavioral consistency and particularly into concurrency-related properties of UML/SPT models. In order to do so, we formally define the UML/SPT concurrency domain model in terms of timed automata. As a straightforward application of this semantics, UML/SPT concurrent models can be validated using well-established model checking techniques and tools.
引用
收藏
页码:412 / +
页数:2
相关论文
共 50 条
  • [41] Semantics-driven extraction of timed automata from Java programs
    Giovanni Liva
    Muhammad Taimoor Khan
    Martin Pinzger
    [J]. Empirical Software Engineering, 2019, 24 : 3114 - 3150
  • [42] Timed Automata Semantics of Spatial-Temporal Consistency Language STeC
    Zhang, Yuanrui
    Mallet, Frederic
    Chen, Yixiang
    [J]. 2014 THEORETICAL ASPECTS OF SOFTWARE ENGINEERING CONFERENCE (TASE), 2014, : 201 - 208
  • [43] Towards a BPMN Semantics Using UML Models
    Nicolae, Oana
    Cosulschi, Mirel
    Giurca, Adrian
    Wagner, Gerd
    [J]. BUSINESS PROCESS MANAGEMENT WORKSHOPS, 2009, 17 : 585 - +
  • [44] A partial order semantics approach to the clock explosion problem of timed automata
    Lugiez, D
    Niebert, P
    Zennou, S
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 296 - 311
  • [45] Automata semantics and analysis of BPEL
    Zheng, Yongyan
    Krause, Paul
    [J]. 2007 INAUGURAL IEEE INTERNATIONAL CONFERENCE ON DIGITAL ECOSYSTEMS AND TECHNOLOGIES, 2007, : 307 - +
  • [46] Forward analysis of updatable timed automata
    Bouyer, P
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2004, 24 (03) : 281 - 320
  • [47] Distributed reachability analysis in timed automata
    Behrmann G.
    [J]. International Journal on Software Tools for Technology Transfer, 2005, 7 (1) : 19 - 30
  • [48] Diagonal constraints in timed automata: Forward analysis of timed systems
    Bouyer, P
    Laroussinie, F
    Reynier, PA
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2005, 3829 : 112 - 126
  • [49] Symbolic robustness analysis of timed automata
    Daws, Conrado
    Kordy, Piotr
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2006, 4202 : 143 - 155
  • [50] Approximate reachability analysis of timed automata
    Balarin, F
    [J]. 17TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1996, : 52 - 61