An Institutional Framework for Heterogeneous Formal Development in UML

TL;DR

This paper introduces an institution-based heterogeneous framework for formal UML development, enabling direct formal semantics for various UML diagrams without relying on a single formalism, and supporting consistency verification across development stages.

Contribution

It proposes a novel heterogeneous formal semantics approach for UML using institutions, allowing direct expression of semantics for different diagram types without mapping to a single formalism.

Findings

Framework formalizes requirements, design, and implementation coherently.

Enables verification of consistency among UML diagrams.

Supports correctness checks from requirements to code.

Abstract

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).