Synchronous Interfaces and Assume/Guarantee Contracts

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)\mapsto (A,G{\vee }{\lnot }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.

Hej Kim!: It is both a pleasure and an honor to write a tribute to Kim. Kim was preincarnated a “contractor”: in his previous life, by inventing modal specifications he contributed to contracts way before the concept ever existed. But there was a long way to the grail: getting to the point where Modal Interfaces have become comprehensive and solid occurred only recently. While joining the aristocracy of formal methods, Modal Interfaces have become terribly sophisticated. Tom (Hallo Tom!) kept telling us: “those asynchronous interfaces are too complex, look for the synchronous ones”. We offer this trial to Kim as a gift. Is it really simple? We let you judge.

The authors apologize for having used sometimes set theoretic operations {union, intersection} and in other places logical operations {or, and}. The reader will easily correct this.