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

The Fluids and Combustion Facility (FCF) will be a permanent modular, multi-user facility used to accommodate microgravity science experiments in the U.S. Laboratory Module onboard the International Space Stations (ISS). The ability to withstand faults is vital for all ISS installations. Currently, the FCF safety specification requires a one-component fault-tolerance. In future versions, a more extensive faulttolerance model may be required. In this paper, we describe the formal verification of fault-tolerance of the FCF Distributed State Model using SPIN. We program the FCF module state transitions in PROMELA (SPIN's internal language). We first verify the correctness of FCF without faults. We then simulate a single fault by moving one of the modules to an arbitrary state and verify correct recovery of the system. We extend our verification to the case of an extensive fault where the whole system has to recover from an arbitrary global state.

• Type: Conference
• Year: 2006
• Where: ICDCSW
• Authors: Raquel S. Whittlesey-Harris, Mikhail Nesterenko
• Keywords: Distributed And Parallel Computing, FCF Distributed State, FCF Module State, FCF Safety Specification, ICDCSW 2006