Graphical Modelling Meets Formal Methods

The graphical modelling languages UML and SysML, nowadays widely used in industry, integrate different modelling concepts and notations in one standardised framework. However, they lack a clearly defined, unambiguous semantics and thus their formal verification represents a challenge. On the other hand, current safety standards, including ISO 26262, demand such verification especially for safety-relevant systems. The literature proposes a plethora of different semantics and formalisms for UML/SysML. In this paper we compare and summarise existing work on the formalisation of behavioural UML and SysML models and their verification. Our goal is to foster a better understanding of the problems related to UML/SysML formalisation, and to aid people bridging the gap from high level graphical modelling to formal verification techniques.