Temporal Properties Verification of Real-Time Systems Using UML/MARTE/OCL-RT

Dependability is a key feature of critical Real-Time Systems (RTS). In fact, errors may lead to disastrous consequences on life beings and economy. To ensure the absence or avoidance of such errors, it is important to focus on RTS verification as early as possible. As MARTE UML profile is the standard de facto for modelling RTS, we suggest to extend UML diagrams by a formal verification stage. More precisely, in the first part we propose a transformation approach of Interaction Overview Diagrams and Timing Diagram merged with UML-MARTE annotations into Time Petri Nets (TPN) models Then, in the second part, we show how we can derive Timed Computational Tree Logic formulae from Object Constraint Language-Real Time (OCL-RT) constraints. This formal verification is performed by the Romeo model-checker. Finally, we illustrate our approach through a case study derived from a RT asynchronous system (Integrated Modular Avionics/based airborne system).