direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content


Formal Verification of Java Code Generation from UML Models
Citation key BGL2005
Author Jan Olaf Blech and Sabine Glesner and Johannes Leitner
Title of Book Proceedings of the 3rd International Fujaba Days 2005, "MDD in Practice"
Pages 49-56
Year 2005
Address Paderborn, Germany
Month Sep
Publisher Technical Report, University of Paderborn
Abstract 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.
Bibtex Type of Publication Conference Article
Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe