Formal approach to reliability improvement with model checker

Abstract

Since the 1960s, Fault Tree Analysis has been extensively used in Safety Engineering and Reliability Engineering, and other methodologies have been proposed. We study reliability analysis with formal methods. Fault tree analysis is one of the most popular methods of reliability analysis. With this, one analyzes the causes of a fault in a top-down manner. Model checking is an automatic verification method and has recently become popular. In this paper, we incorporate model checking into the fault tree analysis and show a case study of a pressure tank control system. Moreover, we propose a formal approach for introducing a fault detection mechanism. We show an example of a fault detection mechanism in the pressure tank control system, in which it is implemented using a set of lights to check electric current. We successfully show that model checking can evaluate the effectiveness of the fault detection mechanism. © 2013 Springer Science+Business Media New York.