# Presentation: 907140

## Why is SPIDER Design Assurance based on Formal Methods?

- Paul S. Miner
- paul.s.miner@nasa.gov
- NASA Langley
- Internal Formal Methods Workshop
- Wednesday, October 22, 2003

## Short Answer

- One goal of the SPIDER project was to demonstrate the use of Formal Methods in support of certification for complex digital systems
- Which leads to the real question:
*Why should we use formal methods as part of our design assurance for safety-critical systems?  *

- FM for SPIDER

- October 22, 2003

## Longer Answer

**Claim:** A mature engineering discipline is characterized by principled use of analytical models
- Test is used to determine adequacy of analysis** **
- Modern engineering is rooted in Culmann’s *Graphic Statics (1865)*
**Claim:** Computer engineering is an immature discipline
- Design assurance based on testing and process assurance
- Emphasis on build-and-test is analogous to the state of engineering prior to Culmann
- Analysis used to determine adequacy of test (e.g. test coverage analysis)

- FM for SPIDER

- October 22, 2003

## Longer Answer (2)

**Claim: **Increasing logical complexity of digital avionics systems increases risk of catastrophic failure
- Current design and test paradigm is insufficient
- Need better engineering mathematics for analysis of digital systems
**Claim:** Formal Methods is the engineering mathematics for digital system design (both hardware and software)

- FM for SPIDER

- October 22, 2003

## Required Knowledge

- Mature engineering disciplines require familiarity with a variety of mathematical models
- For example, Statics and Dynamics, Maxwell’s equations
- What do we expect of a computer engineer?
- Familiarity with C

- FM for SPIDER

- October 22, 2003

## What about SPIDER?

- Why is current practice insufficient for SPIDER design assurance?

- FM for SPIDER

- October 22, 2003

## Lessons from History

- In *Design Paradigms, *Petroski argues that we should learn from the patterns of past engineering failures
- Many failures are rooted in unfounded extrapolations from earlier successful designs
- We are asking for trouble, if we continue to rely on process assurance and test
- We need better analysis techniques

- FM for SPIDER

- October 22, 2003

## What is SPIDER?

- A family of fault-tolerant Integrated Modular Avionics (FT-IMA) architectures

- FM for SPIDER

- October 22, 2003

## Fault-Tolerant Integrated Modular Avionics

- Avionics evolving from several special-purpose on-board computational platforms (each supporting a few aircraft functions) to a few computational platforms (each supporting many aircraft functions)
- Trend towards integrated modular avionics requires that we revisit fault-tolerance (FT) strategies
- IMA supports many functions of mixed criticality
- Design must enforce *partitioning* between functions of different criticality
- Even when physical faults have occurred
- Increasing dependence on COTS devices
- which are increasingly less reliable

- FM for SPIDER

- October 22, 2003

## Fault-Tolerant Integrated Modular Avionics(2)

- Loss of FT for some application might impact all critical functions
- System restart is not an attractive option
- When necessary, should be fast and (perhaps) automatic
- Must protect against cascading failures
- Shared resources make it possible to dynamically re-allocate computational/communication resources from less critical functions
- We are placing increased reliance on core computation resources, while simultaneously pushing the design envelope

- FM for SPIDER

- October 22, 2003

## SPIDER 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)

- FM for SPIDER

- 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
- _[Triplex Clock Synchronization Demo](file:///clock_sync.exe)_
- 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
- Hard to simulate, harder to test

- FM for SPIDER

- October 22, 2003

## Byzantine faults are real

- Several examples cited in *Byzantine Faults: From Theory to Reality, *Driscoll, et al. (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
- Many current architectures do not explicitly address this failure mode

- FM for SPIDER

- 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

- FM for SPIDER

- October 22, 2003

## Strength of Formal Verification

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

- FM for SPIDER

- October 22, 2003

## Summary

- Trend to FT-IMA is pushing design envelope, while simultaneously placing increased reliance on core resources
- History suggests an increased risk of engineering failure
- SPIDER project is developing formal analytical models that will allow greater design assurance for FT-IMA systems

- FM for SPIDER

- October 22, 2003