Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction

• Autorzy: Cassez Franck , Jensen Peter Gjøl , Guldstrand Larsen Kim

Identyfikatory

DOI

10.3233/FI-2021-1997

• Języki publikacji: EN

Abstrakty

EN

We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

Słowa kluczowe

EN

machine theory; hybrid systems; Petri nets; algorithms

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 178, nr 1/2
• Strony: 31--57
• Opis fizyczny: Bibliogr. 35 poz., rys., tab.

Twórcy

autor

Cassez Franck

• Department of Computing, Macquarie University, Sydney, Australia

autor

Jensen Peter Gjøl

• Department of Computer Science, Aalborg University, Denmark

autor

Guldstrand Larsen Kim

• Department of Computer Science, Aalborg University, Denmark

Bibliografia

• [1] Cassez F, Jensen PG, Guldstrand Larsen K. Refinement of Trace Abstraction for Real-Time Programs. In: Hague M, Potapov I (eds.), Reachability Problems. Springer International Publishing, Cham, 2017 pp. 42-58. ISBN: 978-3-319-67089-8.
• [2] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided Abstraction Refinement. In: Emerson EA, Sistla AP (eds.), Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science. Springer. ISBN: 3-540-67770-4, 2000 pp. 154-169. doi:10.1007/10722167\_15.
• [3] Heizmann M, Hoenicke J, Podelski A. Refinement of Trace Abstraction. In: Palsberg J, Su Z (eds.), Static Analysis, 16th International Symposium, SAS 2009, Los Angeles, CA, USA, August 9-11, 2009. Proceedings, volume 5673 of Lecture Notes in Computer Science. Springer. ISBN: 978-3-642-03236-3, 2009 pp. 69-85. doi:10.1007/978-3-642-03237-0\_7.
• [4] Heizmann M, Hoenicke J, Podelski A. Software Model Checking for People Who Love Automata. In: Sharygina N, Veith H (eds.), CAV, volume 8044 of LNCS. Springer, 2013 pp. 36-52. ISBN: 978-3-642-39798-1.
• [5] Beyer D, Huisman M, Kordon F, Steffen B (eds.). Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science. Springer, 2019. ISBN: 978-3-030-17501-6. doi:10.1007/978-3-030-17502-3.
• [6] Alur R, Dill DL. A Theory of Timed Automata. Theor. Comput. Sci., 1994. 126(2):183-235. doi:10.1016/0304-3975(94)90010-8.
• [7] Behrmann G, David A, Larsen K, Hakansson J, Petterson P, Yi W, Hendriks M. UPPAAL 4.0. In: QEST’06. 2006 pp. 125-126. doi:10.1109/QEST.2006.59.
• [8] Cassez F, Larsen KG. The Impressive Power of Stopwatches. In: Palamidessi C (ed.), CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science. Springer, 2000 pp. 138-152. doi:10.1007/3-540-44618-4_12.
• [9] Henzinger TA, Kopke PW, Puri A, Varaiya P. What’s Decidable about Hybrid Automata? Journal of Computer and System Sciences, 1998. 57(1):94-124. doi:http://dx.doi.org/10.1006/jcss.1998.1581.
• [10] Frehse G. PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari M, Thiele L (eds.), Hybrid Systems: Computation and Control, volume 3414 of Lecture Notes in Computer Science, pp. 258-273. Springer Berlin Heidelberg. ISBN: 978-3-540-25108-8, 2005. doi:10.1007/978-3-540-31954-2_17.
• [11] Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O. SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan G, Qadeer S (eds.), Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pp. 379-395. Springer Berlin Heidelberg. ISBN: 978-3-642-22109-5, 2011. doi:10.1007/978-3-642-22110-1_30.
• [12] Henzinger TA, Ho PH, Wong-toi H. HyTech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer, 1997. 1:460-463.
• [13] Wang W, Jiao L. Trace Abstraction Refinement for Timed Automata. In: Cassez F, Raskin J (eds.), Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science. Springer. ISBN: 978-3-319-11935-9, 2014 pp. 396-410. doi:10.1007/978-3-319-11936-6\_28.
• [14] Alur R, Dang T, Ivančić F. Reachability Analysis of Hybrid Systems via Predicate Abstraction. In: Tomlin CJ, Greenstreet MR (eds.), Hybrid Systems: Computation and Control. Springer Berlin Heidelberg, Berlin, Heidelberg, 2002 pp. 35-48.
• [15] Dierks H, Kupferschmid S, Larsen KG. Automatic abstraction refinement for timed automata. In: International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 2007 pp. 114-129.
• [16] Frehse G, Jha SK, Krogh BH. A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata. In: Egerstedt M, Mishra B (eds.), Hybrid Systems: Computation and Control. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008 pp. 187-200.
• [17] Tiwari A. Abstractions for hybrid systems. Formal Methods in System Design, 2008. 32(1):57-83. doi:10.1007/s10703-007-0044-3.
• [18] Bradley AR. SAT-Based Model Checking without Unrolling. In: Jhala R, Schmidt D (eds.), Verification, Model Checking, and Abstract Interpretation. Springer Berlin Heidelberg, Berlin, Heidelberg. 2011 pp. 70-87. ISBN: 978-3-642-18275-4.
• [19] Bozzano M, Cimatti A, Griggio A, Mattarei C. Efficient Anytime Techniques for Model-Based Safety Analysis. In: Kroening D, Păsăreanu CS (eds.), Computer Aided Verification. Springer International Publishing, Cham. 2015 pp. 603-621. ISBN: 978-3-319-21690-4.
• [20] Bérard B, Fribourg L. Reachability Analysis of (Timed) Petri Nets Using Real Arithmetic. In: Baeten JCM, Mauw S (eds.), CONCUR’99 Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg. 1999 pp. 178-193. ISBN: 978-3-540-48320-5.
• [21] Cimatti A, Griggio A, Mover S, Tonetta S. Parameter synthesis with IC3. In: 2013 Formal Methods in Computer-Aided Design. 2013 pp. 165-168. doi:10.1109/FMCAD.2013.6679406.
• [22] Kafle B, Gallagher JP, Gange G, Schachte P, Søndergaard H, Stuckey PJ. An iterative approach to precondition inference using constrained Horn clauses. CoRR, 2018. abs/1804.05989. 1804.05989, URL http://arxiv.org/abs/1804.05989.
• [23] Kordy P, Langerak R, Mauw S, Polderman JW. A Symbolic Algorithm for the Analysis of Robust Timed Automata. In: Jones CB, Pihlajasaari P, Sun J (eds.), FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science. Springer. ISBN: 978-3-319-06409-3, 2014 pp. 351-366. doi:10.1007/978-3-319-06410-9\_25.
• [24] Sankur O. Symbolic Quantitative Robustness Analysis of Timed Automata. In: Baier C, Tinelli C (eds.), Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science. Springer. ISBN: 978-3-662-46680-3, 2015 pp. 484-498. doi:10.1007/978-3-662-46681-0\_48.
• [25] 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: Formal Methods: 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN: 978-3-642-32759-9, 2012 pp. 33-36. doi:10.1007/978-3-642-32759-9_6.
• [26] Bérard B, Cassez F, Haddad S, Lime D, Roux OH. Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: Pettersson P, Yi W (eds.), Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings, volume 3829 of Lecture Notes in Computer Science. Springer, 2005 pp. 211-225. doi:10.1007/11603009_17.
• [27] Cassez F, Roux OH. Structural Translation from Time Petri Nets to Timed Automata. Journal of Software and Systems, 2006. 79(10):1456-1468.
• [28] Bérard B, Cassez F, Haddad S, Lime D, Roux OH. The expressive power of time Petri nets. Theoretical Computer Science, 2013. 474:1-20. doi:http://dx.doi.org/10.1016/j.tcs.2012.12.005.
• [29] Byg J, Jacobsen M, Jacobsen L, Jørgensen K, Møller M, Srba J. TCTL-Preserving Translations from Timed-Arc Petri Nets to Networks of Timed Automata. TCS, 2013. doi:10.1016/j.tcs.2013.07.011.
• [30] Dietsch D, Heizmann M, Musa B, Nutz A, Podelski A. Craig vs. Newton in software model checking. In: Bodden E, Schäfer W, van Deursen A, Zisman A (eds.), Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017. ACM. ISBN: 978-1-4503-5105-8, 2017 pp. 487-497. doi:10.1145/3106237.3106307.
• [31] De Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08. Springer-Verlag, Berlin, Heidelberg. ISBN: 3-540-78799-2, 978-3-540-78799-0, 2008 pp. 337-340. URL http://dl.acm.org/citation.cfm?id=1792734.1792766.
• [32] Jensen PG, Cassez F, Larsen KG. Repeatability for ”Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction”, 2020. doi:10.5281/zenodo.3952856.
• [33] André É, Lipari G, Nguyen HG, Sun Y. Reachability Preservation Based Parameter Synthesis for Timed Automata. In: Havelund K, Holzmann G, Joshi R (eds.), NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. Springer International Publishing, Cham. ISBN: 978-3-319-17524-9, 2015 pp. 50-65. doi:10.1007/978-3-319-17524-9_5.
• [34] Cassez F, Ziegler F. Verification of Concurrent Programs Using Trace Abstraction Refinement. In: Davis M, Fehnker A, McIver A, Voronkov A (eds.), Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science. Springer. ISBN: 978-3-662-48898-0, 2015 pp. 233-248. doi:10.1007/978-3-662-48899-7_17.
• [35] Cassez F, Müller C, Burnett K. Summary-Based Inter-Procedural Analysis via Modular Trace Refinement. In: Raman V, Suresh SP (eds.), 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. ISBN: 978-3-939897-77-4, 2014 pp. 545-556. doi:10.4230/LIPIcs.FSTTCS.2014.545.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).