Challenges in the Verification
of Flight-Critical Systems
Alwyn Goodloe
NASA Langley Research Center
So, You Want to Build a Commercial
• Process starts off with a notification of intent to the FAA
– A minuet begins between the company and the regulators
– For a Part 25 aircraft there are over 1500 safety criteria you
must meet
• Autos and medical devices are easy in comparison
• DoD aircraft not subject to these regulations
• The Federal Aviation Administration (FAA) is responsible
for certifying the aircraft
– Designated Engineering Representative (DER)
• The cyber-physical component is one of the largest risk
factors for large transport aircraft
• Verification ≠ Certification & Safety ≠ Stability
– Safety is a systems level property
Eliminating Common Mode Errors
• Independence – A concept to minimize the
likelihood of common mode and cascading errors
• Diversity
– HW, SW,
• Redundancy
– Triple redundancy
– Com/Mon
• Can mix techniques
– Dissimilar com/mon
Guideline Documents
ARP 4761
• Aerospace Recommended Practice for performing
safety assessments on civil aircraft
• Guidelines and methods of performing the safety
• Functional Hazard Analysis (FHA)
• Preliminary Safety Assessment (PSA)
• System Safety Assessment (SSA)
ARP 4761 Contd.
• Safety assessment process
• Safety assessment overview
• Detailed method guidelines
Functional Hazard Assessment (FHA)
Fault-Tree Analysis (FTA)
Failure Modes and Effects Analysis (FMEA)
Common Mode Analysis (CMA)
Zonal Safety Analysis (ZSA)
Formal Methods I
• Aerospace industry has used formal methods to
analyze architectural properties of designs
– TTE protocols
• Existing certification regime very process/test
• DO-333 is an RTCA guidance document for
allowing formal methods to replace unit test for
– Explicitly mentions: syntax, semantics, soundness
– Still resolving tool qualification questions
– I encourage researchers to look at the document
Formal Methods II
• Many barriers need to be resolved before DO-333
is commonly applied
– Most engineers and regulators in the field have no
exposure to formal methods
– An education problem that has not improved much in the
US in decades
– The tool qualification regime still being resolved
Static Analysis
• Avionics software much more conservative than
most commercial software
No recursion
No dynamic memory allocation allowed
Real-time scheduling a pervasive issue
Lots of numerical code
• Most existing static analysis efforts not focused on
this class of code
– Very small market
– Some abstract interpretation tools
– More work needed
Architecture & Design
• Need more work on NEW languages and tools for
specifying and analyzing architectures and designs
of complex distributed hard real-time systems
• A hallmark of any engineering design language
should be “does it facilitate analysis?”
• Industry typically ignores semantics until too late
– Too many meaningless boxes, circles, and lines
• How we model faults and attackers should be the
one of the first questions we ask of any language
aimed at cyber physical systems (CPS) not an
Modular Certification I
• Certification authorities certify an aircraft as a whole
– Engine only component certified separately
– You build everything in conformance to standards and
– DERs sign off every step of the way
– No provision for certification by composition of certified
• Why?
• Hint: Certification is about safety
Modular Certification II
• Safety is not a compositional property
• Can assume/guarantee reasoning help?
– Assumptions must include a fault model
– How does system behave when assumptions fail?
• Little work has been done in identifying the hurdles
for modular certification
– Rushby “Modular Certification”
• Challenge lies in the intersection of formal
verification, fault tolerance, and safety-engineering
Trend in the Cockpit
• The trend in commercial aviation over the last
eighty years has been toward fewer people in the
cockpit and more automation
• As we increase automation we cannot compromise
• We should be wary of automation that overwhelms
humans with information when things go very wrong
Boeing B-314 Clipper
Boeing 707
Boeing 777
Extreme Automation
Flight Management Systems
• Flight Management Systems (FMS) – perform many
navigation and other functions
– Many FMS functions used to be performed by flight
• The FMS is a major contributor to the growth in
software complexity of avionics
– Very large code bases, databases, etc.
– Orders of magnitude more complex than the controls
• FMS are an immediate verification challenge
V&V Challenges
• The FMS allow for managing and making control
inputs, but the modes and logic have become very
complex resulting in problems that were
– Pilot input/control poses many human factors challenges
– Pilots are often expected to know what mode the system is
in when things go wrong
• Mode confusion or bad design?
• Failure of sensor data to be correct, out of date
databases, or functional correctness errors can
result in cascading indications in the flight deck
– Data integrity a huge challenge
– Logical complexity challenging traditional industrial V&V
Who Needs Humans
UAS In the NAS
• Unmanned Airborne Systems (UAS) flying in the
National Airspace (NAS) pose one of the most
significant challenges since the establishment of the
existing air traffic management system in the 1930s
• Likely to be remotely piloted or at least human
monitored for some time
• But must account for hazards where aircraft has lost
all contact with humans
• Conflict detection sense and avoid is necessary, but
not sufficient to maintain safe operation
– Still many open questions need to be resolved to build a
safety case
ICAO View of UAS & Autonomous
Aircraft I
• International Civil Aviation Organization (ICAO)
Circular 328 makes a distinction between
remotely piloted aircraft and autonomous aircraft
‒ Autonomous aircraft: an unmanned aircraft
that does not allow pilot intervention in the
management of the flight
‒ Remotely-piloted aircraft system: a set of
configurable elements consisting of a
remotely-piloted aircraft, its associated
remote pilot station(s), command and control
links and any other system elements as may
be required, at any point during flight
ICAO View of UAS & Autonomous
Aircraft II
Aircraft System
Remotely Piloted
Aircraft System
In this view, a UAS is either autonomous (fully autonomous) or it
is remotely piloted. If a human is involved in piloting the aircraft, it
is a remotely piloted aircraft. A remote pilot may have different
levels of control (which relates to automation). An autonomous
system would have no pilot interaction.
National Needs – V&V of
Autonomy I
“It is possible to develop systems having high levels of autonomy, but it is the
lack of V&V methods that prevents all but relatively low levels of autonomy
from being certified for use”;
“Developing certifiable V&V methods for highly adaptive autonomous
systems is one of the major challenges facing the entire field of control
science, and one that may require the larger part of a decade or more to
develop a fundamental understanding of the underlying theoretical principles
and various ways that these could be applied”
US Air Force Chief Scientist. "Technology Horizons: A Vision for Air Force Science &
Technology During 2010-2030." United States Air Force, Tech. Rep (2010).
“Advanced system attributes (on-board intelligence and adaptive control
laws) will be required to accommodate emerging functional requirements.
This will increase the size and complexity of control systems beyond the
capability of current V&V practices.”
Towards Safety Assurance of Trusted Autonomy in Air Force Flight Critical Systems
National Needs – V&V of
Autonomy II
“Advanced system attributes (on-board intelligence and adaptive control
laws) will be required to accommodate emerging functional requirements.
This will increase the size and complexity of control systems beyond the
capability of current V&V practices.”
Towards Safety Assurance of Trusted Autonomy in Air Force Flight Critical Systems
“NAS access for UAS is currently limited primarily due to regulatory
compliance issues and interim policies”
U.S. Department of Defense. 2011. Unmanned Systems Integrated Roadmap FY20112036
Autonomy Research for Civil Aviation:
Toward a New Era of Flight
The committee did not individually prioritize these
barriers. However, there is one critical, crosscutting
challenge that must be overcome to unleash the full
potential of advanced increasingly autonomous (IA)
systems in civil aviation. This challenge may be
described in terms of the question “How can we assure
that advanced IA systems—especially those systems
that rely on adaptive/nondeterministic software—will
enhance rather than diminish the safety and reliability of
the NAS?” There are four particularly challenging
barriers that stand in the way of meeting this key
National Research Council
Autonomy Research for
Civil Aviation: Toward a New
Era of Flight. Washington,
DC: The National
Academies Press, 2014
•Certification process
•Decision making by adaptive/nondeterministic systems
•Trust in adaptive/nondeterministic IA systems
•Verification and validation
Certifying Adaptive Systems
• Currently certification relies on predictability
– How does the system react to hazards?
• Adaptive systems that employ learning do not
satisfy this critical criteria
• How do we verify and certify that these systems are
• Driving an autonomous car several million miles
DOES NOT say anything about safety
– Train and test tradition in machine learning is a challenge
• Analysis and testing must be driven by the safety
– Functional hazard analysis, etc.
Certification Challenge
• Can we develop sophisticated autonomous
adaptive flight management systems that we can
show are safe?
– Proofs, simulations, and tests under realistic assumptions
about hazards
– Researchers need a good understanding of how current
systems get certified if they hope to get autonomous
systems certified
• Any argument must be have very strong evidence
that the resulting system is not less safe than the
current one
One Possible Path
• Given an autonomous adaptive system controlling
the aircraft that cannot be certified via conventional
means, how might we eventually find a way forward
– Expect deployment in civil aviation to be far in the future
– Adopt Lui Sha’s simplex architecture
– Apply runtime verification (RV) to ensure that the system
does not take unsafe actions
– Steer the system into a safe state when a problem
Some Issues with RV
• The runtime verification system will likely have to be
very robust, secure, and fault tolerant
– Fault model and attacker models must be realistic
• Validating the monitors a challenge
• Extensive verification of monitors will be needed
– Formal verification and testing
– Code generated must be correct
• Steering the aircraft into a safe situation once a
problem is detected is a significant challenge
Another Path
• L1 adaptive control is less exotic than many of the
proposals in adaptive control
• L1 controllers can be subject to mathematical
analysis ensuring stability and demonstrating
guaranteed bounds
– There is a level of predictability
• Preliminary investigations indicate that L1
controllers may be able to be certified under the
current regulations
• Can we develop other adaptive/learning techniques
that have similar nice properties?
Functional Hazard Analysis
• Identifies and classifies the failure conditions
associated with the aircraft functions and
combinations of aircraft functions
– Classification Levels: Minor (D), Major (C), Hazardous (B),
Catastrophic (A)
– Classifications establish safety objectives
– Output starting point for generation and allocation of safety
Copilot Architecture
Runtime Verification in Copilot
• Copilot is a runtime verification framework aimed at
hard real-time systems
– Co-developed by Lee Pike at Galois and myself
– Many Haskell hackers contributed: Robin Moriset, Nis
Wegmann, Sebastian Niller, Jonathan Laurent
• Written as a Haskell EDSL
• Composed of approximately 3000 lines of Haskell
• Copilot type system is embedded in Haskell’s
– Hindley-Milner extended with type classes
• A lot of lightweight verification so far
• Translates into C99 through Atom or SBV
Runtime Verification
• System under observation (SUO)
• Correctness property φ
– Past-time temporal logic
– Regular languages
• Monitors observe SUO and detect violations of φ
• Accept all traces admitting φ

similar documents