Motivations for Model Checking of a Fault Protection System
Martin S. Feather, Steve Fickas · 2001
Model checking of spacecraft systems Model checking is a powerful analysis technique that has emerged from the formal methods research community. Over the last decade or so it has been successfully applied to analyze a variety of hardware and software designs. At NASA, model checking has been employed to analyze spacecrafts ’ critical control software. For example, Schneider et al. used model checking on the checkpoint-rollback scheme of a spacecraft’s fault protection system (Schneider et al. 1998). The NASA-Ames Software Engineering Group