Why are modalities good for interface theory?

Eric Badouel

INRIA Rennes - Bretagne Atlantique

Thursday, 23 July 2009, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: We revisit the fundamentals of Interface theories. Methodological considerations call for supporting "aspects" and "assume/guarantee" reasoning. From these considerations, we show that, in addition to the now classical refinement and substitutability properties of interfaces, two additional operations are needed, namely: conjunction and residuation (or quotient). We draw the attention to the difficulty in handling interfaces having different alphabets - which calls for alphabet equalization. We show that alphabet equalization must be performed differently for the different operations. Then we show that Modal Interfaces, as adapted from the original proposal of Kim Larsen, offer the needed flexibility.

Tarmo Uustalu
Last update 20.7.2009