×
Huerta y Munive, Jonathan Julián; Struth, Georg

Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL. (English) Zbl 07498609

J. Autom. Reasoning 66, No. 1, 93-139 (2022).
Summary: We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or invariant sets for vector fields. We introduce the semantic foundations of this framework and summarise their Isabelle formalisation as well as the resulting verification components. A series of simple examples shows our approach at work.

Cited in 1 Document

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Keywords:

hybrid systems; predicate transformers; modal Kleene algebra; hybrid program verification; interactive theorem proving

Software:

Isabelle/HOL; Coquelicot; KeYmaera; C-CoRN; Archive Formal Proofs; RODAS; Algebraic_VCs; KAD; Ordinary Differential Equations; Quantales; Differential_Game_Logic; Transformer semantics; Kleene Algebra; Bellerophon; KeYmaera X
PDF BibTeX XML Cite
\textit{J. J. Huerta y Munive} and \textit{G. Struth}, J. Autom. Reasoning 66, No. 1, 93--139 (2022; Zbl 07498609)
Full Text: DOI

References:

[1] Ábrahám-Mumm, E., Steffen, M., Hannemann, U.: Verification of hybrid systems: Formalization and proof rules in PVS. In: ICECCS 2001, pp. 48-57. IEEE Computer Society (2001) · Zbl 1023.93510
[2] Armstrong, A.; Gomes, VBF; Struth, G., Building program construction and verification tools from algebraic principles, Formal Aspects Comput., 28, 2, 265-293 (2016) · Zbl 1342.68066
[3] Armstrong, A., Struth, G., Weber, T.: Kleene algebra. Archive of Formal Proofs (2013). https://isa-afp.org/entries/Kleene_Algebra.html
[4] Arnol’d, V.I.: Ordinary Differential Equations. Springer, New York (1992)
[5] Back, R.; von Wright, J., Refinement Calculus—A Systematic Introduction (1998), New York: Springer, New York · Zbl 0949.68094
[6] Bohrer, B., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: CPP 2017, pp. 208-221. ACM (2017)
[7] Boldo, S.; Lelay, C.; Melquiond, G., Coquelicot: a user-friendly library of real analysis for Coq, MCS, 9, 1, 41-62 (2015) · Zbl 1322.68176
[8] Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-corn, the constructive Coq repository at Nijmegen. In: MKM 2004, volume 3119 of LNCS, pp. 88-103. Springer (2004) · Zbl 1108.68586
[9] Desharnais, J.; Struth, G., Internal axioms for domain semirings, Sci. Comput. Program., 76, 3, 181-203 (2011) · Zbl 1211.68242
[10] Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Handbook of Model Checking., pp. 1047-1110. Springer (2018) · Zbl 1392.68246
[11] Foster, S., Huerta y Munive, J.J., Struth, G.: Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. In: RAMiCS 2020, pp. 169-186 (2020) · Zbl 07578341
[12] Foster, S., y Munive, J.J.H., Gleirscher, M., Struth, G.: Hybrid systems verification with isabelle/HOL: simpler syntax, better models, faster proofs. CoRR, abs/2106.05987 (2021)
[13] Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: Tactical theorem proving for hybrid systems. In: ITP 2017, LNCS, pp. 207-224. Springer (2017) · Zbl 1483.68191
[14] Fulton, N., Mitsch, S., Quesel, J., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: CADE-25, volume 9195 of LNCS, pp. 527-538. Springer (2015) · Zbl 1465.68281
[15] Gierz, G.; Hofmann, KH; Lawson, JD; Mislove, M.; Scott, DS, A Compendium of Continuous Lattices (1980), New York: Springer, New York · Zbl 0452.06001
[16] Gomes, V.B.F., Guttmann, W., Höfner, P., Struth, G., Weber, T.: Kleene algebras with domain. Archive of Formal Proofs (2016). https://isa-afp.org/entries/KAD.html
[17] Gomes, V.B.F., Struth, G.: Modal Kleene algebra applied to program correctness. In: FM 2016, volume 9995 of LNCS, pp. 310-325 (2016) · Zbl 1427.68046
[18] Gomes, V.B.F., Struth, G.: Program construction and verification components based on Kleene algebra. In: Archive of Formal Proofs (2016)
[19] Gordon, MJC, Mechanizing Programming Logics in Higher Order Logic, 387-439 (1989), New York: Springer, New York
[20] Hairer, E.; Wanner, G., Solving Ordinary Differential Equations II: Stiff and Differential-Algebraic Problems (1996), New York: Springer, New York · Zbl 1192.65097
[21] Harel, D.; Kozen, D.; Tiuryn, J., Dynamic Logic (2000), Cambridge: MIT Press, Cambridge
[22] Hirsch, MW; Smale, S.; Devaney, RL, Differential Equations, Dynamical Systems, and Linear Algebra (1974), London: Academic Press, London · Zbl 0309.34001
[23] Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: ITP 2013, volume 7998 of LNCS, pp. 279-294. Springer (2013) · Zbl 1317.68213
[24] Hubbard, JH; West, BH, Differential Equations: A Dynamical Systems Approach (1991), New York: Springer, New York
[25] Huerta y Munive, J.J.: Verification components for hybrid systems. Archive of Formal Proofs (2019). https://isa-afp.org/entries/Hybrid_Systems_VCs.html
[26] Huerta y Munive, J.J.: Affine systems of ODEs in Isabelle/HOL for hybrid-program verification. In: SEFM 2020, volume 12310 of LNCS, pp. 77-92. Springer (2020) · Zbl 1476.68301
[27] Huerta y Munive, J.J.: Algebraic verification of hybrid systems in Isabelle/HOL. PhD thesis, University of Sheffield (2021) · Zbl 1476.68301
[28] Huerta y Munive, J.J., Struth, G.: Verifying hybrid systems with modal Kleene algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science, pp. 225-243. Springer (2018) · Zbl 1518.68209
[29] Immler, F., Hölzl, J.: Numerical analysis of ordinary differential equations in Isabelle/HOL. In: ITP 2012, volume 7406 of LNCS, pp. 377-392. Springer (2012) · Zbl 1360.68753
[30] Immler, F., Hölzl, J.: Ordinary differential equations. Archive of Formal Proofs (2012). https://isa-afp.org/entries/Ordinary_Differential_Equations.html · Zbl 1360.68753
[31] Immler, F.; Traut, C., The flow of ODEs: formalization of variational equation and Poincaré map, J. Autom. Reason., 62, 2, 215-236 (2019) · Zbl 1468.68325
[32] Jacobs, B.: A recipe for state-and-effect triangles. In: Logical Methods in Computer Science, vol. 13, no. 2 (2017) · Zbl 1448.68220
[33] Jeannin, J.; Ghorbal, K.; Kouskoulas, Y.; Schmidt, A.; Gardner, R.; Mitsch, S.; Platzer, A., A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system, STTT, 19, 6, 717-741 (2017)
[34] John, F., Partial Differential Equations (1986), New York: Springer, New York
[35] Jónsson, B.; Tarski, A., Boolean algebras with operators, Part I. Americal, J. Math., 73, 4, 207-215 (1951) · Zbl 0045.31505
[36] Kneser, H.: Über die Lösungen eines Systems gewöhnlicher Differentialgleichungen, das der Lipschitzschen Bedingung nicht genügt. Sitz.ber. Preuß, pp. 58-61 (1923) · JFM 49.0302.03
[37] Kozen, D., Kleene algebra with tests, ACM TOPLAS, 19, 3, 427-443 (1997)
[38] Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: APLAS 2010, volume 6461 of LNCS, pp. 1-15. Springer (2010)
[39] Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds) EMSOFT 2011, pp. 97-106. ACM (2011)
[40] Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: Hybrid, distributed, and now formally verified. In: FM 2011, volume 6664 of LNCS, pp. 42-56. Springer (2011)
[41] MacLane, S., Categories for the Working Mathematician (1971), New York: Springer, New York · Zbl 0705.18001
[42] Makarov, E., Spitters, B.: The Picard algorithm for ordinary differential equations in Coq. In: ITP 2013, volume 7998 of LNCS, pp. 463-468. Springer (2013) · Zbl 1317.68222
[43] Manes, EG, Predicate Transformer Semantics (1992), Cambridge: Cambridge University Press, Cambridge · Zbl 0784.68003
[44] Meijer, E., Fokkinga, M.M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: Functional Programming Languages and Computer Architecture 1991, volume 523 of LNCS. Springer (1991)
[45] Mitsch, S., Huerta y Munive, J.J., Jin, X., Zhan, B., Wang, S., Zhan, N.: ARCH-COMP20 category report: Hybrid systems theorem proving. In: ARCH20, pp. 141-161 (2019)
[46] Platzer, A.: The structure of differential invariants and differential cut elimination. In: LMCS, vol. 8, no. 4 (2008) · Zbl 1261.03112
[47] Platzer, A., Logical Analysis of Hybrid Systems (2010), New York: Springer, New York · Zbl 1211.68412
[48] Platzer, A., A complete uniform substitution calculus for differential dynamic logic, J. Autom. Reason., 59, 2, 219-265 (2017) · Zbl 1437.03119
[49] Platzer, A., Logical Foundations of Cyber-Physical Systems (2018), New York: Springer, New York · Zbl 1400.93003
[50] Platzer, A.: Differential game logic. Archive of Formal Proofs (2019). https://isa-afp.org/entries/Differential_Game_Logic.html
[51] Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: LICS, pp. 819-828. ACM (2018) · Zbl 1453.03026
[52] Preoteasa, V.: Algebra of monotonic Boolean transformers. Archive of Formal Proofs (2011). https://isa-afp.org/entries/MonoBoolTranAlgebra.html · Zbl 1349.68051
[53] Preoteasa, V.: Algebra of monotonic boolean transformers. In: Archive of Formal Proofs (2011) · Zbl 1349.68051
[54] Rebiha, R.; Moura, AV; Matringe, N., Generating invariants for non-linear hybrid systems, Theor. Comput. Sci., 594, 180-200 (2015) · Zbl 1328.68130
[55] Rosenthal, KI, The Theory of Quantaloids (1996), London: Chapman and Hall/CRC, London · Zbl 0845.18003
[56] Rosenthal, KL, Quantales and Their Applications (1990), Essex: Longman Scientific & Technical, Essex · Zbl 0703.06007
[57] Rouhling, D.: A formal proof in Coq of a control function for the inverted pendulum. In: CPP 2018, pp. 28-41. ACM (2018)
[58] Sassi, M. A. B., Girard, A., Sankaranarayanan, S.: Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: CDC 2014, pp. 6348-6353. IEEE (2014)
[59] Slagel, J.T., White, L., Dutle, A.: Formal verification of semi-algebraic sets and real analytic functions. In: CPP 21, pp. 278-290. ACM (2021)
[60] Sogokon, A., Mitsch, S., Tan, Y.K., Cordwell, K., Platzer, A.: Pegasus: A framework for sound continuous invariant generation. In: FM 2019, LNCS, pp. 138-157. Springer (2019)
[61] Struth, G., On the expressive power of Kleene algebra with domain, Inf. Process. Lett., 116, 4, 284-288 (2016) · Zbl 1347.68095
[62] Struth, G., Hoare semigroups, Math. Struct. Comput. Sci., 28, 6, 775-799 (2018) · Zbl 1390.68440
[63] Struth, G.: Properties of orderings and lattices. In: Archive of Formal Proofs (2018)
[64] Struth, G.: Quantales. In: Archive of Formal Proofs (2018)
[65] Struth, G.: Transformer semantics. Archive of Formal Proofs (2018). https://isa-afp.org/entries/Transformer_Semantics.html
[66] Teschl, G.: Ordinary Differential Equations and Dynamical Systems. AMS (2012) · Zbl 1263.34002
[67] Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: ICFEM 2015, pp. 382-399 (2015)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.