Synchronous Interfaces and Assume/Guarantee Contracts - Archive ouverte HAL Access content directly
Book Sections Year : 2017

Synchronous Interfaces and Assume/Guarantee Contracts

(1) , (1)
1

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.
Fichier principal
Vignette du fichier
Kim.pdf (144.35 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01616369 , version 1 (13-10-2017)

Identifiers

Cite

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⟩
449 View
364 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More