Formal methods for the validation of fault tolerance in autonomous spacecraft

One of the major challenges to be faced in the design of new-generation spacecrafts comes with the requirement to increase the capacity of autonomous operation, in particular in presence of abnormal events. Formal methods are becoming more accepted in the space industry as a possible way to manage induced systems complexity. The Data Management System Design Validation (DDV) study has accomplished an experimental junction between the spacecraft autonomy trends and emerging formal methodologies. A methodological framework applicable to the early life cycle phases of fault-tolerant systems engineering has been defined. It focuses on the verification of fault tolerance properties using model-based formalisms. The Specification and Design Language (SDL) was selected for this study as the best suited language with respect to the application. This work has resulted in an executable specification establishing the tolerated behaviours of spacecraft computers in presence of faults. Fault tolerance properties have been checked, in spite of limitations inherent to model-based formalisms, by using an appropriate verification process