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 条
  • [31] Quantitative Robustness Analysis of Flat Timed Automata
    Jaubert, Remi
    Reynier, Pierre-Alain
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, 2011, 6604 : 229 - +
  • [32] Languages of Higher-Dimensional Timed Automata
    Amrane, Amazigh
    Bazille, Hugo
    Clement, Emily
    Fahrenberg, Uli
    APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2024, 2024, 14628 : 197 - 219
  • [33] Interrupt Timed Automata with Auxiliary Clocks and Parameters
    Berard, Beatrice
    Haddad, Serge
    Jovanovic, Aleksandra
    Lime, Didier
    FUNDAMENTA INFORMATICAE, 2016, 143 (3-4) : 235 - 259
  • [34] A Conformance Testing Relation for Symbolic Timed Automata
    von Styp, Sabrina
    Bohnenkamp, Henrik
    Schmaltz, Julien
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2010, 6246 : 243 - +
  • [35] Verification of RabbitMQ with Kerberos Using Timed Automata
    Li, Ran
    Yin, Jiaqi
    Zhu, Huibiao
    Phan Cong Vinh
    MOBILE NETWORKS & APPLICATIONS, 2022, 27 (05) : 2049 - 2067
  • [36] Asynchronous multi-process timed automata
    Li, Guoqiang
    Liu, Li
    Fukuda, Akira
    SOFTWARE QUALITY JOURNAL, 2018, 26 (03) : 961 - 989
  • [37] Computing Bisimilarity Metrics for Probabilistic Timed Automata
    Lanotte, Ruggero
    Tini, Simone
    INTEGRATED FORMAL METHODS, IFM 2019, 2019, 11918 : 303 - 321
  • [38] An extension of the inverse method to probabilistic timed automata
    Andre, Etienne
    Fribourg, Laurent
    Sproston, Jeremy
    FORMAL METHODS IN SYSTEM DESIGN, 2013, 42 (02) : 119 - 145
  • [39] Analyzing an Embedded Sensor with Timed Automata in Uppaal
    Bourke, Timothy
    Sowmya, Arcot
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2013, 13 (03)
  • [40] Complete abstractions of dynamical systems by timed automata
    Sloth, Christoffer
    Wisniewski, Rafael
    NONLINEAR ANALYSIS-HYBRID SYSTEMS, 2013, 7 (01) : 80 - 100