Fault-Tolerance Verification of the Fluids and Combustion Facility of the International Space Station

This article describes our experience with faulttolerance verification of the Fluids and Combustion Facility (FCF) of the International Space Station (ISS). The FCF will be a permanent installation for scientific microgravity experiments in the U.S. Laboratory Module aboard the ISS. The ability to withstand faults is vital for all ISS installations. Currently, the FCF safety specification requires one-component faulttolerance. In future versions, even greater robustness may be required. Faults encountered by ISS modules vary in nature and extent. Self-stabilization is an adequate approach to tolerance design of the FCF. However, for systems as complex as the FCF, analytical tolerance verification is not feasible. We use automated model-checking. We model the FCF in SPIN and specify stabilization predicates to which the FCF must conform. Our model of the FCF allows us to inject component faults as well as hazardous conditions. We use SPIN to automatically verify the convergence of the FCF model to legitimate states.