Behavioral conformance verification in an integrated approach using UML and B

Eric Meyer 1 Thomas Santen
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Communication dans un congrès
W. Grieskamp & T. Santen & B. Stoddart. 2nd International Workshop on Integrated Formal Methods - IFM'00, Nov 2000, Dagstuhl Castle, Germany, Springer-Verlag, 1945, pp.358-379, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099377
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:53:24
Dernière modification le : mardi 24 avril 2018 - 13:34:47

Identifiants

  • HAL Id : inria-00099377, version 1

Collections

Citation

Eric Meyer, Thomas Santen. Behavioral conformance verification in an integrated approach using UML and B. W. Grieskamp & T. Santen & B. Stoddart. 2nd International Workshop on Integrated Formal Methods - IFM'00, Nov 2000, Dagstuhl Castle, Germany, Springer-Verlag, 1945, pp.358-379, 2000, Lecture Notes in Computer Science. 〈inria-00099377〉

Partager

Métriques

Consultations de la notice

39