nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

A Benchmark Library for Parametric Timed Model Checking

verfasst von : Étienne André

Erschienen in: Formal Techniques for Safety-Critical Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Formal Verification of Random Forests in Safety-Critical Applications

Nächstes Kapitel Formal Timing Analysis of Digital Circuits

“Formal Methods for Timing Verification Challenge", in the WATERS workshop: http://waters2015.inria.fr/.

In a hybrid automaton, a parameter is a variable that can evolve for an arbitrary amount of time at rate 1, and is then “frozen” (rate 0).

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_46CrossRef

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_22CrossRef

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)

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

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

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 2009

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/S0129054109006905MathSciNetCrossRefMATH

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_21CrossRef

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_6CrossRef

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)

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_3CrossRefMATH

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.

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_2CrossRef

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_70CrossRef

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_6CrossRefMATH

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-0CrossRefMATH

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_12CrossRef

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_29CrossRef

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-xCrossRefMATH

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.

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.009MathSciNetCrossRefMATH

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)

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/BFb0035403CrossRef

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-xCrossRefMATH

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_30CrossRef

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_3CrossRef

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.

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-1MathSciNetCrossRefMATH

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_28CrossRefMATH

30.

Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015)CrossRef

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_6CrossRef

32.

Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)MathSciNetCrossRef

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_15CrossRef

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_6CrossRef

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.6MathSciNetCrossRef

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)

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.

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_48CrossRef

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 2015

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_14CrossRef

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)MathSciNetMATH

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-5CrossRef

Titel: A Benchmark Library for Parametric Timed Model Checking
verfasst von: Étienne André
Verlag: Springer International Publishing
Buch: Formal Techniques for Safety-Critical Systems
Print ISBN: 978-3-030-12987-3

Electronic ISBN: 978-3-030-12988-0

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-12988-0_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"