Parametric Systems : Verification and Synthesis

• Autorzy: Sofronie-Stokkermans Viorica

Identyfikatory

DOI

10.3233/FI-2020-1918

• Języki publikacji: EN

Abstrakty

EN

In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We analyze the possibility of automatically generating such guarantees in the form of constraints on parameters. We illustrate our methods on several examples.

Słowa kluczowe

EN

possibility; suretyship; guaranty

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 173, nr 2-3
• Strony: 91--138
• Opis fizyczny: Bibliogr. 49 poz., rys., tab.

Twórcy

autor

Sofronie-Stokkermans Viorica

• University Koblenz-Landau, Universitätsstr. 1, D-56070 Koblenz, Germany

Bibliografia

• [1] Alur R, Henzinger TA, Ho P. Automatic Symbolic Verification of Embedded Systems. IEEE Trans. Software Eng., 1996. 22(3):181-201. doi:10.1109/32.489079.
• [2] 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, 11th International Workshop, HSCC 2008, St. Louis, MO, USA, April 22-24, 2008. Proceedings, volume 4981 of Lecture Notes in Computer Science. Springer. ISBN 978-3-540-78928-4, 2008 pp. 187-200. doi:10.1007/978-3-540-78929-1_14.
• [3] Wang F. Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures. IEEE Trans. Software Eng., 2005. 31(1):38-51. doi:10.1109/TSE.2005.13.
• [4] Platzer A, Quesel J. European Train Control System: A Case Study in Formal Verification. In: Breitman KK, Cavalcanti A (eds.), Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings, volume 5885 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-10372-8, 2009 pp. 246-265. doi:10.1007/978-3-642-10373-5_13.
• [5] Jacobs S, Sofronie-Stokkermans V. Applications of Hierarchical Reasoning in the Verification of Complex Systems. Electr. Notes Theor. Comput. Sci., 2007. 174(8):39-54. doi:10.1016/j.entcs.2006.11.038.
• [6] Ghilardi S, Nicolini E, Ranise S, Zucchelli D. Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. In: Pfenning F (ed.), Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science. Springer. ISBN 978-3-540-73594-6, 2007 pp. 362-378. doi:10.1007/978-3-540-73595-3_25.
• [7] Hune T, Romijn J, Stoelinga M, Vaandrager FW. Linear parametric model checking of timed automata. J. Log. Algebr. Program., 2002. 52-53:183-220. doi:10.1016/S1567-8326(02)00037-1.
• [8] Cimatti A, Palopoli L, Ramadian Y. Symbolic Computation of Schedulability Regions Using Parametric Timed Automata. In: Proceedings of the 29th IEEE Real-Time Systems Symposium, RTSS 2008, Barcelona, Spain, 30 November - 3 December 2008. IEEE Computer Society. ISBN 978-0-7695-3477-0, 2008 pp. 80-89. doi:10.1109/RTSS.2008.36.
• [9] Cimatti A, Roveri M, Tonetta S. Requirements Validation for Hybrid Systems. In: Bouajjani A, Maler O (eds.), Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-02657-7, 2009 pp. 188-203. doi:10.1007/978-3-642-02658-4_17.
• [10] Alberti F, Ghilardi S, Sharygina N. A Framework for the Verification of Parameterized Infinite-state Systems. Fundam. Inform., 2017. 150(1):1-24. doi:10.3233/FI-2017-1458.
• [11] Bradley AR, Manna Z. Property-directed incremental invariant generation. Formal Asp. Comput., 2008. 20(4-5):379-405. doi:10.1007/s00165-008-0080-9.
• [12] Ghilardi S, Ranise S. Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. Logical Methods in Computer Science, 2010. 6(4).
• [13] Bradley AR. IC3 and beyond: Incremental, Inductive Verification. In: Madhusudan P, Seshia SA (eds.), Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science. Springer, 2012 p. 4. doi:10.1007/978-3-642-31424-7_4.
• [14] Dillig I, Dillig T, Li B, McMillan KL. Inductive invariant generation via abductive inference. In: Hosking AL, Eugster PT, Lopes CV (eds.), Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013. ACM, 2013 pp. 443-456. doi:10.1145/2509136.2509511.
• [15] Kapur D. A Quantifier-Elimination Based Heuristic for Automatically Generating Inductive Assertions for Programs. J. Systems Science & Complexity, 2006. 19(3):307-330. doi:10.1007/s11424-006-0307-x.
• [16] Falke S, Kapur D. When Is a Formula a Loop Invariant? In: Martí-Oliet N, Ölveczky PC, Talcott CL (eds.), Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200 of Lecture Notes in Computer Science. Springer, 2015 pp. 264-286. doi: 10.1007/978-3-319-23165-5_13.
• [17] Padon O, Immerman N, Shoham S, Karbyshev A, Sagiv M. Decidability of inferring inductive invariants. In: Bodík R, Majumdar R (eds.), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. ACM, 2016 pp. 217-231. doi:10.1145/2837614.2837640.
• [18] Karbyshev A, Bjørner N, Itzhaky S, Rinetzky N, Shoham S. Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM, 2017. 64(1):7:1-7:33. doi:10.1145/3022187.
• [19] Sofronie-Stokkermans V. Hierarchical Reasoning for the Verification of Parametric Systems. In: Giesl J, Hähnle R (eds.), Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-14202-4, 2010 pp. 171-187. doi:10.1007/978-3-642-14203-1_15.
• [20] Sofronie-Stokkermans V. Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems. In: Bonacina MP (ed.), Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-38573-5, 2013 pp. 360-376. doi:10.1007/978-3-642-38574-2_25.
• [21] Damm W, Ihlemann C, Sofronie-Stokkermans V. PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata. Mathematics in Computer Science, 2011. 5(4):469-497. doi:10.1007/s11786-011-0098-x.
• [22] Peuter D, Sofronie-Stokkermans V. On Invariant Synthesis for Parametric Systems. In: Fontaine P (ed.), Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science. Springer. ISBN 978-3-030-29435-9, 2019 pp. 385-405. doi:10.1007/978-3-030-29436-6_23.
• [23] Damm W, Horbach M, Sofronie-Stokkermans V. Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata. In: Lutz C, Ranise S (eds.), Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322. Springer. ISBN 978-3-319-24245-3, 2015 pp. 186-202. doi:10.1007/978-3-319-24246-0_12.
• [24] Sofronie-Stokkermans V. Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems. Electr. Notes Theor. Comput. Sci., 2009. 230:161-187. doi:10.1016/j.entcs.2009.02.024.
• [25] Faber J, Ihlemann C, Jacobs S, Sofronie-Stokkermans V. Automatic Verification of Parametric Specifications with Complex Topologies. In: Méry D, Merz S (eds.), Integrated Formal Methods - 8th International Conference, IFM 2010, Nancy, France, October 11-14, 2010. Proceedings, volume 6396 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-16264-0, 2010 pp. 152-167. doi:10.1007/978-3-642-16265-7_12.
• [26] Emerson EA, Srinivasan J. A Decidable Temporal Logic to Reason About Many Processes. In: Dwork C (ed.), Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22-24, 1990. ACM. ISBN 0-89791-404-X, 1990 pp. 233-246. doi:10.1145/93385.93425.
• [27] Abdulla PA, Haziza F, Holík L. All for the Price of Few. In: Giacobazzi R, Berdine J, Mastroeni I (eds.), Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, volume 7737 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-35872-2, 2013 pp. 476-495. doi:10.1007/978-3-642-35873-9_28.
• [28] Jacobs S, Bloem R. Parameterized Synthesis. Logical Methods in Computer Science, 2014. 10(1). doi:10.2168/LMCS-10(1:12)2014.
• [29] Tarski A. A Decision Method for Elementary Algebra and Geometry (2nd ed.). Berkeley, CA: University of California Press, 1951.
• [30] Mal’cev A. Axiomatizable Classes of Locally Free Algebras of Various Types. In: The Metamathematics of Algebraic Systems. Collected Papers: 1936-1967, Studies in Logic and the Foundation of Mathematics, vol. 66, chap. 23. North-Holland, Amsterdam, 1971.
• [31] Chang CC, Keisler HJ. Model theory, Third Edition, volume 73 of Studies in logic and the foundations of mathematics. North-Holland, 1992. ISBN 978-0-444-88054-3.
• [32] Hodges W. A Shorter Model Theory. Cambridge University Press, 1997. ISBN 978-0-521-58713-6.
• [33] Ghilardi S. Model-Theoretic Methods in Combined Constraint Satisfiability. J. Autom. Reasoning, 2004. 33(3-4):221-249. doi:10.1007/s10817-004-6241-5.
• [34] Sofronie-Stokkermans V. Hierarchic Reasoning in Local Theory Extensions. In: Nieuwenhuis R (ed.), Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, volume 3632 of Lecture Notes in Computer Science. Springer. ISBN 3-540-28005-7, 2005 pp. 219-234. doi:10.1007/11532231_16.
• [35] Ganzinger H, Sofronie-Stokkermans V, Waldmann U. Modular proof systems for partial functions with Evans equality. Inf. Comput., 2006. 204(10):1453-1492. doi:10.1016/j.ic.2005.10.002.
• [36] Ihlemann C, Jacobs S, Sofronie-Stokkermans V. On Local Reasoning in Verification. In: Ramakrishnan CR, Rehof J (eds.), Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science. Springer. ISBN 978-3-540-78799-0, 2008 pp. 265-281. doi:10.1007/978-3-540-78800-3_19.
• [37] Ihlemann C, Sofronie-Stokkermans V. On Hierarchical Reasoning in Combinations of Theories. In: Giesl J, Hähnle R (eds.), Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-14202-4, 2010 pp. 30-45. doi:10.1007/978-3-642-14203-1_4.
• [38] Sofronie-Stokkermans V, Ihlemann C. Automated Reasoning in Some Local Extensions of Ordered Structures. Multiple-Valued Logic and Soft Computing, 2007. 13(4-6):397-414. URL http://www.oldcitypublishing.com/journals/mvlsc-home/mvlsc-issue-contents/mvlsc-volume-13-number-4-6-2007/mvlsc-13-4-6-p-397-414/.
• [39] Sofronie-Stokkermans V. Efficient Hierarchical Reasoning about Functions over Numerical Domains. In: Dengel A, Berns K, Breuel TM, Bomarius F, Roth-Berghofer T (eds.), KI 2008: Advances in Artificial Intelligence, 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008. Proceedings, volume 5243 of Lecture Notes in Computer Science. Springer. ISBN 978-3-540-85844-7, 2008 pp. 135-143. doi:10.1007/978-3-540-85845-4_17.
• [40] Ihlemann C, Sofronie-Stokkermans V. System Description: H-PILoT. In: Schmidt RA (ed.), Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-02958-5, 2009 pp. 131-139. doi:10.1007/978-3-642-02959-2_9.
• [41] Sofronie-Stokkermans V. On Interpolation and Symbol Elimination in Theory Extensions. In: Olivetti N, Tiwari A (eds.), Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, volume 9706 of Lecture Notes in Computer Science. Springer. ISBN 978-3-319-40228-4, 2016 pp. 273-289. doi:10.1007/978-3-319-40229-1_19.
• [42] Sofronie-Stokkermans V. On Interpolation and Symbol Elimination in Theory Extensions. Logical Methods in Computer Science, 2018. 14(3). doi:10.23638/LMCS-14(3:23)2018.
• [43] Manna Z, Pnueli A. Temporal verification of reactive systems - safety. Springer, 1995. ISBN 978-0-387-94459-3.
• [44] Dolzmann A, Sturm T. REDLOG: computer algebra meets computer logic. ACM SIGSAM Bulletin, 1997. 31(2):2-9. doi:10.1145/261320.261324.
• [45] Brown CW. QEPCAD B: a system for computing with semi-algebraic sets via cylindrical algebraic decomposition. ACM SIGSAM Bulletin, 2004. 38(1):23-24. doi:10.1145/980175.980185.
• [46] Brown CW. QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 2003. 37(4):97-108. doi:10.1145/968708.968710.
• [47] Damm W, Ihlemann C, Sofronie-Stokkermans V. Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata. In: Caccamo M, Frazzoli E, Grosu R (eds.), Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011. ACM. ISBN 978-1-4503-0629-4, 2011 pp. 73-82. doi:10.1145/1967701.1967714.
• [48] Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Invariant Synthesis for Combined Theories. In: Cook B, Podelski A (eds.), Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings, volume 4349 of Lecture Notes in Computer Science. Springer. ISBN 978-3-540-69735-0, 2007 pp. 378-394. doi:10.1007/978-3-540-69738-1_27.
• [49] Gulwani S, Tiwari A. Constraint-Based Approach for Analysis of Hybrid Systems. In: Gupta A, Malik S (eds.), Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, volume 5123 of Lecture Notes in Computer Science. Springer. ISBN 978-3-540-70543-7, 2008 pp. 190-203. doi:10.1007/978-3-540-70545-1_18.

Uwagi

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