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
关键词
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] Timed automata
    Alur, R
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 233 - 264
  • [3] A Compositional Translation of Timed Automata with Deadlines to UPPAAL Timed Automata
    Gomez, Rodolfo
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2009, 5813 : 179 - 194
  • [4] Timed unfoldings for networks of timed automata
    Bouyer, Patricia
    Haddad, Serge
    Reynier, Pierre-Alain
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2006, 4218 : 292 - 306
  • [5] Timed patterns: TCOZ to timed automata
    Dong, JS
    Hao, P
    Qin, SC
    Sun, J
    Yi, W
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2004, 3308 : 483 - 498
  • [6] Axiomatising timed automata
    Huimin Lin
    Wang Yi
    Acta Informatica, 2002, 38 : 277 - 305
  • [7] Updatable timed automata
    Bouyer, P
    Dufourd, C
    Fleury, E
    Petit, A
    THEORETICAL COMPUTER SCIENCE, 2004, 321 (2-3) : 291 - 345
  • [8] Robust timed automata
    Gupta, V
    Henzinger, TA
    Jagadeesan, R
    HYBRID AND REAL-TIME SYSTEMS, 1997, 1201 : 331 - 345
  • [9] THE THEORY OF TIMED AUTOMATA
    ALUR, R
    DILL, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 600 : 45 - 73
  • [10] On interleaving in timed automata
    Ben Salah, Ramzi
    Bozga, Marius
    Maler, Oded
    CONCUR 2006 - CONCURRENCY THEORY, PROCEEDINGS, 2006, 4137 : 465 - 476