HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Compositional proofs in differential dynamic logic dL

Simon Lunel 1, 2 Benoît Boyer 2 Jean-Pierre Talpin 1
1 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Modularity and composability are essential properties to facilitate and scale the design of cyber-physical systems from the specification of hybrid, discrete and continuous, components. Modularity is essential to break down a system model into comprehensible and manageable component specifications. Composability is essential to design a system from component models while preserving their verified properties, expressed as assume-guarantee contracts. In this paper, we address the specification of hybrid system using Platzer's differential dynamic logic (dL). Our contribution is threefold: (1) We define a new composition operator in dL and prove that it is associative and commutative (AC). Prior notions of composition in dL were not associative. (2) We provide a theorem which characterizes necessary conditions to automate the proof that composed components satisfy the composition of their individual contracts, enabling modular and compositional verification. (3) We case-study our AC composition operator by considering the modular and detailed specification of a cruise controller in KeYmaera X, the latest implementation of dL, to demonstrate the proof automation capability of our contribution and exemplify a compositional design methodology.
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01615140
Contributor : Jean-Pierre Talpin Connect in order to contact the contributor
Submitted on : Thursday, October 12, 2017 - 8:10:44 AM
Last modification on : Monday, April 4, 2022 - 9:28:22 AM

File

acsd17.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01615140, version 1

Citation

Simon Lunel, Benoît Boyer, Jean-Pierre Talpin. Compositional proofs in differential dynamic logic dL. 17th International Conference on Application of Concurrency to System Design, Jun 2017, Zaragoza, Spain. ⟨hal-01615140⟩

Share

Metrics

Record views

188

Files downloads

183