direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


Formal Verification of Java Code Generation from UML Models
Zitatschlüssel BGL2005
Autor Jan Olaf Blech and Sabine Glesner and Johannes Leitner
Buchtitel Proceedings of the 3rd International Fujaba Days 2005, "MDD in Practice"
Seiten 49-56
Jahr 2005
Adresse Paderborn, Germany
Monat Sep
Verlag Technical Report, University of Paderborn
Zusammenfassung UML specifications offer the advantage to describe software systems while the actual task of implementing code for them is passed to code generators that automatically produce e.g. Java code. For safety reasons, it is necessary that the generated code is semantically equivalent to the original UML specification. In this paper, we present our approach to formally verify within the Isabelle/HOL theorem prover that a certain algorithm for Java code generation from UML specifications is semantically correct. This proof is part of more extensive ongoing work aiming to verify UML transformations and code generation within the Fujaba tool suite.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe