NASA LaRC Formal Methods Program: SPIDER

home

welcome

quick page

philosophy

team

research

quote

links

new?

Formal Analysis of Fault Tolerance

For life critical systems, errors may mean disaster. The potential for errors is high, because these systems must not only perform their functions correctly, but also must be able to recover from the effects of failing components (in order to meet stringent ultrareliability requirements.) Often the physical fault-tolerance features of these systems are more complex and susceptible to design error than any of the basic functions of the system. John Rushby writes:

Organization of redundancy and fault-tolerance for ultra-high reliability is a challenging problem: redundancy management can account for half the software in a flight control system and, if less than perfect can itself become the primary source of system failure. Projects include:

Scalable Processor-Independent Design for Extended Reliability (SPIDER)

Honeywell Engines and Systems: Use Time Triggered Architecture (TTA) developed in Europe for the automotive industry and formal verification methods to develop an FTIMA architecture for a Full Authority Digital Engine Control (FADEC). Team includes SRI International and TTTech. See
- PowerPoint Talk.
- An Overview of Formal Verification for the Time-Triggered Architecture
Reliability Analysis Tools

Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 18 October 2002 (09:23:08)