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
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2008年 / 223卷 / 0C期
关键词：
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 条
  • [1] AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
    Andre, Etienne
    Chatain, Thomas
    Fribourg, Laurent
    Encrenaz, Emmanuelle
    INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2009, 20 (05) : 819 - 836
  • [2] 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
  • [3] An extension of the inverse method to probabilistic timed automata
    Étienne André
    Laurent Fribourg
    Jeremy Sproston
    Formal Methods in System Design, 2013, 42 : 119 - 145
  • [4] Parametric Updates in Parametric Timed Automata
    Andre, Etienne
    Lime, Didier
    Ramparison, Mathias
    FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS (FORTE 2019), 2019, 11535 : 39 - 56
  • [5] PARAMETRIC UPDATES IN PARAMETRIC TIMED AUTOMATA
    Andre, Etienne
    Lime, Didier
    Ramparison, Mathias
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (02) : 1 - 13
  • [6] On the Expressiveness of Parametric Timed Automata
    Andre, Etienne
    Lime, Didier
    Roux, Olivier H.
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2016, 2016, 9884 : 19 - 34
  • [7] Timed automata with parametric updates
    Andre, Etienne
    Lime, Didier
    Ramparison, Mathias
    2018 18TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD), 2018, : 21 - 29
  • [8] Parametric Interrupt Timed Automata
    Berard, Beatrice
    Haddad, Serge
    Jovanovic, Aleksandra
    Lime, Didier
    REACHABILITY PROBLEMS, 2013, 8169 : 59 - 69
  • [9] Zone extrapolations in parametric timed automata
    Arcile, Johan
    Andre, Etienne
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2024,
  • [10] Zone Extrapolations in Parametric Timed Automata
    Arcile, Johan
    Andre, Etienne
    NASA FORMAL METHODS (NFM 2022), 2022, 13260 : 451 - 469
12345