Abstract
In this paper, we propose a new framework for the parametric verification of time Petri nets with stopwatches controlled by inhibitor arcs. We first introduce an extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters. Then, we define a symbolic representation of the parametric state space based on the classical state class graph method. The parameters of the model are embedded into the firing domains of the classes, that are represented by convex polyhedra. Finally, we propose semi-algorithms for the parametric model-checking of a subset of parametric TCTL formulae on ITPNs. We can thus generate the set of the parameter valuations that satisfy the formulae.
Work supported by the French Government under grant ANR-SETI-06-003.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Merlin, P.: A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, Univ. of California, Irvine (1974)
Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Time state space analysis of real-time preemptive systems. IEEE trans. on Soft. Eng. 30(2), 97–111 (2004)
Roux, O.H., Lime, D.: Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 371–390. Springer, Heidelberg (2004)
Berthomieu, B., Lime, D., Roux, O.H., Vernadat, F.: Reachability problems and abstract state spaces for time petri nets with stopwatches. Discrete Event Dynamic Systems 17(2), 133–158 (2007)
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: ACM Symposium on Theory of Computing, pp. 592–601 (1993)
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. Springer, Heidelberg (2001)
Bruyère, V., Raskin, J.F.: Real-time model-checking: Parameters everywhere. CoRR abs/cs/0701138 (2007)
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. Int. Journal on Soft. Tools for Technology Transfer 1(1–2), 110–122 (1997)
Wang, F.: Parametric timing analysis for real-time systems. Inf. Comput. 130(2), 131–150 (1996)
Virbitskaite, I., Pokozy, E.: Parametric behaviour analysis for time petri nets. In: Malyshkin, V.E. (ed.) PaCT 1999. LNCS, vol. 1662, pp. 134–140. Springer, Heidelberg (1999)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE trans. on Soft. Eng. 17(3), 259–273 (1991)
Hadjidj, R., Boucheneb, H.: On-the-fly tctl model checking for time petri nets using state class graphs. In: ACSD, pp. 111–122. IEEE Computer Society, Los Alamitos (2006)
Traonouez, L.M., Lime, D., Roux, O.H.: Parametric model-checking of time petri nets with stopwatches using the state-class graph. Technical Report RI2008-3, IRCCyN, Nantes, France (2008)
Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Fundamentals of Computation Theory, pp. 62–88 (1995)
Cassez, F., Roux, O.H.: Structural translation from Time Petri Nets to Timed Automata – Model-Checking Time Petri Nets via Timed Automata. The journal of Systems and Software 79(10), 1456–1468 (2006)
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829. Springer, Heidelberg (2005)
Roux, O.H., Didier Lime, G.G., Magnin, M.: Roméo (2006), http://romeo.rts-software.org
Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library. Quaderno 457, Dipartimento di Matematica, Università di Parma, Italy (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Traonouez, LM., Lime, D., Roux, O.H. (2008). Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph. In: Cassez, F., Jard, C. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2008. Lecture Notes in Computer Science, vol 5215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85778-5_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-85778-5_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85777-8
Online ISBN: 978-3-540-85778-5
eBook Packages: Computer ScienceComputer Science (R0)