Proving Component Interoperability with B Refinement

Samir Chouali; Maritta Heisel; Jeanine Souquières

inria-00000171, version 1

Proving Component Interoperability with B Refinement

Samir Chouali () ¹, Maritta Heisel () ², Jeanine Souquières () ¹

(2005)

Résumé : We use the formal method B for specifying interfaces of software components. Each component interface is equipped with a suitable data model defining all types occurring in the signature of interface operations. Moreover, pre- and postconditions have to be given for all interface operations. The interoperability between two components is proved by using a refinement relation between an adaptation of the interface specifications.

1 : DEDALE (LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2 : Fachbereich Ingenieurwissenschaften Institut fur Medientechnik und Software Engineering
Universität Duisburg-Essen

inria-00000171, version 1
http://hal.inria.fr/inria-00000171
oai:hal.inria.fr:inria-00000171
Contributeur : Samir Chouali <>
Soumis le : Mercredi 20 Juillet 2005, 17:27:30
Dernière modification le : Jeudi 29 Juin 2006, 12:03:57

Voir la fiche détaillée

Documents associés

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-00000171"><monogr>
<author><persName><forename>Samir</forename><surname>Chouali</surname></persName>
<affiliation>
<orgName type="laboratory">LORIA</orgName>
<orgName type="team">DEDALE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Maritta</forename><surname>Heisel</surname></persName>
<affiliation>
<orgName type="team">Fachbereich Ingenieurwissenschaften Institut fur Medientechnik und Software Engineering</orgName>
<country>DE</country>
<orgName type="institution">Universität Duisburg-Essen</orgName>
</affiliation>
</author>
<author><persName><forename>Jeanine</forename><surname>Souquières</surname></persName>
<affiliation>
<orgName type="laboratory">LORIA</orgName>
<orgName type="team">DEDALE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="m">Proving Component Interoperability with B Refinement</title><title type="main" level="m">Proving Component Interoperability with B Refinement</title><imprint><biblScope type="publicationDate">2005-00-00</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00000171</idno><idno type="HALFile">http://hal.inria.fr/inria-00000171/PDF/sefm05.pdf</idno></biblStruct>
</listBibl>
</listBibl>