# Presentation: 301560

## SPIDER Formal Models–Where are we now? 

- Paul S. Miner
- _[paul](mailto:paul.s.miner@nasa.gov)__[.s.miner@](mailto:paul.s.miner@nasa.gov)__[nasa](mailto:paul.s.miner@nasa.gov)__[.](mailto:paul.s.miner@nasa.gov)__[gov](mailto:paul.s.miner@nasa.gov)_
- In collaboration with:
- Alfons Geser (NIA), Jeff Maddalon, and Lee Pike
- Internal Formal Methods Workshop
- NASA Langley Research Center

## What is SPIDER?

- A *family* of fault-tolerant IMA architectures
- Architecure concept due to Paul Miner, Mahyar Malekpour, and Wilfredo Torres-Pomales
- Inspired by several earlier designs
- Main concept inspired by Palumbo’s Fault-tolerant processing system (U.S. Patent 5,533,188)
- Developed as part of Fly-By-Light/Power-By-Wire project
- Other ideas from Draper’s FTPP, FTP, and FTMP; Allied-Signal’s MAFT; SRI’s SIFT; Kopetz’s TTA; Honeywell’s SAFEbus; ...

- SPIDER Update

- October 22, 2003

## SPIDER Architecture

*N* general purpose Processing Elements (PEs) logically connected via a Reliable Optical BUS (ROBUS)
- A PE could be a general purpose processor, remote data concentrator, sensor, actuator, or any other device that needs to reliably communicate with other PEs
- SPIDER must be sufficiently reliable to support several aircraft functions
- Persistent loss of single function could be catastrophic
- The ROBUS is an ultra-reliable unit providing basic fault-tolerant communication services
- ROBUS contains no software

- SPIDER Update

- October 22, 2003

## Logical view of SPIDER(Sample Configuration)

- Logical view of SPIDER(Sample Configuration)

- ROBUS

- 0

- 4

- 2

- 1

- 3

- 5

- 6

- 7

- SPIDER Update

- October 22, 2003

## Design Objectives

- FT-IMA Architecture proven to survive a bounded number of physical faults
- Both permanent and transient
- Must survive ***Byzantine*** faults
- Capability to survive or quickly recover from massive correlated transient failure (e.g. in response to HIRF)

- SPIDER Update

- October 22, 2003

## Byzantine Faults

- Characterized by asymmetric error manifestations
- different manifestations to different fault-free observers
- including dissimilar values
- Can cause redundant computations to diverge
- If not properly handled, single Byzantine fault can defeat several layers of redundancy
- Many architectures neglect this class of fault
- Assumed to be rare or even impossible

- SPIDER Update

- October 22, 2003

## Byzantine faults are real

- Several examples cited in *Byzantine Faults: From Theory to Reality, *Driscoll, et al. (to appear in SAFECOMP 2003)
- Byzantine failures nearly grounded a large fleet of aircraft
- Quad-redundant system failed in response to a single fault
- Typical cases are faulty transmitters (resulting in indeterminate voltage levels at receivers) or faults that cause timing violations (so that multiple observers perceive the same event differently)
- Heavy Ion fault-injection results for TTP/C (Sivencrona, et al.)
- more than 1 in 1000 of observed errors had Byzantine manifestations

- SPIDER Update

- October 22, 2003

## SPIDER Advantages

- Fault-Tolerance independent of applications
- Tolerates more failures
- including any single Byzantine fault (and some combinations)
- including many combinations of less severe failures
- Hybrid fault model: good, asymmetric, symmetric, benign
- Does not require that nodes fail silent
- But can take advantage when they do
- Simpler, stronger protocols with stronger assurance
- Can gracefully evolve to accommodate parts obsolescence
- Off-the-shelf processors and low-level communication

- SPIDER Update

- October 22, 2003

## Failures contained by ROBUS

- Arbitrary failure in any attached Processing Element
- Hardware or Software
- Converts potential asymmetric error manifestations to symmetric
- ROBUS provides a partitioning mechanism between PEs
- Must also operate correctly if a bounded number of internal hardware devices fail
- Cannot tolerate design error within ROBUS

- SPIDER Update

- October 22, 2003

## Design Assurance Strategy 

- Fault-tolerance protocols and reliability models use the same fault classifications
- Reliability analysis using SURE (Butler & White)
- Calculates P(enough good hardware)
- Formal proof of fault-tolerance protocols using PVS (SRI)
-      enough good hardware => correct operation

- SPIDER Update

- October 22, 2003

## Strength of Formal Verification

- Proofs equivalent to testing the protocols
- for all specified ROBUS configurations
- for all combinations of faults that satisfy the maximum fault assumption for each specified ROBUS configuration
- for all specified message values
- The PVS proofs provides verification coverage equivalent to an infinite number of test cases.
- Provided that the PVS model of the protocols is faithful to the VHDL design

- SPIDER Update

- October 22, 2003

## ROBUS Characteristics

- All good nodes agree on communication schedule
- Currently bus access schedule statically determined
- similar to SAFEbus, Time-Triggered Architecture (TTA)
- Architecture supports on-the-fly schedule updates
- similar to FTPP
- Preliminary capability will be in our next prototype
- Some fault-tolerance capabilities must be provided by processing elements
- Analogous to Fault Tolerance Layer in TTA
- Processing Elements need not be uniform
- Some support for dissimilar architectures

- SPIDER Update

- October 22, 2003

## Logical View of ROBUS

- ROBUS operates as a time-division multiple access broadcast bus
- ROBUS strictly enforces write access
- no babbling idiots (prevented by ROBUS topology)
- Processing nodes may be grouped to provide differing degrees of fault-tolerance
- PEs cannot exhibit Byzantine errors (prevented by ROBUS topology)
- Simple N-modular redundancy strategies sufficient for PEs
- Redundancy management for these groupings done by the PEs

- SPIDER Update

- October 22, 2003

##  SPIDER Topology

-  SPIDER Topology

- PE 1

- PE 2

- PE 3

- ROBUSN,M

- PE N

- SPIDER Update

- October 22, 2003

## First ROBUS Prototype

- SPIDER Update

- October 22, 2003

## First SPIDER Prototype

- Picture provided by Derivation Systems, Inc. (www.derivation.com)

- SPIDER Update

- October 22, 2003

## ROBUS Requirements

- All fault-free PEs receive identical message sequences
- If the source is also fault-free, they receive the message sent
- ROBUS provides a reliable time source (RTS)
- The PEs are synchronized relative to this RTS
- ROBUS provides correct and consistent ROBUS diagnostic information to all fault-free PEs
- For 10 hour mission, P(ROBUS Failure) < 10-10

- SPIDER Update

- October 22, 2003

## Other Requirements

- Primary focus is on fault-tolerance requirements
- Other requirements unspecified
- Message format/encoding
- Performance
- These are implementation dependent
- Product Family
- capable of range of performance
- trade-off performance and reliability
- Formal analysis valid for any instance

- SPIDER Update

- October 22, 2003

## ROBUS Protocols

- Interactive Consistency (Byzantine Agreement)
- loop unrolling of classic Oral Messages algorithm
- Inspired by Draper FTP
- Distributed Diagnosis (Group Membership)
- Initially adapted MAFT algorithm to SPIDER topology
- Depends on Interactive Consistency protocol
- Verification process suggested more efficient protocol
- Improved protocol due to Alfons Geser
- Suggested further generalizations
- Clock Synchronization
- adaptation of Srikanth & Toueg protocol to SPIDER topology
- Corresponds to Davies & Wakerly approach

- SPIDER Update

- October 22, 2003

## Recap from last year

- All SPIDER fault-tolerance requirements may be realized using a repeated execution of single abstract protocol
- Basic operation is single stage middle value select
- Useful for readmission of failed nodes
- Two stage middle value select ensures validity and agreement properties for Interactive Consistency, Distributed Diagnosis, and Clock Synchronization

- SPIDER Update

- October 22, 2003

## Single Stage Middle Value Select

- mvs(a,b,c) selects middle value from set {a, b, c}

- SPIDER Update

- October 22, 2003

## Single Stage Middle Value SelectProperties

**Validity**: If there is a majority of good sources, then all good receivers select a value in the range of the good sources
**Agreement** **Propagation:** If all good sources agree, and form a majority,  then all good receivers will agree
**Agreement Generation:** If there are no asymmetric-faulty sources, then all good receivers will agree

- SPIDER Update

- October 22, 2003

## Single Stage Middle Value Select(Validity)

- min(x,z)  mvs(x,?,z)  max(x,z)
- No guarantee of agreement!  _[Demo](file:///clock_sync.exe)_

- SPIDER Update

- October 22, 2003

## Single Stage Middle Value Select(Agreement Propagation)

- SPIDER Update

- October 22, 2003

## Single Stage Middle Value Select(Agreement Generation)

- SPIDER Update

- October 22, 2003

## Current Efforts

- Constructing new PVS proofs of all protocols based on  generalized middle value select
- Have to address conflict between mathematical generality and engineering utility
- Exploiting structure to further generalize diagnosis protocol
- Support a flexible group membership policy
- Non-existence of ideal policy established this summer by Beth Latronico (NIA Intern)
- Adding transient fault recovery capabilities
- to protocols, reliability model, and formal proofs
- to lab prototypes

- SPIDER Update

- October 22, 2003

## Current Efforts (2)

- Evaluating commercial embedded real-time operating systems for use on SPIDER Processing Elements
- Evolving requirements for Processing Elements
- Adapt/extend existing embedded real-time operating system
- Time and Space Partitioning
- Fault-tolerance middleware
- Dynamic computation of communication schedules

- SPIDER Update

- October 22, 2003

## Current Efforts (3)

- Building up PVS library of reusable fault-tolerance results
- SPIDER protocols expressed within this framework
- Framework supports other network topologies
- Improved generic clock synchronization properties
- Improved accuracy results (tighter bounds)
- Cleaner structure for precision results
- Proof framework for general approximate agreement protocols (clock synchronization is special case)
- Results generalized to accomodate weaker fault assumptions (including Azadmanesh & Kieckhafer model of strictly omissive asymmetric faults)
- Preliminary support for wireless fault models

- SPIDER Update

- October 22, 2003

## Additional Resources

*A Conceptual Design for a Reliable Optical BUS (ROBUS)*; Paul Miner, Mahyar Malekpour, and Wilfredo Torres; in Proceedings 21st Digital Avionics Systems Conference (DASC) 2002
*A New On-Line Diagnosis Protocol for the SPIDER Family of Byzantine Fault Tolerant Architectures*, Alfons Geser and Paul Miner, NASA/TM-2003-212432
*A Comparison of Bus Architectures for Safety-Critical Embedded Systems,* John Rushby, NASA/CR-2003-212161

- SPIDER Update

- October 22, 2003