Behavioral Conformance Verification in an Integrated Approach Using UML and B
Identifieur interne : 001A72 ( Istex/Curation ); précédent : 001A71; suivant : 001A73Behavioral Conformance Verification in an Integrated Approach Using UML and B
Auteurs : Eric Meyer [France] ; Thomas Santen [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We propose an integration of diagrammatic object oriented modeling techniques with a formal specification and verification technique. We translate UML class diagrams to B abstract machines in a way that does not only provide a formal interpretation of the class diagrams but that also allows us to verify properties of object oriented models within the framework of the B method. Specifically, we address translating generalization / specialization hierarchies to B. An appropriate construction of B components allows us to express and formally verify behavioral conformance, which ensures that polymorphism can be used safely. Expressing the proof obligations associated with behavioral conformance by constructing B components makes it possible to use the tool AtelierB for mechanically verifying them.
Url:
DOI: 10.1007/3-540-40911-4_21
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001A92
Links to Exploration step
ISTEX:7504E7E0004376A6D8340B347832229F61F2012DCuration
No country items
Thomas Santen<affiliation><mods:affiliation>E-mail: santen@acm.org</mods:affiliation><wicri:noCountry code="no comma">E-mail: santen@acm.org</wicri:noCountry></affiliation>Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Behavioral Conformance Verification in an Integrated Approach Using UML and B</title><author><name sortKey="Meyer, Eric" sort="Meyer, Eric" uniqKey="Meyer E" first="Eric" last="Meyer">Eric Meyer</name><affiliation wicri:level="1"><mods:affiliation>LORIA, Université Nancy 2, UMR 7503 Campus scientifique, BP 239, 54506, Vandæuvre-les-Nancy Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Université Nancy 2, UMR 7503 Campus scientifique, BP 239, 54506, Vandæuvre-les-Nancy Cedex</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: meyer@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Santen, Thomas" sort="Santen, Thomas" uniqKey="Santen T" first="Thomas" last="Santen">Thomas Santen</name><affiliation wicri:level="3"><mods:affiliation>Institut für Kommunikations- und Softwaretechnik, Technische Universität Berlin, Franklinstrasse 28/29, D-10587, Berlin</mods:affiliation><country>Allemagne</country><placeName><settlement type="city">Berlin</settlement><region type="land" nuts="2">Berlin</region></placeName><wicri:orgArea>Institut für Kommunikations- und Softwaretechnik, Technische Universität Berlin, Franklinstrasse 28/29, D-10587</wicri:orgArea></affiliation><affiliation><mods:affiliation>E-mail: santen@acm.org</mods:affiliation><wicri:noCountry code="no comma">E-mail: santen@acm.org</wicri:noCountry></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:7504E7E0004376A6D8340B347832229F61F2012D</idno><date when="2000" year="2000">2000</date><idno type="doi">10.1007/3-540-40911-4_21</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-PS31JBQG-T/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001A92</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001A92</idno><idno type="wicri:Area/Istex/Curation">001A72</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Behavioral Conformance Verification in an Integrated Approach Using UML and B</title><author><name sortKey="Meyer, Eric" sort="Meyer, Eric" uniqKey="Meyer E" first="Eric" last="Meyer">Eric Meyer</name><affiliation wicri:level="1"><mods:affiliation>LORIA, Université Nancy 2, UMR 7503 Campus scientifique, BP 239, 54506, Vandæuvre-les-Nancy Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Université Nancy 2, UMR 7503 Campus scientifique, BP 239, 54506, Vandæuvre-les-Nancy Cedex</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: meyer@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Santen, Thomas" sort="Santen, Thomas" uniqKey="Santen T" first="Thomas" last="Santen">Thomas Santen</name><affiliation wicri:level="3"><mods:affiliation>Institut für Kommunikations- und Softwaretechnik, Technische Universität Berlin, Franklinstrasse 28/29, D-10587, Berlin</mods:affiliation><country>Allemagne</country><placeName><settlement type="city">Berlin</settlement><region type="land" nuts="2">Berlin</region></placeName><wicri:orgArea>Institut für Kommunikations- und Softwaretechnik, Technische Universität Berlin, Franklinstrasse 28/29, D-10587</wicri:orgArea></affiliation><affiliation><mods:affiliation>E-mail: santen@acm.org</mods:affiliation><wicri:noCountry code="no comma">E-mail: santen@acm.org</wicri:noCountry></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We propose an integration of diagrammatic object oriented modeling techniques with a formal specification and verification technique. We translate UML class diagrams to B abstract machines in a way that does not only provide a formal interpretation of the class diagrams but that also allows us to verify properties of object oriented models within the framework of the B method. Specifically, we address translating generalization / specialization hierarchies to B. An appropriate construction of B components allows us to express and formally verify behavioral conformance, which ensures that polymorphism can be used safely. Expressing the proof obligations associated with behavioral conformance by constructing B components makes it possible to use the tool AtelierB for mechanically verifying them.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001A72 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001A72 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:7504E7E0004376A6D8340B347832229F61F2012D
|texte= Behavioral Conformance Verification in an Integrated Approach Using UML and B
}}
| This area was generated with Dilib version V0.6.33. |  |