Skip to main content
SpringerLink
Log in

Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL

  • Conference paper
  • First Online:
Relational and Algebraic Methods in Computer Science (RAMiCS 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12062))

Abstract

We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasoning about the program structure and generating verification conditions at this level. Lenses capture hybrid program stores in a generic algebraic way. The approach has been formalised with the Isabelle/HOL proof assistant. Several examples explain the workflow with the resulting verification components.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/yonoteam/HybridKATpaper.

  2. 2.

    We therefore often write ;  for this operation in later sections.

  3. 3.

    https://www.cs.york.ac.uk/circus/CyPhyAssure/.

References

  1. Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Rechnical Report 2001–1844, Computer Science Department, Cornell University (2001)

    Google Scholar 

  2. Armstrong, A., Gomes, V.B.F., Struth, G.: Kleene algebra with tests and demonic refinement algebras. Archive of Formal Proofs (2014)

    Google Scholar 

  3. Armstrong, A., Gomes, V.B.F., Struth, G.: Building program construction and verification tools from algebraic principles. Formal Aspects Comput. 28(2), 265–293 (2016)

    Article  MathSciNet  Google Scholar 

  4. Back, R., von Wright, J.: Refinement Calculus–A Systematic Introduction. Springer, New York (1998). https://doi.org/10.1007/978-1-4612-1674-2

    Book  MATH  Google Scholar 

  5. Bohrer, B., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: CPP 2017, pp. 208–221. ACM (2017)

    Google Scholar 

  6. Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. Handbook of Model Checking, pp. 1047–1110. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_30

    Chapter  MATH  Google Scholar 

  7. Foster, S.: Hybrid relations in Isabelle/UTP. In: Ribeiro, P., Sampaio, A. (eds.) UTP 2019. LNCS, vol. 11885, pp. 130–153. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31038-7_7

    Chapter  Google Scholar 

  8. Foster, S., Zeyda, F.: Optics in Isabelle/HOL. Archive of Formal Proofs (2018)

    Google Scholar 

  9. Foster, S., Zeyda, F., Nemouchi, Y., Ribeiro, P., Wolff, B.: Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming. Archive of Formal Proofs (2019)

    Google Scholar 

  10. Foster, S., Zeyda, F., Woodcock, J.: Unifying heterogeneous state-spaces with lenses. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 295–314. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_17

    Chapter  Google Scholar 

  11. Furusawa, H., Struth, G.: Binary multirelations. Archive of Formal Proofs (2015)

    Google Scholar 

  12. Furusawa, H., Struth, G.: Taming multirelations. ACM TOCL 17(4), 28:1–28:34 (2016)

    Google Scholar 

  13. Gomes, V.B.F., Struth, G.: Program construction and verification components based on Kleene algebra. Archive of Formal Proofs (2016)

    Google Scholar 

  14. Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279–294. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_21

    Chapter  Google Scholar 

  15. Huerta y Munive, J.J.:: Verification components for hybrid systems. Archive of Formal Proofs (2019)

    Google Scholar 

  16. Huerta y Munive, J.J., Struth, G.: Predicate transformer semantics for hybrid systems: verification components for Isabelle/HOL. arXiv:1909.05618 [cs.LO] (2019)

  17. Immler, F., Hölzl, J.: Ordinary differential equations. Archive of Formal Proofs (2012)

    Google Scholar 

  18. Immler, F., Traut, C.: The flow of ODEs: formalization of variational equation and Poincaré map. J. Autom. Reasoning 62(2), 215–236 (2019)

    Article  Google Scholar 

  19. Kozen, D.: Kleene algebra with tests. ACM TOPLAS 19(3), 427–443 (1997)

    Article  MathSciNet  Google Scholar 

  20. Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM TOCL 1(1), 60–76 (2000)

    Article  MathSciNet  Google Scholar 

  21. Kozen, D., Cohen, E., Smith, F.: The complexity of Kleene algebra with tests. Technical report TR96-1598, Computer Science Department, Cornell University (1996)

    Google Scholar 

  22. Liu, J., et al.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17164-2_1

    Chapter  Google Scholar 

  23. Loos, S.M., Platzer, A.: Differential refinement logic. In: LICS 2016, pp. 505–514. ACM (2016)

    Google Scholar 

  24. Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoret. Comput. Sci. 351(2), 221–239 (2006)

    Article  MathSciNet  Google Scholar 

  25. Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Upper Saddle River (1994)

    MATH  Google Scholar 

  26. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63588-0

    Book  MATH  Google Scholar 

  27. Struth, G.: Hoare semigroups. Math. Struct. Comput. Sci. 28(6), 775–799 (2018)

    Article  MathSciNet  Google Scholar 

  28. Teschl, G.: Ordinary Differential Equations and Dynamical Systems. AMS (2012)

    Google Scholar 

Download references

Acknowledgements

The authors wish to thank the reviewers for their very thorough and insightful comments, and to Sergey Goncharov and André Platzer for discussions on a preliminary version. The second author is sponsored by CONACYT’s scholarship no. 440404; the first author is supported by the EPSRC project CyPhyAssureFootnote 3 (Grant EP/S001190/1).

Author information

Authors and Affiliations

  1. University of York, York, UK

    Simon Foster

  2. University of Sheffield, Sheffield, UK

    Jonathan Julián Huerta y Munive & Georg Struth

Authors
  1. Simon Foster
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jonathan Julián Huerta y Munive
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Georg Struth
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jonathan Julián Huerta y Munive .

Editor information

Editors and Affiliations

  1. Laboratoire d’informatique (LIX), École Polytechnique, Palaiseau, France

    Uli Fahrenberg

  2. Faculty of Mathematics, Chapman University, Orange, CA, USA

    Peter Jipsen

  3. Department of Computer Science, Brock University, St. Catharines, ON, Canada

    Michael Winter

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Foster, S., Huerta y Munive, J.J., Struth, G. (2020). Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL. In: Fahrenberg, U., Jipsen, P., Winter, M. (eds) Relational and Algebraic Methods in Computer Science. RAMiCS 2020. Lecture Notes in Computer Science(), vol 12062. Springer, Cham. https://doi.org/10.1007/978-3-030-43520-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-43520-2_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-43519-6

  • Online ISBN: 978-3-030-43520-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation