Skip past navigation NASA Langley Formal Methods



quick page






  home > research > SPIDER

FM Program: SPIDER






The Scalable Processor-Independent Design for Extended Reliability

This project supports NASA's research in Autonomous Robust Avionics (AuRA) as part of the Vehicle Systems Program.

NASA Langley has been developing advanced fault-tolerant computing systems for over three decades, including the Software-Implemented Fault Tolerance (SIFT,1981), The Fault-Tolerant Multiprocessor (FTMP, 1981), Integrated Airframe/Propulsion Control System Architecture (IAPSA) (1990), Advanced Information Processing System (AIPS, 1991), and an architecture for the Fly-By-Light/Power-By-Wire (FBL/PBW) program. Our most recent fault-tolerant architecture is SPIDER.

The formally-verified fault-tolerant architecture, Scalable Processor-Independent Design for Extended Reliability (SPIDER), is being developed by a team of electronics engineers and formal methods researchers at NASA Langley.

SPIDER is a family of fault-tolerant, reconfigurable architectures that provide powerful mechanisms for integrating inter-dependent applications of differing criticalities. These applications communicate via a Reliable Optical BUS (ROBUS, pictures here), a TDMA bus that provides all of the basic fault-tolerance mechanisms: clock synchronization, group membership, and interactive consistency. These mechanisms have been formally proved correct using a theorem proving system, which provides an unprecedented level of assurance that SPIDER is ultra-dependable. A real-time operating system is under development for SPIDER to tailor SPIDER for Unmanned Aerial Vehicles (UAVs) under the Vehicle Systems Program.

The SPIDER architecture not only offers a greatly improved foundation for safety and mission assurance, but it has the following advancements over its predecessors: (1) it can recover from more combinations of faults including asymmetric faults and has optimizations for more benign faults such as fail-stop or symmetric faults, (2) it provides a generic interface to connect to any kind of processor, so that one is not locked into a particular semiconductor technology, (3) it can support a wide range of fault-masking strategies such as dual-dual, TMR, or even multi-stage threshold voting, (4) processing nodes may be grouped to provide differing degrees of fault-tolerance for different applications, (5) it provides dynamic reconfiguration where less important functions can be eliminated so that critical functions continue to operate, (6) it is being developed in as a case-study for RTCA DO-254, an FAA recognized approach to rigorous development, (7) it provides a mechanism for dealing with transient faults that help prevent inadvertent removal of a functional component, and (8) it is scalable to accommodate large networks of input/output resources.

Future work includes tailoring its capabilities to the unique space failure scenarios, long mission times, and extended cycles between repairs envisioned for a mission to the moon or Mars. By virtue of the use of formal methods during its design, SPIDER provides performance guarantees under well-understood assumptions. Formal Methods is the most rigorous approach available for design verification. Although it is still a fairly expensive approach, much of this cost has been born by prior NASA investment.

Additional information can be found by browsing our talks and publications.

Note: The link to external site tag identifies links that are outside of the NASA domain.

Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Rick Butler
larc privacy statement
last modified: 26 March 2004