Reliability prediction of a hydraulic system with probabilistic model checking

Probabilistic model checking is a formal verification technique, which has been used in many areas including reliability assessment. In this paper, probabilistic model checking is introduced to reliability prediction of hydraulic systems, and a controllable pitch propeller hydraulic system is taken as an example. Firstly, aCTMC (Continuous-time Markov chain) model is established based on the system structure. Then CSL(Continuous Stochastic Logic) formulas are given to describe the reliability and failure rate of the system. Finally, the PRISM model checker is used to verify the properties and give the quantitative results. This paper describes how to analyze the system, create Markov models, and parts of the code. The results show that the method can actually predict the reliability and has potentials of further applications.