Motivations for Model Checking of a Fault Protection System

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.