An Interactive Proof Environment for Object-oriented Specifications

Achim D. Brucker

In dieser Arbeit wird ein semantisches Rahmenwerk für objektorientierte Spezifikationen vorgestellt. Das Rahmenwerk ist als konservative, flache Einbettung in Isabelle/HOL realisiert. Durch die Beschränkung auf konservative Erweiterungen kann die logische Konsistenz der Einbettung garantiert werden. Das semantische Rahmenwerk wird verwendet, um das interaktives Beweissystem HOL-OCL für objektorientierte Spezifikationen im Allgemeinen und insbesondere für UML/OCL zu entwickeln.

Die Hauptbeiträge dieser Arbeit sind die Entwicklung einer erweiterbaren Kodierung objektorientierter Datenstrukturen in HOL, ein Datentyp-Paket für objektorientierte Spezifikationen und die Entwicklung verschiedener Kalküle für objektorientierte Spezifikationen. Zudem zeigen wir, wie das formale Rahmenwerk verwendet werden kann, um eine formale, maschinell geprüfte Semantik für OCL anzugeben, die konform zum Standard für OCL 2.0 ist.

Schluesselwörter: OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL
Kategorien: ,

Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker. An Interactive Proof Environment for Object-oriented Specifications. ETH Zurich,2007. ETH Dissertation No. 17097.
Schluesselwörter: OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL
(PDF) (BibTeX) (Endnote) (RIS) ( )