A new UML profile for real-time system formal design and validation

Abstract

UML solutions in competition on the real-time system market share three common drawbacks: an incomplete formal semantics, temporal operators with limited expression and analysis power, and implementation-oriented tools with limited verification capabilities. To overcome these limitations, the paper proposes a UML profile designed with real-time system validation in mind. Extended class diagrams with associations attributed by composition operators give an explicit semantics to associations between classes. Enhanced activity diagrams with a deterministic delay, a non deterministic delay and a timelimited offering make it possible to work with temporal intervals in lieu of timers with fixed duration. The UML profile is given a precise semantics via its translation into the Formal Description Technique RT-LOTOS. A RT-LOTOS validation tool generates simulation chronograms and reachability graphs for RT-LOTOS specifications derived from UML class and activity diagrams. A coffee machine serves as example. The proposed profile is under evaluation on a satellite-based software reconfiguration system.