UML models for dependability analysis of real-time systems

In this paper, we present the UML profile called DAMRTS (dependability analysis models for real-time systems) representing an extension to the reference metamodels of the OMG profile for "schedulability performance and time" (SPT). The aim is to provide concepts that enable to specify a real-time system with stochastic and probabilistic information allowing dependability analysis. A behavioural UML models are also proposed with a formal semantics designed for probabilistic model checking. An extension of state charts semantics is developed with probabilities and real-time requirements, resulting in probabilistic timed automata (PTA) as semantics models. These models are used to verify probabilistic temporal properties related to the dependability of real-time systems.