Using Model Transformation to Generate Graphical Counter-Examples for the Formal Analysis of xUML Models

The INESS (Integrated European Signalling System) Project, funded by the FP7 programme of the European Union, aims to provide a common, integrated, railway signalling system within Europe. INESS experts have been using the Executable UML (xUML) language to model an executable specification of the proposed system. Due to safety-critical aspects of these systems, one key idea is to formally analyse them. In this context, we have been working with other universities on different translation-based methods that enable the formal verification of xUML models. At the core of this approach is a verification framework based on model transformation technology, used to implement an automatic and transparent verification method for xUML. Since a translation-based approach is used, a key aspect to achieve transparency is the automatic generation of counter-examples for verified properties that have a false result during the analysis, in terms of the original xUML model. We describe in this paper how we achieve this using model transformation technology.