Universität Karlsruhe
Formal Verification of Java Code Generation from UML Models


[BGL2005]Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Formal Verification of Java Code Generation from UML Models, Fujaba Days, september 2005.


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.

[Erzeuge bibTeX Eintrag]


Prof. Sabine Glesner
Jan Olaf Blech
Johannes Leitner