Special Issue – Reachability Problems (RP 2008)No Access

AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA

ÉTIENNE ANDRÉ

LSV – ENS Cachan & CNRS, 61 avenue du Président Wilson, 94230 Cachan, France

Search for more papers by this author

THOMAS CHATAIN

LSV – ENS Cachan & CNRS, 61 avenue du Président Wilson, 94230 Cachan, France

Search for more papers by this author

LAURENT FRIBOURG

LSV – ENS Cachan & CNRS, 61 avenue du Président Wilson, 94230 Cachan, France

Search for more papers by this author

, and

EMMANUELLE ENCRENAZ

LIP6 – Université Pierre et Marie Curie & CNRS, 4 place Jussieu, 75005 Paris, France

Search for more papers by this author

https://doi.org/10.1142/S0129054109006905Cited by:51 (Source: Crossref)

Abstract

We consider in this paper systems modeled by timed automata. The timing bounds involved in the action guards and location invariants of our timed automata are not constants, but parameters. Those parametric timed automata allow the modelling of various kinds of timed systems, e.g. communication protocols or asynchronous circuits. We will also assume that we are given an initial tuple π₀ of values for the parameters, which corresponds to values for which the system is known to behave properly. Our goal is to compute a constraint K₀ on the parameters, satisfied by π₀, guaranteeing that, under any parameter valuation satisfying K₀, the system behaves in the same manner: for any two parameter valuations satisfying K₀, the behaviors of the timed automata are (time-abstract) equivalent, i.e., the traces of execution viewed as alternating sequences of actions and locations are identical. We present an algorithm InverseMethod that terminates in the case of acyclic models, and discuss how to extend it to the cyclic case. We also explain how to combine our method with classical synthesis methods which are based on the avoidance of a given set of bad states. A prototype implementation has been done, and various experiments are described.

This work is partially supported by the Agence Nationale de la Recherche, grant ANR-06-ARFU-005, and by Institut Farman (ENS Cachan).

Keywords:

References

R. Alur and D. L. Dill, TCS 126(2), 183 (1994), DOI: 10.1016/0304-3975(94)90010-8. Crossref, Web of Science, Google Scholar
R. Alur, T. A. Henzinger and M. Y. Vardi, Parametric real-time reasoning, STOC '93 (ACM, 1993) pp. 592–601. Google Scholar
É. André, E. Encrenaz, and L. Fribourg. Synthesizing parametric constraints on various case studies using Imitator. Research report, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2009 . Google Scholar
Étienne André , Imitator: a tool for synthesizing constraints on timing bounds of timed automata , ICTAC'09 , LNCS ( Springer , 2009 ) . Google Scholar
A. Annichini , E. Asarin and A. Bouajjani , Symbolic techniques for parametric reasoning about counter and clock systems , CAV '00 ( Springer-Verlag , 2000 ) . Google Scholar
R. Chevallieret al., Formal Methods in System Design 34(1), 59 (2009), DOI: 10.1007/s10703-008-0061-x. Crossref, Web of Science, Google Scholar
R. Clarisó and J. Cortadella , Verification of concurrent systems with parametric delays using octahedra , ACSD '05 ( IEEE Computer Society , 2005 ) . Google Scholar
R. Clarisó and J. Cortadella, Sci. Comput. Program. 64(1), 115 (2007). Crossref, Web of Science, Google Scholar
E. M. Clarkeet al., Counterexample-guided abstraction refinement, CAV '00 (Springer-Verlag, 2000) pp. 154–169. Google Scholar
A. Collomb–Annichini and M. Sighireanu , Parameterized reachability analysis of the IEEE 1394 Root Contention Protocol using TReX , RT-TOOLS '01 ( 2001 ) . Google Scholar
Laurent Doyen, Information Processing Letters 102(5), 208 (2007), DOI: 10.1016/j.ipl.2006.11.018. Crossref, Web of Science, Google Scholar
G. Frehse, S. K. Jha and B. H. Krogh, A counterexample-guided approach to parameter synthesis for linear hybrid automata, HSCC '084981, LNCS (Springer, 2008) pp. 187–200. Google Scholar
T. A. Henzinger, P. Ho and H. Wong-Toi, A user guide to HyTech, TACAS (1995) pp. 41–71. Google Scholar
T. A. Henzinger and H. Wong-Toi, Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165 (Springer-Verlag, London, UK, 1996) pp. 265–282. Crossref, Google Scholar
T. Huneet al., Journal of Logic and Algebraic Programming (2002). Google Scholar
K. G. Larsen, P. Pettersson and W. Yi, International Journal on Software Tools for Technology Transfer 1(2), 134 (1997). Crossref, Google Scholar
X. Nicollin, J. Sifakis and S. Yovine, IEEE Trans. on Software Engineering 18, 794 (1992), DOI: 10.1109/32.159837. Crossref, Web of Science, Google Scholar
R. Ben Salah, M. Bozga and O. Maler, On interleaving in timed automata, CONCUR '064137, LNCS (Springer, 2006) pp. 465–476. Google Scholar
Alexander Schrijver , Theory of linear and integer programming ( John Wiley & Sons, Inc. , New York, NY, USA , 1986 ) . Google Scholar
D. Simons and M. Stoelinga, IJSTTT 3(4), 469 (2001). Google Scholar
S. Tripakis and S. Yovine, Form. Methods Syst. Des. 18(1), 25 (2001), DOI: 10.1023/A:1008734703554. Crossref, Web of Science, Google Scholar
F. Wang and H. C. Yen, Timing parameter characterization of real-time systems, CIAA '032759, LNCS (2003) pp. 23–34. Google Scholar
Farn Wang, IEEE Trans. Softw. Eng. 31(1), 38 (2005), DOI: 10.1109/TSE.2005.99. Crossref, Web of Science, Google Scholar
T. Yoneda, T. Kitai and C. J. Myers, Automatic derivation of timing constraints by failure analysis, CAV '02 (Springer-Verlag, 2002) pp. 195–208. Google Scholar