IMITATOR 3: synthesis of timing parameters beyond decidability. (English) Zbl 1493.68202
Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12759, 552-565 (2021).
Summary: Real-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. IMITATOR takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. IMITATOR extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by IMITATOR 3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.
For the entire collection see [Zbl 1489.68029].
For the entire collection see [Zbl 1489.68029].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q45 | Formal languages and automata |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Aceto, L.; Bouyer, P.; Burgueño, A.; Larsen, KG, The power of reachability testing for timed automata, TCS, 300, 1-3, 411-475 (2003) · Zbl 1023.68060 · doi:10.1016/S0304-3975(02)00334-1 |
| [2] | Alur, R., The algorithmic analysis of hybrid systems, TCS, 138, 1, 3-34 (1995) · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T |
| [3] | Alur, R.; Dill, DL, A theory of timed automata, TCS, 126, 2, 183-235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8 |
| [4] | Alur, R.; Fix, L.; Henzinger, TA, Event-clock automata: a determinizable class of timed automata, TCS, 211, 1-2, 253-273 (1999) · Zbl 0912.68132 · doi:10.1016/S0304-3975(97)00173-4 |
| [5] | 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, NY, USA (1993). doi:10.1145/167088.167242 · Zbl 1310.68139 |
| [6] | André, É.: Observer patterns for real-time systems. In: Liu, Y., Martin, A. (eds.) ICECCS, pp. 125-134. IEEE Computer Society, July 2013. doi:10.1109/ICECCS.2013.26 |
| [7] | André, É.; Sampaio, A.; Wang, F., Parametric deadlock-freeness checking timed automata, Theoretical Aspects of Computing - ICTAC 2016, 469-478 (2016), Cham: Springer, Cham · Zbl 1482.68132 · doi:10.1007/978-3-319-46750-4_27 |
| [8] | André, É., What’s decidable about parametric timed automata?, STTT, 21, 2, 203-219 (2019) · doi:10.1007/s10009-017-0467-0 |
| [9] | André, É.: Artifact for IMITATOR 3.0, April 2021. doi:10.5281/zenodo.4723415 |
| [10] | André, É.: IMITATOR user manual, January 2021. https://github.com/imitator-model-checker/imitator/releases/download/v3.0.0/IMITATOR-user-manual.pdf |
| [11] | André, É.; Arias, J.; Petrucci, L.; Pol, J., Iterative bounded synthesis for efficient cycle detection in parametric timed automata, Tools and Algorithms for the Construction and Analysis of Systems, 311-329 (2021), Cham: Springer, Cham · Zbl 1467.68078 · doi:10.1007/978-3-030-72016-2_17 |
| [12] | André, É.; Bloemen, V.; Petrucci, L.; van de Pol, J.; Vojnar, T.; Zhang, L., Minimal-time synthesis for parametric timed automata, Tools and Algorithms for the Construction and Analysis of Systems, 211-228 (2019), Cham: Springer, Cham · doi:10.1007/978-3-030-17465-1_12 |
| [13] | André, É., Coquard, E., Fribourg, L., Jerray, J., Lesens, D.: Scheduling synthesis for a launcher flight control using parametric stopwatch automata. In: Keller, J., Penczek, W. (eds.) ACSD, pp. 13-22. IEEE (2019). doi:10.1109/ACSD.2019.00006 · Zbl 1520.93344 |
| [14] | André, É., Coti, C., Evangelista, S.: Distributed behavioral cartography of timed automata. In: Dongarra, J., Ishikawa, Y., Atsushi, H. (eds.) EuroMPI/ASIA, pp. 109-114. ACM, September 2014. doi:10.1145/2642769.2642784 |
| [15] | André, É.; Coti, C.; Nguyen, HG; Butler, M.; Conchon, S.; Zaïdi, F., Enhanced distributed behavioral cartography of parametric timed automata, Formal Methods and Software Engineering, 319-335 (2015), Cham: Springer, Cham · doi:10.1007/978-3-319-25423-4_21 |
| [16] | André, É.; Fribourg, L.; Kučera, A.; Potapov, I., Behavioral cartography of timed automata, Reachability Problems, 76-90 (2010), Heidelberg: Springer, Heidelberg · Zbl 1287.68089 · doi:10.1007/978-3-642-15349-5_5 |
| [17] | André, É.; Fribourg, L.; Kühne, U.; Soulat, R.; Giannakopoulou, D.; Méry, D., IMITATOR 2.5: a tool for analyzing robustness in scheduling problems, FM 2012: Formal Methods, 33-36 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-32759-9_6 |
| [18] | André, É.; Fribourg, L.; Mota, J-M; Soulat, R.; Enea, C.; Piskac, R., Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking, Verification, Model Checking, and Abstract Interpretation, 409-424 (2019), Cham: Springer, Cham · Zbl 1522.68293 · doi:10.1007/978-3-030-11245-5_19 |
| [19] | André, É.; Fribourg, L.; Soulat, R.; Van Hung, D.; Ogawa, M., Merge and conquer: state merging in parametric timed automata, Automated Technology for Verification and Analysis, 381-396 (2013), Cham: Springer, Cham · Zbl 1410.68194 · doi:10.1007/978-3-319-02444-8_27 |
| [20] | André, É., Hasuo, I., Waga, M.: Offline timed pattern matching under uncertainty. In: Lin, A.W., Sun, J. (eds.) ICECCS, pp. 10-20. IEEE Computer Society (2018). doi:10.1109/ICECCS2018.2018.00010 |
| [21] | André, É., Lime, D., Markey, N.: Language preservation problems in parametric timed automata. LMCS 16, January 2020. doi:10.23638/LMCS-16(1:5)2020 · Zbl 1429.68098 |
| [22] | André, É.; Lime, D.; Ramparison, M.; Pérez, JA; Yoshida, N., Parametric updates in parametric timed automata, Formal Techniques for Distributed Objects, Components, and Systems, 39-56 (2019), Cham: Springer, Cham · Zbl 1533.68126 · doi:10.1007/978-3-030-21759-4_3 |
| [23] | André, É., Lime, D., Ramparison, M., Stoelinga, M.: Parametric analyses of attack-fault trees. In: Keller, J., Penczek, W. (eds.) ACSD, pp. 33-42. IEEE (2019). doi:10.1109/ACSD.2019.00008 · Zbl 1491.68034 |
| [24] | André, É.; Lin, S-W; Bouajjani, A.; Silva, A., Learning-based compositional parameter synthesis for event-recording automata, Formal Techniques for Distributed Objects, Components, and Systems, 17-32 (2017), Cham: Springer, Cham · Zbl 1489.68136 · doi:10.1007/978-3-319-60225-7_2 |
| [25] | André, É.; Lipari, G.; Nguyen, HG; Sun, Y.; Havelund, K.; Holzmann, G.; Joshi, R., Reachability preservation based parameter synthesis for timed automata, NASA Formal Methods, 50-65 (2015), Cham: Springer, Cham · doi:10.1007/978-3-319-17524-9_5 |
| [26] | André, É., Marinho, D., van de Pol, J.: A benchmarks library for extended timed automata. In: Loulergue, F., Wotawa, F. (eds.) TAP (2021). (to appear) |
| [27] | André, É.; Nguyen, HG; Petrucci, L.; Sun, J.; Barrett, C.; Davies, M.; Kahsai, T., Parametric model checking timed automata under non-zenoness assumption, NASA Formal Methods, 35-51 (2017), Cham: Springer, Cham · doi:10.1007/978-3-319-57288-8_3 |
| [28] | André, É., Petrucci, L.: Unifying patterns for modelling timed relationships in systems and properties. In: Moldt, D., Rölke, H., Störrle, H. (eds.) PNSE, vol. 1372, pp. 25-40. CEUR-WS, June 2015 |
| [29] | André, É., Soulat, R.: The Inverse Method. FOCUS Series in Computer Engineering and Information Technology, p. 176, ISTE Ltd and John Wiley & Sons Inc. Hoboken (2013) |
| [30] | André, É.; Sun, J.; Chen, Y-F; Cheng, C-H; Esparza, J., Parametric timed model checking for guaranteeing timed opacity, Automated Technology for Verification and Analysis, 115-130 (2019), Cham: Springer, Cham · Zbl 1437.68110 · doi:10.1007/978-3-030-31784-3_7 |
| [31] | Arias, J.; Budde, CE; Penczek, W.; Petrucci, L.; Sidoruk, T.; Stoelinga, M.; Lin, S-W; Hou, Z.; Mahony, B., Hackers vs. Security: attack-defence trees as asynchronous multi-agent systems, Formal Methods and Software Engineering, 3-19 (2020), Cham: Springer, Cham · doi:10.1007/978-3-030-63406-3_1 |
| [32] | Bagnara, R.; Hill, PM; 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. Programm., 72, 1-2, 3-21 (2008) · doi:10.1016/j.scico.2007.08.001 |
| [33] | Becchi, A.; Zaffanella, E.; Chang, B-YE, Revisiting polyhedral analysis for hybrid systems, Static Analysis, 183-202 (2019), Cham: Springer, Cham · Zbl 1539.68149 · doi:10.1007/978-3-030-32304-2_10 |
| [34] | Becchi, A., Zaffanella, E.: PPLite: zero-overhead encoding of NNC polyhedra. Inf. Comput. 275, 104620 (2020). doi:10.1016/j.ic.2020.104620 · Zbl 1496.68351 |
| [35] | Beneš, N.; Bezděk, P.; Larsen, KG; Srba, J.; Halldórsson, MM; Iwama, K.; Kobayashi, N.; Speckmann, B., Language emptiness of continuous-time parametric timed automata, Automata, Languages, and Programming, 69-81 (2015), Heidelberg: Springer, Heidelberg · Zbl 1440.68150 · doi:10.1007/978-3-662-47666-6_6 |
| [36] | Cassez, F.; Larsen, K.; Palamidessi, C., The impressive power of stopwatches, CONCUR 2000 — Concurrency Theory, 138-152 (2000), Heidelberg: Springer, Heidelberg · Zbl 0999.68112 · doi:10.1007/3-540-44618-4_12 |
| [37] | Chevallier, R.; Encrenaz-Tiphène, E.; Fribourg, L.; Xu, W., Timed verification of the generic architecture of a memory circuit using parametric timed automata, FMSD, 34, 1, 59-81 (2009) · Zbl 1165.68401 · doi:10.1007/s10703-008-0061-x |
| [38] | Fanchon, L., Jacquemard, F.: Formal timing analysis of mixed music scores. In: ICMC. Michigan Publishing, August 2013 |
| [39] | Frehse, G.; Gopalakrishnan, G.; Qadeer, S., SpaceEx: scalable verification of hybrid systems, Computer Aided Verification, 379-395 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-22110-1_30 |
| [40] | 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. doi:10.1109/TIME.2012.10 |
| [41] | Henzinger, TA; Ho, PH; Wong-Toi, H., HyTech: a model checker for hybrid systems, STTT, 1, 1-2, 110-122 (1997) · Zbl 1060.68603 · doi:10.1007/s100090050008 |
| [42] | Larsen, KG; Pettersson, P.; Yi, W., UPPAAL in a nutshell, STTT, 1, 1-2, 134-152 (1997) · Zbl 1060.68577 · doi:10.1007/s100090050010 |
| [43] | Lime, D.; Roux, OH; Seidner, C.; Traonouez, L-M; Kowalewski, S.; Philippou, A., Romeo: a parametric model-checker for petri nets with stopwatches, Tools and Algorithms for the Construction and Analysis of Systems, 54-57 (2009), Heidelberg: Springer, Heidelberg · Zbl 1542.68107 · doi:10.1007/978-3-642-00768-2_6 |
| [44] | Luthmann, L.; Gerecht, T.; Stephan, A.; Bürdek, J.; Lochau, M., Minimum/maximum delay testing of product lines with unbounded parametric real-time constraints, J. Syst. Softw., 149, 535-553 (2019) · doi:10.1016/j.jss.2018.12.028 |
| [45] | 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.) ICECCS, pp. 1-9. IEEE Computer Society, December 2018. doi:10.1109/ICECCS2018.2018.00009 |
| [46] | Sun, Y., André, É., Lipari, G.: Verification of two real-time systems using parametric timed automata. In: Quinton, S., Vardanega, T. (eds.) WATERS, July 2015 |
| [47] | Traonouez, LM; Lime, D.; Roux, OH, Parametric model-checking of stopwatch Petri nets, J. Univ. Comput. Sci., 15, 17, 3273-3304 (2009) · Zbl 1217.68140 · doi:10.3217/jucs-015-17-3273 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
