Digital flight control systems utilize redundant hardware to meet high reliability requirements. In this study we use the
SMV model checker to assess the design correctness of a sensor voter algorithm used to manage three redundant sensors. The
sensor voter design is captured as a Simulink diagram. The requirements verified include normal operation, transient conditions,
and fault handling.
The sensor voter algorithm is a realistic example of flight citical embedded software used to manage redundant air data or
inertial reference sensors. We are using it to evaluate different design methods, languages, and tools currently available
for formal verification. Key issues are 1) integration of formal verification into existing development processes and tools,
and 2) synthesis of the correct environment (world abstraction) needed for analysis of normal and off-normal operation conditions.
This work has been supported in part by NASA contract NAS1-00079.