Martin S. Feather and Stephen S. Fickas
We are about to embark on a modest study (approximately 5 work-months in total) that seeks to apply model checking to the core of the fault protection system of a new spacecraft. Fault protection systems are good candidates for model checking. Furthermore, this particular fault protection system shares some characteristics with "intelligent" systems -- its design is formally specified and the responses it commands are formally specified. These make it particularly amenable to model checking.