Abstract
We present here Imitator, a tool for synthesizing constraints on timing bounds (seen as parameters) in the framework of timed automata. Unlike classical synthesis methods, we take advantage of a given reference valuation of the parameters for which the system is known to behave properly. Our aim is to generate a constraint such that, under any valuation satisfying this constraint, the system is guaranteed to behave, in terms of alternating sequences of locations and actions, as under the reference valuation. This is useful for safely relaxing some values of the reference valuation, and optimizing timing bounds of the system. We have successfully applied our tool to various examples of asynchronous circuits and protocols.
This work is partially supported by the Agence Nationale de la Recherche, grant ANR-06-ARFU-005, and by Institut Farman (ENS Cachan).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC 1993, pp. 592–601. ACM Press, New York (1993)
Amari, S., André, É., Chatain, T., De Smet, O., Denis, B., Encrenaz, E., Fribourg, L., Ruel, S.: Timed analysis of distributed control systems combining simulation and parametric model checking. Research report, LSV, ENS Cachan, France (2009)
André, É., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. International Journal of Foundations of Computer Science (IJFCS) (to appear)
André, É., Encrenaz, E., Fribourg, L.: Synthesizing parametric constraints on various case studies using Imitator. Research report, Laboratoire Spécification et Vérification, ENS Cachan, France (June 2009)
Chevallier, R., Encrenaz-Tiphène, E., Fribourg, L., Xu, W.: Verification of the generic architecture of a memory circuit using parametric timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 113–127. Springer, Heidelberg (2006)
Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 312–327. Springer, Heidelberg (2004)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187–200. Springer, Heidelberg (2008)
Henzinger, T.A., Ho, P., Wong-Toi, H.: A user guide to HyTech. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 41–71. Springer, Heidelberg (1995)
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 189–203. Springer, Heidelberg (2001)
Nicollin, X., Sifakis, J., Yovine, S.: Compiling real-time specifications into extended automata. IEEE Trans. on Software Engineering 18, 794–804 (1992)
Simons, D., Stoelinga, M.: Mechanical verification of the IEEE 1394a Root Contention Protocol using Uppaal2k. International Journal on Software Tools for Technology Transfer 3(4), 469–485 (2001)
Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures. IEEE Trans. Softw. Eng. 31(1), 38–51 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
André, É. (2009). IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata . In: Leucker, M., Morgan, C. (eds) Theoretical Aspects of Computing - ICTAC 2009. ICTAC 2009. Lecture Notes in Computer Science, vol 5684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03466-4_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-03466-4_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03465-7
Online ISBN: 978-3-642-03466-4
eBook Packages: Computer ScienceComputer Science (R0)