pdfreaders.org

An Interactive Proof Environment for Object-oriented Specifications

Achim D. Brucker

Cover for brucker:interactive:2007.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.

Schlüsselwörter: OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker:interactive:2007.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.
Schlüsselwörter: OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@PhDThesis{ brucker:interactive:2007,
abstract = {We present a semantic framework for object-oriented specification languages. We develop this framework as a conservative shallow embedding in Isabelle/HOL. Using only conservative extensions guarantees by construction the consistency of our formalization. Moreover, we show how our framework can be used to build an interactive proof environment, called HOL-OCL, for object-oriented specifications in general and for UML/OCL in particular.\\\\Our main contributions are an extensible encoding of object-oriented data structures in HOL, a datatype package for object-oriented specifications, and the development of several equational and tableaux calculi for object-oriented specifications. Further, we show that our formal framework can be the basis of a formal machine-checked semantics for OCL that is compliant to the OCL 2.0 standard.},
abstract_de = {In dieser Arbeit wird ein semantisches Rahmenwerk f{\"u}r objektorientierte Spezifikationen vorgestellt. Das Rahmenwerk ist als konservative, flache Einbettung in Isabelle/HOL realisiert. Durch die Beschr{\"a}nkung auf konservative Erweiterungen kann die logische Konsistenz der Einbettung garantiert werden. Das semantische Rahmenwerk wird verwendet, um das interaktives Beweissystem HOL-OCL f{\"u}r objektorientierte Spezifikationen im Allgemeinen und insbesondere f{\"u}r UML/OCL zu entwickeln.\\\\Die Hauptbeitr{\"a}ge dieser Arbeit sind die Entwicklung einer erweiterbaren Kodierung objektorientierter Datenstrukturen in HOL, ein Datentyp-Paket f{\"u}r objektorientierte Spezifikationen und die Entwicklung verschiedener Kalk{\"u}le f{\"u}r objektorientierte Spezifikationen. Zudem zeigen wir, wie das formale Rahmenwerk verwendet werden kann, um eine formale, maschinell gepr{\"u}fte Semantik f{\"u}r OCL anzugeben, die konform zum Standard f{\"u}r OCL 2.0 ist.},
author = {Achim D. Brucker},
keywords = {OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL},
month = {mar},
note = {ETH Dissertation No. 17097.},
pdf = {https://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf},
school = {ETH Zurich},
title = {An Interactive Proof Environment for Object-oriented Specifications},
url = {https://www.brucker.ch/bibliography/abstract/brucker-interactive-2007},
year = {2007},
}