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 条
  • [31] 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
  • [32] PARAMETRIC VERIFICATION AND TEST COVERAGE FOR HYBRID AUTOMATA USING THE INVERSE METHOD
    Fribourg, Laurent
    Kuehne, Ulrich
    INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2013, 24 (02) : 233 - 249
  • [33] Parametric Verification and Test Coverage for Hybrid Automata Using the Inverse Method
    Fribourg, Laurent
    Kuehne, Ulrich
    REACHABILITY PROBLEMS, 2011, 6945 : 191 - +
  • [34] What's Decidable About Parametric Timed Automata?
    Andre, Etienne
    FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, (FTSCS 2015), 2016, 596 : 52 - 68
  • [35] 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
  • [36] 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
  • [37] What's decidable about parametric timed automata?
    Andre, Etienne
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (02) : 203 - 219
  • [38] Durations and parametric model-checking in timed automata
    Bruyere, Veronique
    Dall'olio, Emmanuel
    Raskin, Jean-Francois
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2008, 9 (02)
  • [39] A CLP proof method for timed automata
    Jaffar, J
    Santosa, A
    Voicu, R
    25TH IEEE INTERNATIONAL REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2004, : 175 - 186
  • [40] A New Method for Transforming Timed Automata
    Khoumsi, Ahmed
    Ouedraogo, Lucien
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 130 : 101 - 128
12345