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
Contributor : Jean-Pierre Talpin <>
Submitted on : Thursday, October 12, 2017 - 8:10:44 AM
Last modification on : Friday, January 8, 2021 - 3:40:40 AM


Files produced by the author(s)


  • HAL Id : hal-01615140, version 1


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⟩



Record views


Files downloads