Skip to Main content Skip to Navigation
Conference papers

A Mechanically Verified Theory of Contracts

Stéphane Kastenbaum 1, 2 Benoît Boyer 1 Jean-Pierre Talpin 2 
2 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Cyber-physical systems (CPS) are assemblies of networked, heterogeneous, hardware, and software components sensing, evaluating, and actuating a physical environment. This heterogeneity induces complexity that makes CPSs challenging to model correctly. Since CPSs often have critical functions, it is however of utmost importance to formally verify them in order to provide the highest guarantees of safety. Faced with CPS complexity, model abstraction becomes paramount to make verification attainable. To this end, assume/guarantee contracts enable component model abstraction to support a sound, structured, and modular verification process. While abstractions of models by contracts are usually proved sound, none of the related contract frameworks themselves have, to the best of our knowledge, been formally proved correct so far. In this aim, we present the formalization of a generic assume/guarantee contract theory in the proof assistant Coq. We identify and prove theorems that ensure its correctness. Our theory is generic, or parametric, in that it can be instantiated and used with any given logic, in particular hybrid logics, in which highly complex cyber-physical systems can uniformly be described.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03329311
Contributor : Stéphane Kastenbaum Connect in order to contact the contributor
Submitted on : Monday, August 30, 2021 - 6:17:27 PM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM

Identifiers

Citation

Stéphane Kastenbaum, Benoît Boyer, Jean-Pierre Talpin. A Mechanically Verified Theory of Contracts. ICTAC 2021 - 18th International Colloquium on Theoretical Aspects of Computing, Sep 2021, Nur-Sultan, Kazakhstan. pp.134-151, ⟨10.1007/978-3-030-85315-0_9⟩. ⟨hal-03329311⟩

Share

Metrics

Record views

31

Files downloads

60