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 条
  • [21] Abstraction Refinement Algorithms for Timed Automata
    Roussanaly, Victor
    Sankur, Ocan
    Markey, Nicolas
    COMPUTER AIDED VERIFICATION, CAV 2019, PT I, 2019, 11561 : 22 - 40
  • [22] Trace Abstraction Refinement for Timed Automata
    Wang, Weifeng
    Jiao, Li
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2014, 2014, 8837 : 396 - 410
  • [23] Symbolic and Compositional Reachability for Timed Automata
    Larsen, Kim Guldstrand
    REACHABILITY PROBLEMS, 2010, 6227 : 24 - 28
  • [24] Robust parametric reachability for timed automata
    Doyen, Laurent
    INFORMATION PROCESSING LETTERS, 2007, 102 (05) : 208 - 213
  • [25] Abstraction of Dynamical Systems by Timed Automata
    Wisniewski, Rafael
    Sloth, Christoffer
    MODELING IDENTIFICATION AND CONTROL, 2011, 32 (02) : 79 - 90
  • [26] Logics for Weighted Timed Pushdown Automata
    Droste, Manfred
    Perevoshchikov, Vitaly
    FIELDS OF LOGIC AND COMPUTATION II: ESSAYS DEDICATED TO YURI GUREVICH ON THE OCCASION OF HIS 75TH BIRTHDAY, 2015, 9300 : 153 - 173
  • [27] Implementing timed automata specifications: the "sandwich" approach
    Devillers, Raymond
    Didier, Jean-Yves
    Klaudel, Hanna
    2013 13TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD 2013), 2013, : 226 - 235
  • [28] Verification of continuous dynamical systems by timed automata
    Christoffer Sloth
    Rafael Wisniewski
    Formal Methods in System Design, 2011, 39 : 47 - 82
  • [29] Learning Timed Automata from Interaction Traces
    Vain, J.
    Kanter, G.
    Anier, A.
    IFAC PAPERSONLINE, 2019, 52 (19): : 205 - 210
  • [30] Verifying Opacity of Discrete-Timed Automata
    Klein, Julian
    Kogel, Paul
    Glesner, Sabine
    PROCEEDINGS OF THE 2024 IEEE/ACM 12TH INTERNATIONAL CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING, FORMALISE 2024, 2024, : 55 - 65