Towards an implementation of differential dynamic logic in PVS
Authors: 
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, Lauren WhiteAuthors Info & Claims
Pages 44 - 50
Abstract
This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.
References
[1]
Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen. 2001. Verification of hybrid systems: Formalization and proof rules in PVS. In Proceedings Seventh IEEE International Conference on Engineering of Complex Computer Systems. 48–57. https://doi.org/10.1109/ICECCS.2001.930163
[2]
Swee Balachandran, Christopher Manderino, César Muñoz, and María Consiglio. 2020. A decentralized framework to support uas merging and spacing operations in urban canyons. In 2020 International Conference on Unmanned Aircraft Systems (ICUAS). 204–210. https://doi.org/10.1109/ICUAS48674.2020.9213973
[3]
Swee Balachandran, César Muñoz, and María Consiglio. 2018. Distributed consensus to enable merging and spacing of UAS in an urban environment. In 2018 International Conference on Unmanned Aircraft Systems (ICUAS). 670–675. https://doi.org/10.1109/ICUAS.2018.8453460
[4]
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer. 2017. Formally verified differential dynamic logic. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. 208–221. https://doi.org/10.1145/3018610.3018616
[5]
Marc Daumas, David Lester, and César Munoz. 2008. Verified real number calculations: A library for interval arithmetic. IEEE Trans. Comput., 58, 2 (2008), 226–237. https://doi.org/10.1109/tc.2008.213
[6]
Guillaume Dupont. 2021. Correct-by-construction design of hybrid systems based on refinement and proof. Ph.D. Dissertation. https://oatao.univ-toulouse.fr/28190/1/Dupont_Guillaume.pdf
[7]
Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In International Conference on Automated Deduction. 527–538. https://doi.org/10.1007/978-3-319-21401-6_36
[8]
Jonathan Julian Huerta y Munive. 2020. Algebraic verification of hybrid systems in Isabelle/HOL. Ph.D. Dissertation. University of Sheffield. https://etheses.whiterose.ac.uk/28886/
[9]
Jonathan Julián Huerta y Munive and Georg Struth. 2018. Verifying hybrid systems with modal Kleene algebra. In International Conference on Relational and Algebraic Methods in Computer Science. 225–243. https://doi.org/10.1007/978-3-030-02149-8_14
[10]
Jonathan Julián Huerta y Munive and Georg Struth. 2022. Predicate Transformer Semantics for Hybrid Systems. Journal of Automated Reasoning, 66, 1 (2022), 93–139. https://doi.org/10.1007/s10817-021-09607-x
[11]
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer. 2017. A Formally Verified Hybrid System for Safe Advisories in the Next-generation Airborne Collision Avoidance System. STTT, 19, 6 (2017), 717–741. https://doi.org/10.1007/s10009-016-0434-1
[12]
Yanni Kouskoulas, David W. Renshaw, André Platzer, and Peter Kazanzides. 2013. Certifying the Safe Design of a Virtual Fixture Control Algorithm for a Surgical Robot. In Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC’13, Philadelphia, PA, USA, April 8-13, 2013, Calin Belta and Franjo Ivancic (Eds.). ACM, 263–272. https://doi.org/10.1145/2461328.2461369
[13]
Paolo Masci and César A. Muñoz. 2019. An Integrated Development Environment for the Prototype Verification System. In Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019, Rosemary Monahan, Virgile Prevosto, and José Proença (Eds.) (EPTCS, Vol. 310). 35–49. https://doi.org/10.4204/EPTCS.310.5
[14]
Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer. 2017. Formal Verification of Obstacle Avoidance and Navigation of Ground Robots. I. J. Robotics Res., 36, 12 (2017), 1312–1340. https://doi.org/10.1177/0278364917733549
[15]
Mariano M Moscato, César A Muñoz, and Andrew P Smith. 2015. Affine arithmetic and applications to real-number proving. In International Conference on Interactive Theorem Proving. 294–309. https://doi.org/10.1007/978-3-319-22102-1_20
[16]
César Munoz and Anthony Narkawicz. 2013. Formalization of Bernstein polynomials and applications to global optimization. Journal of Automated Reasoning, 51, 2 (2013), 151–196. https://doi.org/10.1007/s10817-012-9256-3
[17]
Anthony Narkawicz and César Munoz. 2013. A formally verified generic branching algorithm for global optimization. In Working Conference on Verified Software: Theories, Tools, and Experiments. 326–343. https://doi.org/10.1007/978-3-642-54108-7_17
[18]
Anthony Narkawicz and César Muñoz. 2014. A Formally Verified Generic Branching Algorithm for Global Optimization. In Proceedings of the 5th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2013), Ernie Cohen and Andrey Rybalchenko (Eds.) (Lecture Notes in Computer Science, Vol. 8164). Springer, Menlo Park, CA, US. 326–343. https://doi.org/10.1007/978-3-642-54108-7_17
[19]
Anthony Narkawicz, César Munoz, and Aaron Dutle. 2015. Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. Journal of Automated Reasoning, 54, 4 (2015), 285–326. https://doi.org/10.1007/s10817-015-9320-x
[20]
Sam Owre, John M Rushby, and Natarajan Shankar. 1992. PVS: A prototype verification system. In International Conference on Automated Deduction. 748–752. https://doi.org/10.1007/3-540-55602-8_217
[21]
André Platzer. 2008. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41, 2 (2008), 143–189. https://doi.org/10.1007/s10817-008-9103-8
[22]
André Platzer. 2010. Differential-algebraic Dynamic Logic for Differential-algebraic Programs. J. Log. Comput., 20, 1 (2010), 309–352. https://doi.org/10.1093/logcom/exn070 Advance Access published on November 18, 2008.
[23]
André Platzer. 2017. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59, 2 (2017), 219–265. https://doi.org/10.1007/s10817-016-9385-1
[24]
André Platzer. 2018. Logical Foundations of Cyber-Physical Systems. Springer, Cham. isbn:978-3-319-63587-3 https://doi.org/10.1007/978-3-319-63588-0
[25]
André Platzer and Jan-David Quesel. 2008. KeYmaera: A hybrid theorem prover for hybrid systems (system description). In International Joint Conference on Automated Reasoning. 171–178. https://doi.org/10.1007/978-3-540-71070-7_15
[26]
André Platzer and Jan-David Quesel. 2009. European Train Control System: A Case Study in Formal Verification. In ICFEM, Karin Breitman and Ana Cavalcanti (Eds.) (LNCS, Vol. 5885). Springer, 246–265. https://doi.org/10.1007/978-3-642-10373-5_13
[27]
Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer. 2016. How to model and prove hybrid systems with KeYmaera: a tutorial on safety. International Journal on Software Tools for Technology Transfer, 18, 1 (2016), 67–91. https://doi.org/10.1007/s10009-015-0367-0
[28]
J Tanner Slagel, Lauren White, and Aaron Dutle. 2021. Formal verification of semi-algebraic sets and real analytic functions. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. 278–290. https://doi.org/10.1145/3437992.3439933
[29]
Georg Struth. 2021. Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. In Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. 13047, 367. https://doi.org/10.1007/978-3-030-90870-6_20
[30]
Hannah S Walsh, Eleni Spirakis, Sequoia R Andrade, Daniel E Hulse, and Misty D Davies. 2020. SMARt-STEReO: Preliminary concept of operations. https://ntrs.nasa.gov/citations/20205007665
Index Terms
- Towards an implementation of differential dynamic logic in PVS
Recommendations
Formally verified differential dynamic logic
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and ProofsWe formalize the soundness theorem for differential dynamic logic, a logic for verifying hybrid systems. To increase confidence in the formalization, we present two versions: one in Isabelle/HOL and one in Coq. We extend the metatheory to include ...
A Temporal Differential Dynamic Logic Formal Embedding
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and ProofsDifferential temporal dynamic logic dTL2 is a logic to specify and verify temporal properties of hybrid systems. It extends differential dynamic logic (dL) with temporal operators that enable reasoning on intermediate states in both discrete and ...
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics
CPP 2016: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and ProofsDifferential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyber-physical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2022 ACM.
ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the United States government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 14 June 2022
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
SOAP '22
Sponsor:
SOAP '22: 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis
June 14, 2022
CA, San Diego, USA
Acceptance Rates
Overall Acceptance Rate 11 of 11 submissions, 100%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 50Total Downloads
- Downloads (Last 12 months)6
- Downloads (Last 6 weeks)0
Reflects downloads up to 24 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in