Fault tree analysis method based on probabilistic model checking and discrete time Markov Chain

In order to fully consider the dynamic characteristics of event failure in fault tree analysis, the probabilistic model checking and discrete-time Markov chain are applied to the fault tree analysis. The formal probability of gate events in a fault tree is studied and the fault tree is established based on the probabilistic model checking technique. The logic gates in a fault tree are converted into discrete-time Markov chain that can be encoded into the probabilistic model checker. The discrete-time Markov chain is used to simulate the known behavior probability distribution of the system in the known situational environment, and the Markov decision process is used to simulate the non-deterministic behavior of the system under the unknown environment, and to carry out the quantitative analysis of the system. The fault tree analysis of the spindle system of a certain CNC machine tool is taken as an example to illustrate the proposed method.