An Inverse Method for Parametric Timed Automata

被引:6
|
作者
Andre, Etienne [1 ]
Chatain, Thomas [1 ]
Fribourg, Laurent [1 ]
Encrenaz, Emmanuelle [1 ]
机构
[1] Univ Paris 06, CNRS, Paris, France
关键词
Timed automata; parameters; verification; asynchronous circuits;
D O I
10.1016/j.entcs.2008.12.029
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Given a timed automaton with parametric timings, our objective is to describe a procedure for deriving constraints on the parametric timings in order to ensure that, for each value of parameters satisfying these constraints, the behaviors of the timed automata are time-abstract equivalent. We will exploit a reference valuation of the parameters that is supposed to capture a characteristic proper behavior of the system. The method has been implemented and is illustrated on various examples of asynchronous circuits.
引用
收藏
页码:29 / 46
页数:18
相关论文
共 50 条
  • [41] Interrupt Timed Automata
    Berard, Beatrice
    Haddad, Serge
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2009, 5504 : 197 - +
  • [42] 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
  • [43] Alternating timed automata
    Lasota, Slawomir
    Walukiewicz, Igor
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2008, 9 (02)
  • [44] Timed automata and recognizability
    Hermann, P
    INFORMATION PROCESSING LETTERS, 1998, 65 (06) : 313 - 318
  • [45] Timed Automata Patterns
    Dong, Jin Song
    Hao, Ping
    Qin, Shengchao
    Sun, Jun
    Yi, Wang
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2008, 34 (06) : 844 - 859
  • [46] Scheduling with timed automata
    Abdeddaïm, Y
    Asarin, E
    Maler, O
    THEORETICAL COMPUTER SCIENCE, 2006, 354 (02) : 272 - 300
  • [47] Diagnosing timed automata using timed markings
    Bouyer, Patricia
    Henry, Leo
    Jaziri, Samy
    Jeron, Thierry
    Markey, Nicolas
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2021, 23 (02) : 229 - 253
  • [48] Diagnosing timed automata using timed markings
    Patricia Bouyer
    Léo Henry
    Samy Jaziri
    Thierry Jéron
    Nicolas Markey
    International Journal on Software Tools for Technology Transfer, 2021, 23 : 229 - 253
  • [49] Distributed parametric model checking timed automata under non-Zenoness assumption
    Andre, Etienne
    Hoang Gia Nguyen
    Petrucci, Laure
    Sun, Jun
    FORMAL METHODS IN SYSTEM DESIGN, 2021, 59 (1-3) : 253 - 290
  • [50] Guaranteeing Timed Opacity using Parametric Timed Model Checking
    Andre, Etienne
    Lime, Didier
    Marinho, Dylan
    Sun, Jun
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2022, 31 (04)