Graphical modelling meets formal methods

Author

Gulan, Stefan ; Johr, Sven ; Kretschmer, Roberto ; Rieger, S. ; Ditze, Michael

Author_Institution

TWT GmbH Sci. & Innovation, Neuhausen, Germany

fYear

2013

fDate

29-31 July 2013

Firstpage

716

Lastpage

721

Abstract

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.

Keywords

ISO standards; Unified Modeling Language; formal verification; ISO 26262; SysML models; behavioural UML models; formal methods; formal verification techniques; graphical modelling languages; high level graphical modelling; safety standards; safety-relevant systems; standardised framework; Computational modeling; Model checking; Object oriented modeling; Petri nets; Safety; Semantics; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Industrial Informatics (INDIN), 2013 11th IEEE International Conference on

Conference_Location

Bochum

Type

conf

DOI

10.1109/INDIN.2013.6622972

Filename

6622972