2016/08/05 by Waqar Ahmed, Ahmed, Waqar, Osman Hasan +1
Computer Science · Decision Sciences · Engineering · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Reliability and Maintenance Optimization #Risk and Safety Analysis #Software Reliability and Analysis Research #cs.LO
paper · pdf · doi:10.48550/arxiv.1608.01755
16 pages. arXiv admin note: text overlap with arXiv:1505.02648
arxiv created 2016/08/05 · openalex publication_date 2016/08/05 · arxiv updated 2016/08/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 inaccuracy 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.