Methodology for UML Modeling and Formal Verification of Real-Time Systems

In the paper, we present a methodology developed in order to verify probabilistic timed properties related to dependability of real-time systems. The methodology is made of three essential steps. The first one is a UML profile called DAMRTS (dependability analysis models for real-time systems) designed using GME tool. The aim is to model a real-time system with qualitative and quantitative information related to its quality of service. In this profile, UML statecharts are used to represent the system behavior. An extension is introduced with probabilities, real-time requirements and nondeterministic choices. The second one proposes a translation from extended UML statecharts to probabilistic timed automata. In this step, synchronization by events is used in probabilistic timed automata to describe the concurrency in UML statecharts. The last one is about the probabilistic model checking. This requires specification of dependability properties with a suitable temporal logic.