×

zbMATH — the first resource for mathematics

Synchronous interfaces and assume/guarantee contracts. (English) Zbl 1431.68070
Aceto, Luca (ed.) et al., Models, algorithms, logics and tools. Essays dedicated to Kim Guldstrand Larsen on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 10460, 233-248 (2017).
Summary: In this short note, we establish a link between the theory of Moore Interfaces proposed by A. Chakrabarti et al. [ibid. 2404, 414–427 (2002; Zbl 1010.68518)] as a specification framework for synchronous transition systems, and the Assume/Guarantee contracts as proposed by the authors et al. [ibid. 5382, 200–225 (2008; Zbl 1209.68120)] 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)\mapsto (A,G{\vee}{\lnot }A))\), which was considered a drawback of this theory, is indeed implemented by the Moore Game of Chakrabarti et al. [loc. cit.]. We further develop this link and come up with some remarks on Moore Interfaces.
For the entire collection see [Zbl 1368.68004].
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI