×

zbMATH — the first resource for mathematics

Linear parametric model checking of timed automata. (English) Zbl 1008.68069
Summary: We present an extension of the model checker UPPAAL, capable of synthesizing linear parameter constraints for the correctness of parametric timed automata. A symbolic representation of the (parametric) state space in terms of parametric difference bound matrices 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 known to be undecidable. Also, we present a number of results that reduce the verification effort for L/U automata in certain 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).

MSC:
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Kronos; TREX; Uppaal; Uppaal2k
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Annichini, A.; Asarin, E.; Bouajjani, A., Symbolic techniques for parametric reasoning about counter and clock systems, (), 419-434 · Zbl 0974.68523
[2] Annichini, A.; Bouajjani, A.; Sighireanu, M., Trex: a tool for reachability analysis of complex systems, () · Zbl 0991.68645
[3] Alur, R.; Dill, D.L., Automata for modeling real-time systems, (), 322-335, Full version appeared as [4] · Zbl 0765.68150
[4] Alur, R.; Dill, D.L., A theory of timed automata, Theoret. comput. sci., 126, 183-235, (1994) · Zbl 0803.68071
[5] Alur, R.; Henzinger, T.A.; Vardi, M.Y., Parametric real-time reasoning, (), 592-601 · Zbl 1310.68139
[6] Abadi, M.; Lamport, L., An old-fashioned recipe for real time, (), 1-27
[7] R. Alur, Timed automata, in: NATO-ASI Summer School on Verification of Digital and Hybrid Systems, Springer, Berlin, 1998, to appear
[8] Bozga, M.; Daws, C.; Maler, O.; Olivero, A.; Tripakis, S.; Yovine, S., Kronos: A model-checking tool for real-time systems, (), 546-550
[9] G. Bandini, R.L. Lutje Spelberg, R.C.H. de Rooij, W.J. Toetenel, Application of Parametric Model Checking—The Root Contention Protocol using LPMC, in: Proceedings of the 34th Hawaii International Conference on System Sciences (HICCS’01), 2001
[10] Clarke, E.M.; Grumberg, O.; Peled, D., Model checking, (1999), MIT Press Cambridge, MA
[11] Cormen, T.H.; Leiserson, C.E.; Rivest, R.L., Introduction to algorithms, (1991), McGraw-Hill New York
[12] A. Collomb-Annichini, M. Sighireanu, Parameterized reachability analysis of the IEEE 1394 Root Contention Protocol using TReX, in: P. Pettersson, S. Yovine (Eds.), Proceedings of the Workshop on Real-Time Tools (RT-TOOLS’2001), 2001
[13] Dill, D., Timing assumptions and verification of finite-state concurrent systems, (), 197-212
[14] D’Argenio, P.R.; Katoen, J.-P.; Ruys, T.C.; Tretmans, J., The bounded retransmission protocol must be on time!, (), 416-431
[15] Henzinger, T.A.; Ho, P.-H.; Wong-Toi, H., \schytech: A model checker for hybrid systems, (), 460-463
[16] Hune, T.S.; Romijn, J.M.T.; Stoelinga, M.I.A.; Vaandrager, F.W., Linear parametric model checking of timed automata, (), 189-203 · Zbl 0978.68094
[17] IEEE Computer Society. IEEE Standard for a High Performance Serial Bus. Std 1394-1995, August 1996
[18] Kristoffersen, K.J.; Laroussinie, F.; Larsen, K.G.; Pettersson, P.; Yi, W., A compositional proof of a real-time mutual exclusion protocol, (), 565-579
[19] Lamport, L., A fast mutual exclusion algorithm, ACM trans. comput. syst., 5, 1, 1-11, (1987)
[20] Larsen, K.G.; Larsson, F.; Pettersson, P.; Wang Yi, Efficient verification of real-time systems: compact data structures and state-space reduction, (), 14-24
[21] Larsen, K.G.; Pettersson, P.; Wang Yi, \scuppaal in a nutshell, Int. J. software tools technol. transfer, 1, 1-2, 134-152, (1997) · Zbl 1060.68577
[22] Lutje Spelberg, R.F.; Toetenel, W.J.; Ammerlaan, M., Partition refinement in real-time model checking, (), 143-157
[23] Lynch, N.A., Distributed algorithms, (1996), Morgan Kaufmann San Fransisco, CA · Zbl 0877.68061
[24] Merritt, M.; Modugno, F.; Tuttle, M., Time constrained automata, (), 408-423
[25] D.P.L. Simons, M.I.A. Stoelinga, Mechanical verification of the IEEE 1394a Root Contention Protocol using Uppaal2k. Springer International Journal on Software Tools for Technology Transfer (STTT) 3 (2001) 469-485 · Zbl 1053.68580
[26] M.I.A. Stoelinga, Fun with FireWire: a comparative study of formal verification methods applied to the IEEE 1394 Root Contention Protocol, Formal Aspects of Computing, to appear (2002) · Zbl 1029.68022
[27] Stoelinga, M.I.A.; Vaandrager, F.W., Root contention in IEEE 1394, (), 53-74
[28] Yovine, S., Model checking timed automata, (), 114-152
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.