Reliability analysis for flight control systems using probabilistic model checking
Luyao Wang, Fang Cai · 2017
Flight control systems (FCSs) are safety-critical systems, which require high reliability requirements. Probabilistic model checking techniques use mathematical reasoning to check quantitative properties and generate accurate value. This paper combines the probabilistic model checking and reliability analysis for FCSs, so that it is possible to make full use of the quantitative verification for solving reliability value. The FCS is described as Continuous-Time Markov Chains (CTMCs), a commonly used probabilistic model, using PRISM language. Each software component and device component with the behavior is encoded as a module in PRISM model. We also formalize rules for obtaining temporal logical formulae from reliability requirements. A FCS is employed to introduce the modeling approach and demonstrate the applicability of the proposed approach.