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 条
  • [41] Verification of RabbitMQ with Kerberos Using Timed Automata
    Ran Li
    Jiaqi Yin
    Huibiao Zhu
    Phan Cong Vinh
    Mobile Networks and Applications, 2022, 27 : 2049 - 2067
  • [42] PROBABILITY TIMED AUTOMATA FOR INVESTIGATING COMMUNICATION PROCESSES
    Piech, Henryk
    Grodzki, Grzegorz
    INTERNATIONAL JOURNAL OF APPLIED MATHEMATICS AND COMPUTER SCIENCE, 2015, 25 (02) : 403 - 414
  • [43] Linear parametric model checking of timed automata
    Hune, T
    Romijn, J
    Stoelinga, M
    Vaandrager, F
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2002, 52-3 : 183 - 220
  • [44] Polynomial interrupt timed automata: Verification and expressiveness
    Berard, B.
    Haddad, S.
    Picaronny, C.
    El Din, M. Safey
    Sassolas, M.
    INFORMATION AND COMPUTATION, 2021, 277
  • [45] Symbolic model checking for probabilistic timed automata
    Kwiatkowska, Marta
    Norman, Gethin
    Sproston, Jeremy
    Wang, Fuzhi
    INFORMATION AND COMPUTATION, 2007, 205 (07) : 1027 - 1077
  • [46] Verification of continuous dynamical systems by timed automata
    Sloth, Christoffer
    Wisniewski, Rafael
    FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (01) : 47 - 82
  • [47] Web Service Composition Automation based on Timed Automata
    Hu Jingjing
    Zhu Wei
    Zhao Xing
    Zhu Dongfeng
    APPLIED MATHEMATICS & INFORMATION SCIENCES, 2014, 8 (04): : 2017 - 2024
  • [48] Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
    D'Argenio, Pedro R.
    Hartmanns, Arnd
    Legay, Axel
    Sedwards, Sean
    INTEGRATED FORMAL METHODS (IFM 2016), 2016, 9681 : 99 - 114
  • [49] Verifying Simulink Stateflow Model: Timed Automata Approach
    Yang, Yixiao
    Jiang, Yu
    Gu, Ming
    Sun, Jiaguang
    2016 31ST IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2016, : 852 - 857
  • [50] Parametric Deadlock-Freeness Checking Timed Automata
    Andre, Etienne
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2016, 2016, 9965 : 469 - 478