2000 | OriginalPaper | Buchkapitel
Behavioral Conformance Verification in an Integrated Approach Using UML and B
verfasst von : Eric Meyer, Thomas Santen
Erschienen in: Integrated Formal Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.