On Implementable Timed Automata

被引:4
|
作者
Feo-Arenis, Sergio [1 ]
Vujinovic, Milan [2 ]
Westphal, Bernd [2 ]
机构
[1] Airbus Cent R&T, Munich, Germany
[2] Albert Ludwigs Univ Freiburg, Freiburg, Germany
来源
FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2020 | 2020年 / 12136卷
关键词
PROGRAMMING LANGUAGE; VERIFICATION; SEMANTICS;
D O I
10.1007/978-3-030-50086-3_5
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Generating code from networks of timed automata is a well-researched topic with many proposed approaches, which have in common that they not only generate code for the processes in the network, but necessarily generate additional code for a global scheduler which implements the timed automata semantics. For distributed systems without shared memory, this additional component is, in general, undesired. In this work, we present a new approach to the generation of correct code (without global scheduler) for distributed systems without shared memory yet with (almost) synchronous clocks if the source model does not depend on a global scheduler. We characterise a set of implementable timed automata models and provide a translation to a timed while language. We show that each computation of the generated program has a network computation path with the same observable behaviour.
引用
收藏
页码:78 / 95
页数:18
相关论文
共 50 条
  • [1] Timed Automata Can Always Be Made Implementable
    Bouyer, Patricia
    Larsen, Kim G.
    Markey, Nicolas
    Sankur, Ocan
    Thrane, Claus
    CONCUR 2011: CONCURRENCY THEORY, 2011, 6901 : 76 - +
  • [2] STOCHASTIC TIMED AUTOMATA
    Bertrand, Nathalie
    Bouyer, Patricia
    Brihaye, Thomas
    Menet, Quentin
    Baier, Christel
    Groesser, Marcus
    Jurdzinski, Marcin
    LOGICAL METHODS IN COMPUTER SCIENCE, 2014, 10 (04)
  • [3] The Opacity of Timed Automata
    An, Jie
    Gao, Qiang
    Wang, Lingtai
    Zhan, Naijun
    Hasuo, Ichiro
    FORMAL METHODS, PT I, FM 2024, 2025, 14933 : 620 - 637
  • [4] Shrinking timed automata
    Sankur, Ocan
    Bouyer, Patricia
    Markey, Nicolas
    INFORMATION AND COMPUTATION, 2014, 234 : 107 - 132
  • [5] Robustness in Timed Automata
    Bouyer, Patricia
    Markey, Nicolas
    Sankur, Ocan
    REACHABILITY PROBLEMS, 2013, 8169 : 1 - 18
  • [6] Shrinking Timed Automata
    Sankur, Ocan
    Bouyer, Patricia
    Markey, Nicolas
    IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2011), 2011, 13 : 90 - 102
  • [7] Dynamical properties of timed automata
    Puri, A
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2000, 10 (1-2): : 87 - 113
  • [8] Dynamical properties of timed automata
    Puri, A
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1998, 1486 : 210 - 227
  • [9] Behavioral Cartography of Timed Automata
    Andre, Etienne
    Fribourg, Laurent
    REACHABILITY PROBLEMS, 2010, 6227 : 76 - +
  • [10] Dynamical Properties of Timed Automata
    Anuj Puri
    Discrete Event Dynamic Systems, 2000, 10 : 87 - 113