Angel Herranz, Assistant Professor, BABEL, UPM
There is a growing interest in the use of UML for the modeling of embedded and hybrid systems. A key factor for the adoption of model driven methods is the possibility to promptly validate designs and reveal inconsistent and incomplete requirements. But most of the interesting properties to check are beyond the capabilities of common tools. We show a transformation of UML models into Uppaal specifications that can then be used to analyse complex behavioural properties. An industrial case study on the modelling of ERTMS is used to show the applicability of our approach in the detection of property violations.