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.
Type de document :
Communication dans un congrès
17th International Conference on Application of Concurrency to System Design, Jun 2017, Zaragoza, Spain
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01615140
Contributeur : Jean-Pierre Talpin <>
Soumis le : jeudi 12 octobre 2017 - 08:10:44
Dernière modification le : mercredi 16 mai 2018 - 11:24:13

Fichier

acsd17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

32