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

Conference Article

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

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.

[Generate bibTeX entry]

Authors

Alumni
Prof. Sabine Glesner
Jan Olaf Blech
Former Students
Johannes Leitner
Login
Links