Inhalt des Dokuments
Publikationen
| 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 |
Zusatzinformationen / Extras
Direktzugang
Schnellnavigation zur Seite über Nummerneingabe