Synchronous Interfaces and Assume/Guarantee Contracts

Albert Benveniste 1 Benoît Caillaud 1
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : In this short note, we establish a link between the theory of Moore Interfaces proposed in 2002 by Chakraborty et al. as a specification framework for synchronous transition systems, and the Assume/Guarantee contracts as proposed in 2007 by Benveniste et al. as a simple and flexible contract framework. As our main result we show that the operation of saturation of A/G contracts (namely the mapping (A, G) → (A, G∨¬A)), which was considered a drawback of this theory, is indeed implemented by the Moore Game of Chakraborty et al. We further develop this link and come up with some remarks on Moore Interfaces.
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01616369
Contributor : Benoît Caillaud <>
Submitted on : Friday, October 13, 2017 - 3:40:02 PM
Last modification on : Thursday, December 13, 2018 - 3:55:29 PM
Long-term archiving on : Sunday, January 14, 2018 - 2:07:40 PM

File

Kim.pdf
Files produced by the author(s)

Identifiers

Citation

Albert Benveniste, Benoît Caillaud. Synchronous Interfaces and Assume/Guarantee Contracts. Luca Aceto; Giorgio Bacci; Giovanni Bacci; Anna Ingólfsdóttir; Radu Mardare. Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, 10460, Springer, pp.233-248, 2017, Theoretical Computer Science and General Issues, 978-3-319-63121-9. ⟨10.1007/978-3-319-63121-9_12⟩. ⟨hal-01616369⟩

Share

Metrics

Record views

1708

Files downloads

237