HAL - INRIA :: [inria-00375098, version 1] Why are modalities good for Interface Theories?

inria-00375098, version 1

Why are modalities good for Interface Theories?

Jean-Baptiste Raclet ( Auteur à contacter de préférence ) ¹, Eric Badouel ()^a^, 2, Albert Benveniste ()^a^, 3, Benoit Caillaud ()^a^, 2, Roberto Passerone ()^b^, 4

N° RR-6899 (2009)

Résumé : In this paper 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 by Kim Larsen, offer the needed flexibility.

a – INRIA
b – Trento University
1 : POP ART (INRIA Rhône-Alpes)
INRIA
2 : S4 (INRIA - IRISA)
CNRS : UMR6074 – INRIA – INSA Rennes – Université de Rennes 1
3 : DISTRIBCOM (INRIA - IRISA)
CNRS : UMR6074 – INRIA – École normale supérieure de Cachan - ENS Cachan – INSA Rennes – Université de Rennes 1
4 : Department of Information Engineering and Computer Science (DISI)
University of Trento, Italy

inria-00375098, version 1
http://hal.inria.fr/inria-00375098
oai:hal.inria.fr:inria-00375098
Contributeur : Jean-Baptiste Raclet <>
Soumis le : Lundi 13 Avril 2009, 15:45:12
Dernière modification le : Jeudi 16 Avril 2009, 11:23:56

Voir la fiche détaillée

Documents associés

PS :

PDF :

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="report"><head>Rapports</head>
<biblStruct type="report" xml:id="inria-00375098"><monogr>
<author><persName><forename>Jean-Baptiste</forename><surname>Raclet</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Rhône-Alpes</orgName>
<orgName type="team">POP ART</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
</affiliation>
</author>
<author><persName><forename>Eric</forename><surname>Badouel</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">S4</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Albert</forename><surname>Benveniste</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">DISTRIBCOM</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Benoit</forename><surname>Caillaud</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">S4</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Roberto</forename><surname>Passerone</surname></persName>
<affiliation>
<orgName type="laboratory">DISI</orgName>
<orgName type="team">Department of Information Engineering and Computer Science</orgName>
<country>IT</country>
<orgName type="institution">University of Trento, Italy</orgName>
</affiliation>
</author>
<title type="main" level="m">Why are modalities good for Interface Theories?</title><title type="main" level="m">Why are modalities good for Interface Theories?</title><imprint><biblScope type="publicationDate">2009-00-00</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00375098</idno><idno type="HALFile">http://hal.inria.fr/inria-00375098/PDF/RR-6899.pdf</idno></biblStruct>
</listBibl>
</listBibl>