UML and RT-LOTOS: an integration for real-time system validation

Abstract

The paper presents a UML profile that overcomes the limitations of real-time solutions currently available on the market. Associations between classes are given a formal semantics. New temporal operators are introduced; they include a non deterministic delay and a time-limited offering. UML models can be validated against logical and timing constraints. The profile’s semantics is given through a translation into the formal language RT-LOTOS. The latter is supported by a validation tool which generates reachability graphs from extended UML models. A coffee machine serves as example in the paper. The profile is under evaluation on a satellite-based software reconfiguration system.