Motivations for Model Checking of a Fault Protection System

Model-Based Validation of Intelligence

Volume

Papers from the 2001 AAAI Spring Symposium

Contents

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.