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 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
  • [2] PARAMETRIC UPDATES IN PARAMETRIC TIMED AUTOMATA
    Andre, Etienne
    Lime, Didier
    Ramparison, Mathias
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (02) : 13:1 - 13:67
  • [3] Parametric Interrupt Timed Automata
    Berard, Beatrice
    Haddad, Serge
    Jovanovic, Aleksandra
    Lime, Didier
    REACHABILITY PROBLEMS, 2013, 8169 : 59 - 69
  • [4] 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
  • [5] Control synthesis for parametric timed automata under reachability
    Gol, Ebru A. Y. D. I. N.
    TURKISH JOURNAL OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCES, 2021, 29 (03) : 1751 - 1764
  • [6] Robust parametric reachability for timed automata
    Doyen, Laurent
    INFORMATION PROCESSING LETTERS, 2007, 102 (05) : 208 - 213
  • [7] Durations and parametric model-checking in timed automata
    Bruyere, Veronique
    Dall'olio, Emmanuel
    Raskin, Jean-Francois
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2008, 9 (02)
  • [8] Timed verification of the generic architecture of a memory circuit using parametric timed automata
    Chevallier, Remy
    Encrenaz-Tiphene, Emmanuelle
    Fribourg, Laurent
    Xu, Weiwen
    FORMAL METHODS IN SYSTEM DESIGN, 2009, 34 (01) : 59 - 81
  • [9] Parametric Verification and Test Coverage for Hybrid Automata Using the Inverse Method
    Fribourg, Laurent
    Kuehne, Ulrich
    REACHABILITY PROBLEMS, 2011, 6945 : 191 - +
  • [10] Layered and Collecting NDFS with Subsumption for Parametric Timed Automata
    Hoang Gia Nguyen
    Petrucci, Laure
    van de Pol, Jaco
    2018 23RD INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS), 2018, : 1 - 9
12345