Abstract
This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toruń (2016) and Zaragoza (2017). A video of the presentation is available at https://www.youtube.com/playlist?list=PL9SOLKoGjbeqNcdQVqFpUz7HYqD1fbFIg, consisting of 14 short sequences. The paper presents not only the basic formal concepts tackled in the video version, but also an extensive literature to provide the reader with further references covering the area.
We first introduce motivation behind parametric verification in general, and then focus on different models and approaches, for verifying several kinds of systems. They include Parametric Timed Automata, for modelling real-time systems, where the timing constraints are not necessarily known a priori. Similarly, Parametric Interval Markov Chains allow for modelling systems where probabilities of events occurrences are intervals with parametric bounds. Parametric Petri Nets allow for compact representation of systems, and cope with different types of parameters. Finally, Action Synthesis aims at enabling or disabling actions in a concurrent system to guarantee some of its properties. Some tools implementing these approaches were used during hands-on sessions at the tutorial. The corresponding practicals are freely available on the Web.
This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002).
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 subscriptionsNotes
- 1.
- 2.
This figure comes from [19], itself coming from an adaptation of a figure by Ulrich Kühne.
- 3.
- 4.
References
Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Arvind, V., Ramanujam, S. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 245–256. Springer, Heidelberg (1998). https://doi.org/10.1007/978-3-540-49382-2_22
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993). https://doi.org/10.1006/inco.1993.1024
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) STOC, pp. 592–601. ACM, New York (1993). https://doi.org/10.1145/167088.167242
André, É.: Parametric deadlock-freeness checking timed automata. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 469–478. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_27
André, É.: A benchmark library for parametric timed model checking. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 75–83. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-12988-0_5
André, É.: What’s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf. 21(2), 203–219 (2019). https://doi.org/10.1007/s10009-017-0467-0
André, É., Bloemen, V., Petrucci, L., van de Pol, J.: Minimal-time synthesis for parametric timed automata. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 211–228. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_12
André, É., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819–836 (2009). https://doi.org/10.1142/S0129054109006905
André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_6
André, É., Hasuo, I., Waga, M.: Offline timed pattern matching under uncertainty. In: Lin, A.W., Sun, J. (eds.) ICECCS, pp. 10–20. IEEE CPS (2018). https://doi.org/10.1109/ICECCS2018.2018.00010
André, É., Lime, D.: Liveness in L/U-parametric timed automata. In: Legay, A., Schneider, K. (eds.) ACSD, pp. 9–18. IEEE (2017). https://doi.org/10.1109/ACSD.2017.19
André, É., Lime, D., Ramparison, M.: TCTL model checking lower/upper-bound parametric timed automata without invariants. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 37–52. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00151-3_3
André, É., Lime, D., Roux, O.H.: Decision problems for parametric timed automata. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 400–416. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_25
André, É., Lipari, G., Nguyen, H.G., Sun, Y.: Reachability preservation based parameter synthesis for timed automata. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 50–65. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_5
André, É., Liu, Y., Sun, J., Dong, J.S., Lin, S.-W.: PSyHCoS: parameter synthesis for hierarchical concurrent real-time systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 984–989. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_70
André, É., Markey, N.: Language preservation problems in parametric timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 27–43. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22975-1_3
André, É., Nguyen, H.G., Petrucci, L., Sun, J.: Parametric model checking timed automata under non-zenoness assumption. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 35–51. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_3
André, É., Soulat, R.: The Inverse Method. FOCUS Series in Computer Engineering and Information Technology, ISTE Ltd and Wiley, 176 p. (2013)
Andreychenko, A., Magnin, M., Inoue, K.: Analyzing resilience properties in oscillatory biological systems using parametric model checking. Biosystems 149, 50–58 (2016). https://doi.org/10.1016/j.biosystems.2016.09.002. Selected Papers from the Computational Methods in Systems Biology 2015 Conference
Aştefănoaei, L., Bensalem, S., Bozga, M., Cheng, C.-H., Ruess, H.: Compositional parameter synthesis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 60–68. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_4
Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008). https://doi.org/10.1016/j.scico.2007.08.001
Beneš, N., Bezděk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 69–81. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_6
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, pp. 211–225. Springer, Heidelberg (2005). https://doi.org/10.1007/11603009_17
Bouyer, P., Markey, N., Sankur, O.: Robustness in timed automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 1–18. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41036-9_1
Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Formal Methods Syst. Design 35(2), 121–151 (2009). https://doi.org/10.1007/s10703-009-0074-0
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986). https://doi.org/10.1109/TC.1986.1676819
Bundala, D., Ouaknine, J.: Advances in parametric real-time reasoning. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 123–134. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44522-8_11
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10\(^{20}\) states and beyond. In: LICS, pp. 428–439. IEEE Computer Society (1990). https://doi.org/10.1109/LICS.1990.113767
Chevallier, R., Encrenaz-Tiphène, E., Fribourg, L., Xu, W.: Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods Syst. Des. 34(1), 59–81 (2009). https://doi.org/10.1007/s10703-008-0061-x
David, N.: Discrete parameters in Petri nets. Ph.D. thesis. University of Nantes, France (2017)
David, N., Jard, C., Lime, D., Roux, O.H.: Discrete parameters in Petri nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 137–156. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19488-2_7
David, N., Jard, C., Lime, D., Roux, O.H.: Coverability synthesis in parametric Petri nets. In: Meyer, R., Nestmann, U. (eds.) CONCUR. LIPIcs, Dagstuhl Publishing (2017). https://doi.org/10.4230/LIPIcs.CONCUR.2017.14
Delahaye, B.: Consistency for parametric interval Markov chains. In: André, É., Frehse, G. (eds.) SynCoP. OASICS, vol. 44, pp. 17–32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015). https://doi.org/10.4230/OASIcs.SynCoP.2015.17
Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Consistency and refinement for interval Markov chains. J. Log. Algebr. Program. 81(3), 209–226 (2012). https://doi.org/10.1016/j.jlap.2011.10.003
Delahaye, B., Lime, D., Petrucci, L.: Parameter synthesis for parametric interval Markov chains. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 372–390. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_18
Demri, S.: On selective unboundedness of VASS. J. Comput. Syst. Sci. 79(5), 689–713 (2013). https://doi.org/10.1016/j.jcss.2013.01.014
Di Giampaolo, B., La Torre, S., Napoli, M.: Parametric metric interval temporal logic. Theoret. Comput. Sci. 564, 131–148 (2015). https://doi.org/10.1016/j.tcs.2014.11.019
Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208–213 (2007). https://doi.org/10.1016/j.ipl.2006.11.018
Fanchon, L., Jacquemard, F.: Formal timing analysis of mixed music scores. In: ICMC. Michigan Publishing, August 2013
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008). https://doi.org/10.1007/s10009-007-0062-x
Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30
Fribourg, L., Lesens, D., Moro, P., Soulat, R.: Robustness analysis for scheduling problems using the inverse method. In: Reynolds, M., Terenziani, P., Moszkowski, B. (eds.) TIME, pp. 73–80. IEEE Computer Society Press, September 2012. https://doi.org/10.1109/TIME.2012.10. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLMS-time12.pdf
Geeraerts, G., Heußner, A., Praveen, M., Raskin, J.: \(\omega \)-Petri nets: algorithms and complexity. Fundamenta Informaticae 137(1), 29–60 (2015)
Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039066
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1–2), 110–122 (1997). https://doi.org/10.1007/s100090050008
Hoare, C.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Upper Saddle River (1985)
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52–53, 183–220 (2002). https://doi.org/10.1016/S1567-8326(02)00037-1
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)
Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015). https://doi.org/10.1109/TSE.2014.2357445
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969). https://doi.org/10.1016/S0022-0000(69)80011-5
Knapik, M.: https://michalknapik.github.io/spatula
Knapik, M., Meski, A., Penczek, W.: Action synthesis for branching time logic: theory and applications. ACM Trans. Embed. Comput. 14(4), 64 (2015). https://doi.org/10.1145/2746337
Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. Trans. Petri Nets Other Models Concurr. 5, 141–159 (2012). https://doi.org/10.1007/978-3-642-29072-5_6
Knapik, M., Penczek, W.: Fixed-point methods in parametric model checking. In: Angelov, P., et al. (eds.) Intelligent Systems’2014. AISC, vol. 322, pp. 231–242. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-11313-5_22
Li, J., Sun, J., Gao, B., André, É.: Classification-based parameter synthesis for parametric timed automata. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 243–261. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68690-5_15
Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_6
Luthmann, L., Stephan, A., Bürdek, J., Lochau, M.: Modeling and testing product lines with unbounded parametric real-time constraints. In: Cohen, M.B., et al. (eds.) SPLC, vol. A, pp. 104–113. ACM (2017). https://doi.org/10.1145/3106195.3106204
Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 296–310. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46430-1_26
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Upper Saddle River (1967)
Parquier, B., et al.: Applying parametric model-checking techniques for reusing real-time critical systems. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2016. CCIS, vol. 694, pp. 129–144. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-53946-1_8
Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt 2006. LNCS (LNAI), vol. 4428, pp. 113–128. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74128-2_8
Petrucci, L., van de Pol, J.: Parameter synthesis algorithms for parametric interval Markov chains. In: Baier, C., Caires, L. (eds.) FORTE 2018. LNCS, vol. 10854, pp. 121–140. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92612-4_7
Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. J. Appl. Log. 5(2), 235–251 (2007). https://doi.org/10.1016/j.jal.2005.12.010
Sankur, O.: Symbolic quantitative robustness analysis of timed automata. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 484–498. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_48
Seidner, C.: Vérification des EFFBDs: model checking en Ingénierie Système. (EFFBDs verification: model checking in systems engineering). Ph.D. thesis. University of Nantes, France (2009). https://tel.archives-ouvertes.fr/tel-00440677
Somenzi, F.: CUDD: CU decision diagram package - release 2.5.0. https://github.com/ivmai/cudd
Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., André, É.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. 22(1), 3:1–3:29 (2013). https://doi.org/10.1145/2430536.2430537
Sun, Y., André, É., Lipari, G.: Verification of two real-time systems using parametric timed automata. In: Quinton, S., Vardanega, T. (eds.) WATERS, July 2015
Traonouez, L.M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. J. Univ. Comput. Sci. 15(17), 3273–3304 (2009). https://doi.org/10.3217/jucs-015-17-3273
Valk, R., Jantzen, M.: The residue of vector sets with applications to decidability problems in Petri nets. Acta Informatica 21(6), 643–674 (1985). https://doi.org/10.1007/BF00289715
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer-Verlag GmbH Germany, part of Springer Nature
About this chapter
Cite this chapter
André, É., Knapik, M., Lime, D., Penczek, W., Petrucci, L. (2019). Parametric Verification: An Introduction. In: Koutny, M., Pomello, L., Kristensen, L. (eds) Transactions on Petri Nets and Other Models of Concurrency XIV. Lecture Notes in Computer Science(), vol 11790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-60651-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-60651-3_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-60650-6
Online ISBN: 978-3-662-60651-3
eBook Packages: Computer ScienceComputer Science (R0)