Advertisement

A Benchmark Library for Parametric Timed Model Checking

  • Étienne AndréEmail author
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1008)

Abstract

Verification of real-time systems involving hard timing constraints and concurrency is of utmost importance. Parametric timed model checking allows for formal verification in the presence of unknown timing constants or uncertainty (e. g., imprecision for periods). With the recent development of several techniques and tools to improve the efficiency of parametric timed model checking, there is a growing need for proper benchmarks to test and compare fairly these tools. We present here a benchmark library for parametric timed model checking made of benchmarks accumulated over the years. Our benchmarks include academic benchmarks, industrial case studies and examples unsolvable using existing techniques.

Keywords

Case studies Model checking Parameter synthesis Parametric timed automata 

References

  1. 1.
    Abdeddaïm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 478–492. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44585-4_46CrossRefGoogle Scholar
  2. 2.
    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_22CrossRefGoogle Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) Proceedings of the Twenty-fifth Annual ACM Symposium on Theory of Computing, STOC 1993, pp. 592–601. ACM, New York (1993)Google Scholar
  4. 4.
    André, É.: Observer patterns for real-time systems. In: Liu, Y., Martin, A. (eds.) 18th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2013, pp. 125–134. IEEE Computer Society, July 2013.  https://doi.org/10.1109/ICECCS.2013.26
  5. 5.
    André, É.: What’s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf. (2018, to appear).  https://doi.org/10.1007/s10009-017-0467-0
  6. 6.
    André, É., Chatain, Th., De Smet, O., Fribourg, L., Ruel, S.: Synthèse de contraintes temporisées pour une architecture d’automatisation en réseau. In: Lime, D., Roux, O.H. (eds.) Actes du 7ème colloque sur la modélisation des systèmes réactifs, MSR 2009. Journal Européen des Systèmes Automatisés, vol. 43, pp. 1049–1064. Hermès, November 2009Google Scholar
  7. 7.
    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/S0129054109006905MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    André, É., Coti, C., Nguyen, H.G.: Enhanced distributed behavioral cartography of parametric timed automata. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 319–335. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-25423-4_21CrossRefGoogle Scholar
  9. 9.
    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_6CrossRefGoogle Scholar
  10. 10.
    André, É., Hasuo, I., Waga, M.: Offline timed pattern matching under uncertainty. In: Lin, A.W., Sun, J. (eds.) Proceedings of the 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018. IEEE (2018, to appear)Google Scholar
  11. 11.
    André, É., Lime, D., Ramparison, M.: TCTL model checking lower/upper-bound parametric timed automata without invariants. In: Jansen, D., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-00151-3_3CrossRefzbMATHGoogle Scholar
  12. 12.
    André, É., Lime, D., Ramparison, M.: Timed automata with parametric updates. In: Juhás, G., Chatain, T., Grosu, R. (eds.) Proceedings of the 18th International Conference on Application of Concurrency to System Design, ACSD 2018, pp. 21–29. IEEE (2018, to appear).  https://doi.org/10.1109/ACSD.2018.000-2
  13. 13.
    André, É., Lin, S.-W.: Learning-based compositional parameter synthesis for event-recording automata. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 17–32. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-60225-7_2CrossRefGoogle Scholar
  14. 14.
    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_70CrossRefGoogle Scholar
  15. 15.
    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_6CrossRefzbMATHGoogle Scholar
  16. 16.
    Bozzelli, L., La Torre, S.: Decision problems for lower/upper bound parametric timed automata. Formal Methods Syst. Des. 35(2), 121–151 (2009).  https://doi.org/10.1007/s10703-009-0074-0CrossRefzbMATHGoogle Scholar
  17. 17.
    Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138–152. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44618-4_12CrossRefGoogle Scholar
  18. 18.
    Chen, X., Schupp, S., Makhlouf, I.B., Ábrahám, E., Frehse, G., Kowalewski, S.: A benchmark suite for hybrid systems reachability analysis. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 408–414. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-17524-9_29CrossRefGoogle Scholar
  19. 19.
    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-xCrossRefzbMATHGoogle Scholar
  20. 20.
    Clarisó, R., Cortadella, J.: Verification of concurrent systems with parametric delays using octahedra. In: Proceedings of the Fifth International Conference on Application of Concurrency to System Design, ACSD 2005, pp. 122–131. IEEE Computer Society (2005).  https://doi.org/10.1109/ACSD.2005.34
  21. 21.
    Clarisó, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program. 64(1), 115–139 (2007).  https://doi.org/10.1016/j.scico.2006.03.009MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Collomb-Annichini, A., Sighireanu, M.: Parameterized reachability analysis of the IEEE 1394 root contention protocol using TReX. In: Proceedings of the Real-Time Tools Workshop, RT-TOOLS 2001 (2001)Google Scholar
  23. 23.
    D’Argenio, P.R., Katoen, J.-P., Ruys, T.C., Tretmans, J.: The bounded retransmission protocol must be on time!. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0035403CrossRefGoogle Scholar
  24. 24.
    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-xCrossRefzbMATHGoogle Scholar
  25. 25.
    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_30CrossRefGoogle Scholar
  26. 26.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A user guide to HyTech. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 41–71. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60630-0_3CrossRefGoogle Scholar
  27. 27.
    Hoxha, B., Abbas, H., Fainekos, G.E.: Benchmarks for temporal logic requirements for automotive systems. In: Frehse, G., Althoff, M. (eds.) Proceedings of the 1st and 2nd International Workshops on Applied veRification for Continuous and Hybrid Systems, ARCH@CPSWeek 2014/ARCH@CPSWeek 2015. EPiC Series in Computing, vol. 34, pp. 25–30. EasyChair (2014). http://www.easychair.org/publications/paper/250954
  28. 28.
    Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Logic Algebraic Program. 52–53, 183–220 (2002).  https://doi.org/10.1016/S1567-8326(02)00037-1MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 401–415. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_28CrossRefzbMATHGoogle Scholar
  30. 30.
    Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015)CrossRefGoogle Scholar
  31. 31.
    Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 141–159. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-29072-5_6CrossRefGoogle Scholar
  32. 32.
    Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)MathSciNetCrossRefGoogle Scholar
  33. 33.
    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_15CrossRefGoogle Scholar
  34. 34.
    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_6CrossRefGoogle Scholar
  35. 35.
    Lipari, G., Sun, Y., André, É., Fribourg, L.: Toward parametric timed interfaces for real-time components. In: Andre, E., Frehse, G. (eds.) 1st International Workshop on Synthesis of Continuous Parameters, SynCoP 2014. Electronic Proceedings in Theoretical Computer Science, vol. 145, pp. 49–64, April 2014.  https://doi.org/10.4204/EPTCS.145.6MathSciNetCrossRefGoogle Scholar
  36. 36.
    Nguyen, H.G., Petrucci, L., van de Pol, J.: Layered and collecting NDFS with subsumption for parametric timed automata. In: Lin, A.W., Sun, J. (eds.) Proceedings of the 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018. IEEE, December 2018 (to appear)Google Scholar
  37. 37.
    Palencia Gutiérrez, J.C., González Harbour, M.: Schedulability analysis for tasks with static and dynamic offsets. In: Proceedings of the 19th IEEE Real-Time Systems Symposium, RTSS 1998, pp. 26–37. IEEE Computer Society (1998).  https://doi.org/10.1109/REAL.1998.739728
  38. 38.
    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_48CrossRefGoogle Scholar
  39. 39.
    Sun, Y., André, É., Lipari, G.: Verification of two real-time systems using parametric timed automata. In: Quinton, S., Vardanega, T. (eds.) Proceedings of the 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems, WATERS 2015, July 2015Google Scholar
  40. 40.
    Sun, Y., Soulat, R., Lipari, G., André, É., Fribourg, L.: Parametric schedulability analysis of fixed priority real-time distributed systems. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2013. CCIS, vol. 419, pp. 212–228. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-05416-2_14CrossRefGoogle Scholar
  41. 41.
    Traonouez, L.M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. J. Univers. Comput. Sci. 15(17), 3273–3304 (2009)MathSciNetzbMATHGoogle Scholar
  42. 42.
    Wandeler, E., Thiele, L., Verhoef, M., Lieverse, P.: System architecture evaluation using modular performance analysis: a case study. Int. J. Softw. Tools Technol. Transf. 8(6), 649–667 (2006).  https://doi.org/10.1007/s10009-006-0019-5CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Université Paris 13, LIPN, CNRS, UMR 7030VilletaneuseFrance
  2. 2.JFLI, CNRSTokyoJapan
  3. 3.National Institute of InformaticsTokyoJapan

Personalised recommendations