# Presentation: 139341

## The Nation’s Needs in Formal Methods

- Amy R. Pritchett
- Director, NASA Aviation Safety Program
- April 30, 2008

## What are Formal Methods?

**For****·****mal** -adjective
- 17. pertaining to the form, shape, or mode of a thing, esp. as distinguished from the substance: *formal writing, bereft of all personality. *
- 18.being such merely in appearance or name; nominal: *a formal head of the government having no actual powers. *
- 19.*Mathematics. *
- a.(of a proof) in strict logical form with a justification for every step.
- b.(of a calculation) correct in form; made with strict justification for every step.
- c.(of a calculation, derivation, representation, or the like) of or pertaining to manipulation of symbols without regard to their meaning.
*Formal* may mean in proper form, or may imply excessive emphasis on empty form [i.e.] arbitrary, forced, or meaningless conformance to mere rules or belief in impractical theories.

## Trying Again: What are Formal Methods?

**Formal methods** are mathematically-based techniques for the specification, development and verification of software and hardware systems.
- Note: We could argue over the extent to which we are considering meaning ‘versus’ form

## What is Software?

- Software is
- The description of a human concept or abstraction as based on subjective reality
- Implemented according to some form
- A form relatively unconstrained compared to hardware
- Intended to create some behavior acting on an objective reality
- Automation is the software’s manifestation

## The Philosophic View of Software

- Objective Reality

- Subjective Reality

- Abstraction

- Software/Automation

## Trying Again: What are Formal Methods?

**Formal methods** are mathematically-based techniques for the specification, development and verification of software and hardware systems.
- Corollary: This requires examination of more than just software and hardware

## Why Formal Methods?

- Software cost
- Cost of a ‘failure’
- Special needs of new systems

## Why Formal Methods?

- Software cost
- Cost of a ‘failure’
- Special needs of new systems

## Design Assurance Level 

| Level | Failure condition |  | Objectives | Independence |
| --- | --- | --- | --- | --- |
| A | Catastrophic | Failure may cause a crash | 66 | 25 |
| B | Hazardous | Failure has a large negative impact on safety or performance, or reduces the ability of the crew to operate the plane due to physical distress or a higher workload, or causes serious or fatal injuries among the passengers. | 65 | 14 |
| C | Major | Failure is significant, but has a lesser impact than a Hazardous failure (for example, leads to passenger discomfort rather than injuries). | 58 | 2 |
| D | Minor | Failure is noticeable, but has a lesser impact than a Major failure (for example, causing passenger inconvenience or a routine flight plan change)  | 28 | 2 |
| E | No effect |  | 0 | 0 |

## SLOC-Cost

- Software Development Productivity for Industry Average Projects*
- 	Cost from requirements analysis through software Integration and test
- 	Assuming a full cost rate of $150k/year/person the cost for one line of new embedded flight software is between $735 and $119 per line of source code
- * Lum, Karen Et, *Handbook for Software Cost Estimation. *May 30, 2003, JPL D-26303, Rev 0, Jet Propulsion Laboratory
- 			
- 		

| Characteristic Software Development Productivity | Source Line of Code/Work Month
(SLOC/WM) |
| --- | --- |
| Classic rates | 130-195 |
| Evolutionary approaches | 244-325 |
| New embedded flight software | 17-105 |

## ... and There’s A Lot of SLOC!

- Modern flight management systems run to the millions of SLOC*
- All told, software development is often more than 50% of the development cost*
**** anecdotally***

## Reducing Software Cost

- Intervening early through a systematic process
- Formal methods for specification
- Auto-coding
- Formal methods for verification
- Using automation
- Need it to be fast
- Need it to be interpretable

## Review of Formal Methods

- Much of the effort has been on verification:
- Automated analysis of an established heuristic or mathematical proof
- Automated theorem proving: system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules.
- Model checking: system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules.

## Gödel: Axiomatic Methods Have Limits!

- Gödel’s Theorem: for any computable axiomatic system powerful enough to describe the arithmetic of the natural numbers, then:
- If the system is consistent, then it can not be complete (“Incompleteness theorem”).
- The consistency of the axioms cannot be proved within the system.

## What if the Software is (Essentially) Internally Complete?

***Then we are probably missing something!***

## Should We Follow Gödel Into Illogical Extremes?

*“**Einstein and Morgenstern coached Gödel for his U.S. citizenship exam, concerned that their friend's unpredictable behavior might jeopardize his chances. *
*“**When the Nazi regime was briefly mentioned, Gödel informed the presiding judge that he had discovered a way in which a dictatorship could be legally installed in the United States, through a logical contradiction in the Constitution.*
*“**Neither judge, nor Einstein or Morgenstern allowed Gödel to finish his line of thought and he was awarded citizenship.”*
*May we have the same common sense!*

## Review of Efforts to Establish Cost-Effective Formal Methods

- No one silver bullet
- A method will need to ‘buy its way’ into the development process
- Several methods may be needed
*To err is human, but to really foul things up you need a computer. by *_[Paul Ehrlich](http://www.whatquote.com/authors/3170-Paul-Ehrlich.htm)_
*Program testing can be used to show the presence of bugs, but never to show their absence! *_[Edsger](http://www.brainyquote.com/quotes/authors/e/quotes/quotes/e/edsgerdijk201165.html)__[ ](http://www.brainyquote.com/quotes/authors/e/quotes/quotes/e/edsgerdijk201165.html)__[Dijkstra](http://www.brainyquote.com/quotes/authors/e/quotes/quotes/e/edsgerdijk201165.html)_

## Why Formal Methods?

- Software cost
- Formal methods can help manage complexity
- Cost of a ‘failure’
- Will it work in the operating environment?
- Special needs of new systems

## Let’s Situate Our Limited Picture

- We may have created a beautiful picture...But does it cover the operating environment?

## Describing Automation 

- Robustness: The range of operating conditions with satisfactory performance
- Autonomy:
- (Engineering): The sophistication of the automation’s behaviors when objective and subjective reality overlap – regardless of problems with robustness
- (Management): The ability to go do any task, no matter how simple, and report back when the manager should know anything

## An Authoritative Source on Automation...

- Maximum Homerdrive:
- Homer Beats Truck Driver in Texas Steak-Eating Contest
- Truck-Driver Keels Over and Dies
- Homer Ends Up Driving Truck

## Homer Gets Sleepy...

*Automatic Truck Driver Kicks In!*

## Truck Skids Around Mountain, Drives to Safety

*Homer Wakes Up With Truck Sitting at Gas Station*

## Sometimes Automation Works Well!

## The Other Truck Drivers Get Mad

## And Try to Run Down Homer

## ‘Save Me, Automation!’*

- *Note operation outside boundary conditions

## There Is Much Chaos...

*And Homer Saves the Day.*

## But That’s a Cartoon!  It Doesn’t Happen in Real-life...

- May 12, 1997
- AA Flight 903 descends to 16,000’ as it near Miami
- Something ‘upset’ the aircraft
- Flight control oscillations for 34 seconds
- Lost 3000’ altitude
- The maneuvering exceeded some internal software check-limit
- The flight instrumentation databus reset itself
- The EFIS showed only black with white diagonal slash marks while the pilots were trying to recover

## Another Example: Airbus A320

- Built In ‘Stall’ Protection
- Won’t Let Airplane Climb Too Steeply
- When Close to Ground, Helps Pilot Land Airplane
- Pilot Doesn’t Control Airplane Directly -- Instead, ‘Asks’ Computer Through Controls for Changes
- Overall, Works Great In Normal Conditions!

## Airshow Flyby

- June 26, 1988 – Habsheim, France

## Implications for Formal Methods

- We check the software
- We check the requirements to the software
- We check the requirements to reality?
- Including changing circumstances?

## Why Formal Methods?

- Software cost
- Formal methods can help manage complexity
- Cost of a ‘failure’
- Will it work in the operating environment?
- Will it work with the pilot?
- Special needs of new systems

## ‘Human Error’

- Can anyone name an accident not caused by ‘human error’?
- Formal methods generally used to examine for ‘designer/coder/specifier error’
- Formal methods can also be used to identify likely ‘pilot error’ of particular types
- E.g., will the pilot properly understand the Flight Management System?

## Automated Cockpit?

## Human-Automation-Interaction and Complexity

- One issue with automation is its complexity
- E.g. 757/767 has 250+ autoflight modes
- Pilots normally trained on ‘common’ modes
- Accidents occurring with ‘rare’ modes
- Measuring ‘complexity’ is hard
- Has many elements
- Number of modes (simplistic)
- Consistency of behaviors between modes (allowing for inferential reasoning)
- Consistency of behaviors of a mode (dissuading frequential simplification)

## Interaction Mechanism

## A Finite State Machine...

- Taken from the work of Denis Javaux:
- To operate this machine, one needs to know...
- What state you’re in
- Under what conditions the state will transition automatically
- What you would need to do to command a transition yourself
- And under what conditions this transition will and won’t happen!

## For Example: Will You End Up With Both Autopilots Engaged?

- Note: Some of these conditions are ‘tricky’!
- 	Rarely seen (frequential problem)
- 	Not-like other conditions (inferential problem)

## Here’s the Case of an Automatic Transition...

- If the pilot setups the aircraft right
- ‘Nav’ mode engaged and ‘Clb’ mode armed
- AND once some conditions are later met
- THEN the system will go into ‘Clb’ mode

## Simplification: A Logical Behavior

- Reality:

- Believed by the pilot, based on common experience:

## Formal Methods in HAI

- For finite state machines, structured, verified, demonstrated methods now exist to go through the structure of the finite state machine
- Highlight rare, unusual, un-predictable conditions in which the pilot will:
- Not predict an automatic mode transition
- Not predict correctly the response to a command
- Can be used to go through a system design, highlighting problems
- Hopefully, designers will then re-think their designs as much as possible, possibly simplifying them
***Note, Denis Javaux’s work is now proprietary to Airbus...***

## Why Formal Methods?

- Software cost
- Formal methods can help manage complexity
- Cost of a ‘failure’
- Will it work in the operating environment?
- Will it work with the pilot?
- Will it work with (continuous) flight dynamics?
- Special needs of new systems

## Software Control of (Continuous) Dynamics?

- First digital flight control system: F-8

## Modern Software Control of Continuous Dynamics?

- Flight demonstration of the YF-22

## Current ‘Formal Methods’ for Continuous Dynamics?

- Heuristics to check for pilot controllability
- Specifications (e.g., gain and phase margin) for closed-loop stability
- ‘Tell me what the control gains will be in every flight condition within the operating envelope’
***Can they have a closer tie to (discrete formalism-based) formal methods?***

## Why Formal Methods?

- Software cost
- Formal methods can help manage complexity
- Cost of a ‘failure’
- Will it work in the operating environment?
- Will it work with the pilot?
- Will it work with (continuous) flight dynamics?
- Special needs of new systems
- Adaptive systems

## Adaptive Systems

- What if we want a system that can adapt to conditions outside the (nominal) flight envelope?
- We can’t describe *a priori* its behavior
- Maybe we would need to ask different questions:
- “Is it possible for the adaptive system to cause harm?”
- “Can the adaptive element recover from a failure in adaptation?”
- “Is there a way to verify the adaptation function (in flight test) without risk to the vehicle?”

## Why Formal Methods?

- Software cost
- Formal methods can help manage complexity
- Cost of a ‘failure’
- Will it work in the operating environment?
- Will it work with the pilot?
- Will it work with (continuous) flight dynamics?
- Special needs of new systems
- Adaptive systems
- Emergent behaviors

## Emergence

- Emergence: Behaviors observed at one level of abstraction which can not be predicted  (maybe not explained!) at a different level of abstraction
- Example:
- An unstable compression wave in a traffic stream in which each aircraft is individually stable
- My hypothesis: Many aspects of complex system safety (and issues) are emergent phenomenon
- How does analysis at one level extrapolate to another?

## Represent This...

- Abstraction is necessary...

## Many Possible Abstractions!

## Why Formal Methods?

- Software cost
- Formal methods can help manage complexity
- Cost of a ‘failure’
- Will it work in the operating environment?
- Will it work with the pilot?
- Will it work with (continuous) flight dynamics?
- Special needs of new systems
- Adaptive systems
- Emergent behaviors

## Why Formal Methods?

- Key Challenges Identified in the Decadal Survey of Civil Aeronautics include:
- Aircraft systems:
- D4: Intelligent and adaptive flight control techniques
- D5: Fault-tolerant and integrated VHM
- D7: Advanced comm, nav and surveillance
- D8: Human-machine integration
- D11: Network-centric avionics architectures
- D12: Smaller, lighter and less expensive avionics
- D13: More efficient certification processes
- D14: Design, development and upgrade processes for complex, software-intensive systems
***Formal Methods Can Be Pivotal!***

## Why Formal Methods?

- Key Challenges Identified in the Decadal Survey of Civil Aeronautics include:
- Complex systems (including multi-vehicle / airspace):
- E1: Methodologies, tools and simulation and modeling to design and evaluate complex interactive systems
- E6: Vulnerability analysis as an integral element in architecture design [of the air transportation system].
- E12: Autonomous flight monitoring
- E16: Appropriate metrics [of air transportation systems]
- E19: Provably correct protocols for fault-tolerant aviation communication systems.
- E20: Comprehensive models and standards for designing and certifying aviation networking and comm systems.
***Formal Methods Can Be Pivotal!***

## The Nation’s Needs in FM

- Aircraft systems are unbelievably complex
- NextGen is the biggest engineering challenge... ever
- Safety must be demonstrated to levels hitherto unimaginable
- The challenge to the FM community:
- Make the theory consistent and complete
- Make its application cost- and time-effective
- Work with the community to demonstrate the new capability they provide
- Oh, and as a program director let me add, do it on-budget and on-time?

## Thank You!

- Special thanks to:
- Steve Jacobson, DFRC & HQ
- Eric Feron & Eric Johnson, Georgia Tech
- Denis Javaux
- John Wheeler, LM
- Duane McRuer, STI
- ATAC Corp.