HHLPy: practical verification of hybrid systems using Hoare logic. (English) Zbl 1529.68164
Chechik, Marsha (ed.) et al., Formal methods. 25th international symposium, FM 2023, Lübeck, Germany, March 6–10, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14000, 160-178 (2023).
Summary: We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP programs with pre- and postconditions, invariants, and proof rules for reasoning about ordinary differential equations. Verification conditions are generated from the annotations following the rules of a Hoare logic for hybrid systems. We designed labeling and highlighting mechanisms to distinguish and visualize different verification conditions. The tool is implemented in Python and has a web-based user interface. We evaluated the effectiveness of the tool on translations of Simulink/Stateflow models and on KeYmaera X benchmarks.
For the entire collection see [Zbl 1517.68007].
For the entire collection see [Zbl 1517.68007].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B70 | Logic in computer science |
References:
| [1] | Bohrer, R., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) Conference on Certified Programs and Proofs (CPP 2017), pp. 208-221. ACM (2017) |
| [2] | Chen, M.; Hinchey, MG; Bowen, JP; Olderog, E-R, MARS: a toolchain for modelling, analysis and verification of hybrid systems, Provably Correct Systems, 39-58 (2017), Cham: Springer, Cham · doi:10.1007/978-3-319-48628-4_3 |
| [3] | Dijkstra, EW, Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, 18, 8, 453-457 (1975) · Zbl 0308.68017 · doi:10.1145/360933.360975 |
| [4] | Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976) · Zbl 0368.68005 |
| [5] | Filliâtre, J-C; Paskevich, A.; Felleisen, M.; Gardner, P., Why3—where programs meet provers, Programming Languages and Systems, 125-128 (2013), Heidelberg: Springer, Heidelberg · Zbl 1435.68366 · doi:10.1007/978-3-642-37036-6_8 |
| [6] | Foster, S.; Huerta y. Munive, JJ; Gleirscher, M.; Struth, G.; Huisman, M.; Păsăreanu, C.; Zhan, N., Hybrid systems verification with Isabelle/HOL: simpler syntax, better models, faster proofs, Formal Methods, 367-386 (2021), Cham: Springer, Cham · doi:10.1007/978-3-030-90870-6_20 |
| [7] | Foster, S.; Huerta y. Munive, JJ; Struth, G.; Fahrenberg, U.; Jipsen, P.; Winter, M., Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL, Relational and Algebraic Methods in Computer Science, 169-186 (2020), Cham: Springer, Cham · Zbl 07578341 · doi:10.1007/978-3-030-43520-2_11 |
| [8] | Fulton, N.; Mitsch, S.; Bohrer, B.; Platzer, A.; Ayala-Rincón, M.; Muñoz, CA, Bellerophon: tactical theorem proving for hybrid systems, Interactive Theorem Proving, 207-224 (2017), Cham: Springer, Cham · Zbl 1483.68191 · doi:10.1007/978-3-319-66107-0_14 |
| [9] | Fulton, N.; Mitsch, S.; Quesel, J-D; Völp, M.; Platzer, A.; Felty, AP; Middeldorp, A., KeYmaera X: an axiomatic tactical theorem prover for hybrid systems, Automated Deduction - CADE-25, 527-538 (2015), Cham: Springer, Cham · Zbl 1465.68281 · doi:10.1007/978-3-319-21401-6_36 |
| [10] | Goncharov, S., Neves, R.: An adequate while-language for hybrid computation. In: Komendantskaya, E. (ed.) International Symposium on Principles and Practice of Programming Languages (PPDP 2019), pp. 11:1-11:15. ACM (2019) |
| [11] | Guo, P.; Zhan, B.; Xu, X.; Wang, S.; Sun, W., Translating a large subset of Stateflow to hybrid CSP with code optimization, J. Syst. Archit., 130 (2022) · doi:10.1016/j.sysarc.2022.102665 |
| [12] | Jacobs, B.; Smans, J.; Philippaerts, P.; Vogels, F.; Penninckx, W.; Piessens, F.; Bobaru, M.; Havelund, K.; Holzmann, GJ; Joshi, R., VeriFast: a powerful, sound, predictable, fast verifier for C and Java, NASA Formal Methods, 41-55 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-20398-5_4 |
| [13] | Jifeng, H.: From CSP to hybrid systems, pp. 171-189. Prentice Hall International (UK) Ltd., GBR (1994) |
| [14] | Kekatos, N.: Verifying a cruise control system using Simulink and SpaceEx. CoRR abs/2101.00102 (2021) |
| [15] | Leino, KRM; Clarke, EM; Voronkov, A., Dafny: an automatic program verifier for functional correctness, Logic for Programming, Artificial Intelligence, and Reasoning, 348-370 (2010), Heidelberg: Springer, Heidelberg · Zbl 1253.68095 · doi:10.1007/978-3-642-17511-4_20 |
| [16] | Liebrenz, T.; Herber, P.; Glesner, S.; Sun, J.; Sun, M., Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X, Formal Methods and Software Engineering, 89-105 (2018), Cham: Springer, Cham · doi:10.1007/978-3-030-02450-5_6 |
| [17] | Mitsch, S., Jin, X., Zhan, B., Wang, S., Zhan, N.: ARCH-COMP21 category report: hybrid systems theorem proving. In: Frehse, G., Althoff, M. (eds.) International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2021). EPiC Series in Computing, vol. 80, pp. 120-132. EasyChair (2021) |
| [18] | Moggi, E., Notions of computation and monads, Inf. Comput., 93, 1, 55-92 (1991) · Zbl 0723.68073 · doi:10.1016/0890-5401(91)90052-4 |
| [19] | de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [20] | Huerta y. Munive, JJ; de Boer, F.; Cerone, A., Affine systems of ODEs in Isabelle/HOL for hybrid-program verification, Software Engineering and Formal Methods, 77-92 (2020), Cham: Springer, Cham · Zbl 1476.68301 · doi:10.1007/978-3-030-58768-0_5 |
| [21] | Huerta y. Munive, JJ; Struth, G.; Desharnais, J.; Guttmann, W.; Joosten, S., Verifying hybrid systems with modal Kleene algebra, Relational and Algebraic Methods in Computer Science, 225-243 (2018), Cham: Springer, Cham · Zbl 1518.68209 · doi:10.1007/978-3-030-02149-8_14 |
| [22] | Huerta y. Munive, JJ; Struth, G., Predicate transformer semantics for hybrid systems, J. Autom. Reason., 66, 1, 93-139 (2021) · Zbl 07498609 · doi:10.1007/s10817-021-09607-x |
| [23] | Platzer, A., Differential dynamic logic for hybrid systems, J. Autom. Reason., 41, 2, 143-189 (2008) · Zbl 1181.03035 · doi:10.1007/s10817-008-9103-8 |
| [24] | Platzer, A., A complete uniform substitution calculus for differential dynamic logic, J. Autom. Reason., 59, 2, 219-265 (2017) · Zbl 1437.03119 · doi:10.1007/s10817-016-9385-1 |
| [25] | Platzer, A., Logical Foundations of Cyber-Physical Systems (2018), Cham: Springer, Cham · Zbl 1400.93003 · doi:10.1007/978-3-319-63588-0 |
| [26] | Platzer, A.; Quesel, J-D; Armando, A.; Baumgartner, P.; Dowek, G., KeYmaera: a hybrid theorem prover for hybrid systems (system description), Automated Reasoning, 171-178 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68469 · doi:10.1007/978-3-540-71070-7_15 |
| [27] | Platzer, A., Tan, Y.K.: Differential equation invariance axiomatization. J. ACM 67(1), 6:1-6:66 (2020) · Zbl 1494.03079 |
| [28] | Sheng, H., Bentkamp, A., Zhan, B.: HHLPy: practical verification of hybrid systems using Hoare logic (full paper). CoRR abs/2210.17163 (2022). doi:10.48550/arXiv.2210.17163 |
| [29] | Wang, S.; Zhan, N.; Zou, L.; Butler, M.; Conchon, S.; Zaïdi, F., An improved HHL prover: an interactive theorem prover for hybrid systems, Formal Methods and Software Engineering, 382-399 (2015), Cham: Springer, Cham · doi:10.1007/978-3-319-25423-4_25 |
| [30] | Wolfram Research Inc.: Wolfram Engine, Version 13.1, Champaign, IL (2022). https://www.wolfram.com/engine |
| [31] | Xu, X.; Zhan, B.; Wang, S.; Talpin, JP; Zhan, N., A denotational semantics of Simulink with higher-order UTP, J. Log. Algebraic Methods Program., 130 (2023) · Zbl 07618116 · doi:10.1016/j.jlamp.2022.100809 |
| [32] | Zhan, N.; Wang, S.; Zhao, H., Formal Verification of Simulink/Stateflow Diagrams (2017), Cham: Springer, Cham · Zbl 1412.68006 · doi:10.1007/978-3-319-47016-0 |
| [33] | Chaochen, Z.; Ji, W.; Ravn, AP; Alur, R.; Henzinger, TA; Sontag, ED, A formal description of hybrid systems, Hybrid Systems III, 511-530 (1996), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0020972 |
| [34] | Zou, L.; Zhan, N.; Wang, S.; Fränzle, M.; Finkbeiner, B.; Pu, G.; Zhang, L., Formal verification of Simulink/Stateflow diagrams, Automated Technology for Verification and Analysis, 464-481 (2015), Cham: Springer, Cham · Zbl 1471.68159 · doi:10.1007/978-3-319-24953-7_33 |
| [35] | Zou, L., Zhan, N., Wang, S., Fränzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid Hoare logic prover. In: Ernst, R., Sokolsky, O. (eds.) International Conference on Embedded Software, (EMSOFT 2013), pp. 9:1-9:10. IEEE (2013) |
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.
