Performance Analysis And Research On High Dependable System Based On Probabilistic Model Checking

With the continuous development of science and technology,people's life has gradually entered the era of smart information and Automatic Control,which relies on a variety of largescale and high dependable system.In order to improve the performance of the system and reduce the maintenance cost,people put forward higher requirements for the reliability and safety of the system.Therefore,it is urgent to optimize the system architecture and develop new high-reliability system software.It is very necessary to evaluate the security and reliability of the system.As a branch of evolution based on traditional model checking,probabilistic model checking technology not only could complete verification automatically,but also produce quantitative results,provide more detailed basis for system verification,and provide a more clear direction to improve system performance.In this paper,two practical application scenarios of high-reliability system are studied,and the system is modeled and verified by probabilistic model checking technology.The main contributions of this paper are as follows:(1)For the characteristics of the low degree of formalization of the traditional embedded control system's fault model,this paper combines the probability model checking technology to abstract the model of the system's failure scenario,and expands the Continuous-Time Markov Chain probability model(Embedded Systems Continuous-Time Markov Chain,EMCTMC)to meet the actual scenario of the embedded control system,and puts forward three stages of the operation process based on the probability model checking algorithm DCES subalgorithm,PDES sub-algorithm and SIES sub-algorithm to describe the system operation logic.Using PRISM language to formalize the system model and attributes,after the construction and verification,the fault boundary condition attributes of the system,different types of fault conditions,as well as the reboot and energy consumption of the system are further studied,which provides an effective way to improve the stability and reliability of the system.(2)The key of cluster relying on availability is to provide continuous service.In this paper,the fault-tolerant backup process of cluster is modeled and analyzed with probability model checking technology.By abstracting the process,extended the Continuous-Time Markov Chain(Expanded Continuous-Time Markov Chain,ECTMC)which is consistent with the process of cluster fault-tolerant backup recovery,and proposed the FCR sub-algorithm and REP subalgorithm based on the probability model checking algorithm.On the basis of the model,a strategy of producer + queue + consumer queue model is added to solve the problem of mismatch between cluster system failure and maintenance efficiency,and the priority of maintenance unit repair components is defined to improve the reliability of the system.The model is described in PRISM,a probabilistic model checking tool.the stability of system,system boundary,fault recovery and reliability of system quality of service(QoS)are described by CSL.Through the verification,it is found that by increasing the queue model and the priority of components,the system reliability and disaster resistance are greatly improved,which provides an effective solution for system improvement.The research results of this paper provide better theoretical guidance and solutions for the reliability verification and optimization of system architecture of high system,expand the application theory of probability model checking,and provide better foundation for the practical application of high-reliability system combined with probability model checking technology.