| Abstract / Kurzbeschreibung: |
We present a framework for formal software development with UML. In
contrast to previous approaches that equip UML with a formal
semantics, we follow an institution based heterogeneous approach. This
can express suitable formal semantics of the different UML diagram
types directly, without the need to map everything to one specific
formalism (let it be first-order logic or graph grammars). We show how
different aspects of the formal development process can be coherently
formalised, ranging from requirements over design and Hoare-style
conditions on code to the implementation itself. The framework can be
used to verify consistency of different UML diagrams both horizontally
(e.g., consistency among various requirements) as well as vertically
(e.g., correctness of design or implementation w.r.t. the
requirements). |
