Abstract
We present an extension of the model checker Uppaal capable of synthesize linear parameter constraints for the correctness of parametric timed automata. The symbolic representation of the (parametric) state-space is shown to be correct. A second contribution of this paper is the identification of a subclass of parametric timed automata (L/U automata), for which the emptiness problem is decidable, contrary to the full class where it is know to be undecidable. Also we present a number of lemmas enabling the verification effort to be reduced for L/U automata in some cases. We illustrate our approach by deriving linear parameter constraints for a number of well-known case studies from the literature (exhibiting a flaw in a published paper).
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Research supported by Esprit Project 26270, Verification of Hybrid Systems (VHS), and PROGRESS Project TES4199, Verification of Hard and Softly Timed Systems (HaaST). This work was initiated during a visit of the first author to Nijmegen.
Download to read the full chapter text
Chapter PDF
References
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
R. Alur, T.A. Henzinger, and M.Y. Vardi. Parametric real-time reasoning. In Proc. 25th Annual Symp. on Theory of Computing, pages 592–601. ACM Press, 1993.
A. Annichini, E. Asarin, and A. Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems. In Proc. 12th Int. Conference on Computer Aided Verification, LNCS 1855, pages 419–434. Springer-Verlag, 2000.
G. Bandini, R. Lutje Spelberg, and H. Toetenel. Parametric verification of the IEEE 1394a root contention protocol using LPMC. http://tvs.twi.tudelft.nl/, July 2000. Submitted.
M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. In Proc. 10th Int. Conference on Computer Aided Verification, LNCS 1427, pages 546–550. Springer-Verlag, June/July 1998.
T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. McGraw-Hill, Inc., 1991.
P.R. D’Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In Proc. Third Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1217, pages 416–431. Springer-Verlag, April 1997.
D. Dill. Timing assumptions and verification of finite-state concurrent systems. In Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, pages 197–212. Springer-Verlag, 1990.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems. In Proc. 9th Int. Conference on Computer Aided Verification, LNCS 1254, pages 460–463. Springer-Verlag, 1997.
T.S. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager. Linear parametric model checking of timed automata. Report CSI-R0102, CSI, University of Nijmegen, January 2001.
K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1–2):134–152, October 1997.
R.F. Lutje Spelberg, W.J. Toetenel, and M. Ammerlaan. Partition refinement in real-time model checking. In Proc. FTRTFT’98, LNCS 1486, pages 143–157. Springer-Verlag, 1998.
D.P.L. Simons and M.I.A. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Technical Report CSI-R0009, CSI, University of Nijmegen, May 2000. Conditionally accepted for STTT.
M.I.A. Stoelinga and F.W. Vaandrager. Root contention in IEEE 1394. In Proc. 5th Int. AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601, pages 53–74. Springer-Verlag, 1999.
S. Yovine. Model checking timed automata. In Lectures on Embedded Systems, LNCS 1494, pages 114–152. Springer-Verlag, October 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F. (2001). Linear Parametric Model Checking of Timed Automata. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_14
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive