Analysis of UML Models

If you are interested in this topic, please contact Manuel Wimmer.

The fUML standard defines an operational semantics for UML that allows to execute UML models based on activity diagrams. However, for the analysis of such activity diagrams, there is currently only limited support.

The goal of this thesis topic is to explore mappings from fUML to well-studied formalisms for analysis such as Coloured Petri Nets and Maude. For instance, these formalisms allow for checking several interesting properties such as termination and confluence as well as model checking in general.