Formal Availability Analysis using Theorem Proving

Abstract: Availability analysis is used to assess the possible failures and their restoration process for a given system. This analysis involves the calculation of instantaneous and steady-state availabilities of the individual system components and the usage of this information along with the commonly used availability modeling techniques, such as Availability Block Diagrams (ABD) and Fault Trees (FTs) to determine the system-level availability. Traditionally, availability analyses are conducted using paper-and-pencil methods and simulation tools but they cannot ascertain absolute correctness due to their inherent limitations. As a complementary approach, we propose to use the higher-order-logic theorem prover HOL4 to conduct the availability analysis of safety-critical systems. For this purpose, we present a higher-order-logic formalization of instantaneous and steady-state availability, ABD configurations and generic unavailability FT gates. For illustration purposes, these formalizations are utilized to conduct formal availability analysis of a satellite solar array, which is used as the main source of power for the Dong Fang Hong-3 (DFH-3) satellite.

Proof Script: Availability_Script

Automation SML Script: automation_availability_solar_array

Waqar Ahmad is a PhD student at the School of Electrical Engineering and Computer Science of National University of Sciences and Technology. He is working on his PhD thesis in the System Analysis & Verification (SAVE) Lab of NUST-SEECS, under the supervision of Dr. Osman Hasan.