Résumé
The paper proposes a dependability analysis method based on probabilistic model checking. Using the profile DAMRTS (Dependability Analysis Models for Real-Time Systems), stochastic real-time systems are modelled with stochastic and probabilistic information. In this profile, static model of the system includes depen-dability information excerpted from fault trees. Behavioural UML models are given with combined collaboration statecharts diagrams. A method of translating these models to continuous time Markov chains (CTMCs) is proposed. The CTMCs are widely used in the context of performance and reli-ability evaluation of various systems. A formal approach is proposed to verify temporal probabilistic proper-ties related to dependability of stochastic systems. It consists to use a probabilistic model checker which sup-ports the CTMC models and then to specify properties with the suitable temporal logic.