Formal Methods in the
Aerospace Industry:
Follow the Money
ICFEM

15 November 2012
Dr. Darren Cofer
cofer@ieee.org© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Rockwell Collins
Headquartered in Cedar Rapids, Iowa
20,000 Employees Worldwide
2012 Sales of ~$4.8 Billion

Domestic
California
Carlsbad
Cypress
IrvineLos Angeles
PomonaPoway
San Francisco
San Jose
TustinFloridaMelbourne
Miami
OrlandoGeorgia
AtlantaWarner Robins
Hawaii
Honolulu
Illinois
ChicagoIowa
Bellevue
CoralvilleDecorahManchester
KansasWichita
MarylandWhite Marsh
Massachusetts
BostonMichigan
Ann Arbor
DetroitInternational
Minnesota
Minneapolis
MissouriKansas City
St. Louis
New York
New York
North Carolina
Charlotte
Raleigh
Oklahoma
Midwest City
Tulsa
OregonPortlandPennsylvania
Philadelphia
Pittsburgh
Texas
DallasFort WorthRichardson
Utah
Salt Lake City
Virginia
Sterling
Warrenton
Washington
Kirkland
RentonSeattleWashington, DC

Commercial & Military Avionics Systems
Flight Control Systems & Displays
Heads Up Displays
Navigation & Landing Systems
Defense Communications
Advanced Technology Center
Weapons Data Links
Trusted Systems group
Cryptographic Equipment(Formal Methods researchers)© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

AfricaJohannesburg, South Africa
Asia
Bangkok, Thailand
Beijing, China
Hong Kong
Hyderabad, India
Kuala Lumpur, Malaysia
Manila, Philippines
Moscow, Russia
Osaka, Japan
Shanghai, China
Singapore
Tokyo, Japan
Australia
Auckland, New Zealand
Brisbane, Australia
Melbourne, Australia
Sydney, Australia
CanadaMontreal
OttawaEuropeAmsterdam, Netherlands
Frankfurt, Germany
Heidelberg, Germany
London, England
Lyon, France
Manchester, England
Paris, France
Reading, EnglandRome, Italy
Toulouse, France
MexicoMexicaliSouth America
Santiago, Chile
Sao Jose dos Campos, Brazil
Sao Paulo, Brazil

Outline• Problem– Verification of high-assurance complex systems• Why use formal methods– Cost, safety, certification• Formal methods for verification– Model checking• Formal methods for certification– DO-178C / DO-333• What’s next
– Compositional reasoning© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

3

Domain – avionics• Embedded systems with safety and security
requirements that are critical to operation of vehicle andperformance of the mission• Commercial and military• Manned and unmanned© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

4

Software in commercial aircraft

B787: 6.5M

Boeing’s new 787 Dreamliner…requires about
6.5 million lines of software code to operate its
avionics and onboard support systems.
This Car Runs on Code, IEEE Spectrum, 2/09

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Software in military aircraft“Software providing essential JSF capability has
grown in size and complexity, and is taking longer
to complete than expected,” the GAO warned.
Pentagon: Trillion-Dollar Jet on Brink ofBudgetary Disaster, Wired 3/21/12

F-35

Source: D. Gary Van Oss (USAF), “Avionics Acquisition, Production, and Sustainment: Lessons
Learned – The Hard Way,” NDIA Systems Engineering Conference, Oct 2002.

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

The use of formal methods is motivated by the
expectation that, as in other engineering
disciplines, performing appropriate mathematicalanalyses can contribute to establishing thecorrectness and robustness of a design.

FM : software ::FEA : structure© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

7

Why use formal methods with avionics SW?
(A lesson in technology transition)• Increase confidence?
– Complete examination of complex software and requirements– “Our systems are already safe.”• Satisfy certification objectives?
– DO-178C allows certification credit for formal methods– Requirements/model verification is done by review (too cheap), andformal source/object code verification is difficult (too expensive)• Reduce cost?
– YES!
– Early detection/elimination of defects– Automation of verification activities

Follow the money.

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Formal Methods
for Verification
Formal Methods
for Certification© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

10

1
sync
2

sy nc<>

input_a3[trigger][DSTi]

[B]

DST

[C]

input_c5

Data StoreRead[status_a]status_a6[status_b]

status_b
7[status_c]status_c8
dst_index

Extract Bits
[0 3]

[A]

input_b4

Index
Vector[DSTi][A]

mon_f ailure_report

input_af ailreport[B]input_bf ailreport[status_a]status_a[status_b]

status_b[status_c]status_c

trip_level

trip_lev el

f ailure_reportprev _sel[A]

input_a1

input_b

failure_report[B]

dst_index

Failure_Isolation2

persistence_cnt<pc>

persistence_cnt

trip_lev elpc

persist_l impersistence limit[MS]persist_lim

persist_lim[trigger]tc

MS

triplex_input_monitor

totalizer_cnt<tc>

3
totalizer_cnt

[A]
[B]
[C]
[DSTi]

trigger
input_ainput_b

input_sel

4
input_sel

input_c
DST_index[prev_sel]

triplex_input_selector

STATE Transition( char *str ) {int NEXT_SYMBOL;
for( ; *str && state != INVALID; str++ ) {NEXT_SYMBOL = *str;
switch(state) {case START:
if(isdigit(NEXT_SYMBOL)) {state = INT;

MBD enhances the FM value proposition• Take advantage of– Industry adoption of Model-Based Development tools– Increasing power of formal methods analysis engines– Moore’s Law• Use formal methods to fight cost and complexity with
automation and rigor© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

[DST i]

Failure_Processing

input_c

input_cpc

trip_level1

f ailure_report[prev_sel]

[C]

DOC

– Early simulation and debugging– Automated code generation– DSL promotes higher level of abstraction
in design[MS][trigger]

[C]

T ext

doubleExtract Bits

CONCRETE

Domain-specific (often) graphical design
environments for software development

ABSTRACT

Model-based development

Barriers to use of FM• “If formal methods are so great, why aren’t they more widely
used?”• The main barriers in the past have been:
1. Cost: building/maintaining separate analysis models
2. Fidelity: models don’t match real system
3. Usability: unfamiliar notations/tools
4. Scale: inadequacy of tools for industrial-sized problems• MBD is eliminating the first three barriers– Leverages existing modeling effort– Automated translations and analysis– Familiar notations for engineers (Simulink + Stateflow)• Fourth barrier is also falling…
– Moore’s Law = more power available on desktop– Exploit rapid advances in model checking (e.g., SMT)

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Problem: bridging the gap• MBD captures design at sufficient detail and sufficient formality• Powerful formal methods tools can analyze large models• However…
– there are still a variety of models used in MBD environments– and many good analysis tools with different strengths andweaknesses{ KIND }© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Automatic translation

Gryphontranslation
framework•••

Automatictranslation
Design feedback© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Supports a wide
variety of back end
tools and languages
Straightforward to
add new tools (e.g.
Prover support
added in 4 days)
Apply “the right tool
for the job”

Translator Framework

Lustre: intermediate
representation of AST

Target CodeTranslator…
• Mechanism: Small source-to-source transformations in Lustre– Deal with one language aspect at a time
– Define pre/post-conditions that describe when transformation can be
performed and its effect– Refine Lustre specification until it resembles target language– Create language-specific emitter to output target code
© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Transformations

LustreRC

LustreRDV

LustreLustreLustreREP

LustreREN

LustreLustreRNC

LustreC Code

IAS

RFBY

RNC

PrettyPrint

IPS

LustreRC

LustreLustreRDV

LustreAda Code

PrettyPrint
PVSPretty
Print

FNH
RACT

PrettyPrint

SCA

LustreNuSMVLustreRNST

LustrePTL

LustrePrettyPrint
Prover• Different target languages use different combinations oftransformations– May be 50+ transformations for a given target• Transformations optimize final output for target language– Strengths of selected analysis engine– Speed/size/readability of source code
– Reduce analysis times from hours to seconds© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Application: Eliminate errors
ADGS-2100
Window Manager SW(cockpit display)

WM

PFD

WM

EICAS

MAP

…

PFD

Display Application
Window Manager© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

EICAS

MAP

…

ADGS-2100 model checking results
Requirement

CTL Properties

R1: If a DU is available, then it
shall display some application
R2: If a DU is unavailable, then it
shall not attempt to display any
application
R3: The cursor will not be
displayed on a DU that isunavailable
R4: The cursor shall not be
displayed on a DU whose
application is not MAP

AG( LEFT_DU_AVAILABLE -> LEFT_DU_APPLICATION != BLANK )AG( RIGHT_DU_AVAILABLE -> RIGHT_DU_APPLICATION != BLANK )AG( !LEFT_DU_AVAILABLE -> LEFT_DU_APPLICATION = BLANK )AG( !RIGHT_DU_AVAILABLE -> RIGHT_DU_APPLICATION = BLANK )AG( !LEFT_DU_AVAILABLE -> CURSOR_LOCATION != LEFT_DU )AG( !RIGHT_DU_AVAILABLE -> CURSOR_LOCATION != RIGHT_DU )AG( LEFT_DU_APPLICATION != MAP -> CURSOR_LOCATION != LEFT_DU))
AG( RIGHT_DU_APPLICATION != MAP -> CURSOR_LOCATION != RIGHT_DU)

GG

Simulink
Diagrams
2,831

PS

144

Subsystem

CM
DUF

139
879

Simulink
Blocks
10,669State Space

Properties

Errors found

9.8 x 109

43

56

398

4.6 x 1023

152

10

1,009

1.2 x 1017

169

10

2941

1.5 x 1037

115

8

84

14

563

98

MFD

302

1,100

6.8 x 1031

Totals4295

16,117n/a© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

19

Application: Eliminate errors and save money• AFRL CerTA FCS program– Team: Lockheed Martin + Rockwell Collins• Problem– The cost of software V&V for UAVs has been identified as theprimary obstacle to their future development– These costs are expected to grow rapidly as sophisticated adaptive
control systems are introduced• Measure cost and quality improvements using model checking
for verification of UAV software– Use RC model-checking tools to verify LM Aero advanced flightcontrol models– Quantify the cost and quality achieved by formal verification vs.
test-based verification

It’s a contest!

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Redundancy Manager software for UAV••

Sensor fusion, failure detection,and reset management for sets of
triply redundant sensors
Mostly discrete logic: ideal
problem for model checking

1
sync
2

sy nc<>[trigger][DSTi]

input_a
3

[B]

DST

input_b4[C]

input_c5

Data StoreRead[status_a]

Index
Vectordouble[status_b]

status_b
7[status_c][DSTi]

dst_index[A]

Triplex voter
no FHT

10 / 963 / 35 / 198

6.0 * 1013

48

5

failureprocessing

7 / 420/0/0

2.1 * 104

6

3

reset
manager

6 / 312 / 26 / 0

1.32 * 1011

8

4

Totals23 / 169

5 / 61 / 198

N/A

62

12

[MS]

mon_f ailure_report

input_af ailreport[B]input_b[C]

input_cf ailreportstatus_a[status_b]

status_b[status_c]status_c[prev_sel]

prev _sel[A]

input_a1[B]

input_b

failure_report

DOC
trip_level1

triplexmonitor

trip_lev el

f ailure_reportf ailure_reportpersistence limit[MS]persist_lim

input_c2

persistence_cnt<pc>

sensorfusionpersistence_cnt

trip_lev elpersist_lim
tcMS

triplex_input_monitor

totalizer_cnt<tc>

3
totalizer_cnt[trigger]

trigger[A]

input_a[B]

input_b[C]

input_c[DSTi]

input_sel

DST_index

triplex_input_selector© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

dst_index

Failure_Processing

pc

persist_lim[DSTi]

Failure_Isolationpc

trip_level

failureisolation[status_a]

[C]

Text

Subsystems
Charts /Reachable Properties Confirmed/ Blocks
Transitions /State
ErrorsTT Cells
Space

Extract Bits

[trigger]

status_a6status_c8Extract Bits
[0 3]

[A]

Subsystem

4
input_sel[prev_sel]

failureprocessing(logging)

Redundancy Manager counterexample
Requirement:

A sensor that does not miscompare
shall not be declared failed in the next frame.

Property:

SPEC AG((!b_miscompare & !dst_b_failed) ->AX (failure_report != b_failed));Sensor b miscompares for 4 steps.

Counterexample:
IN P U T S
in p u t_ ain p u t_ b
in p u t_ cs ta tu s _ a
s ta tu s _ b
s ta tu s _ c

0
0
0
0
0
0

3
1
3
0
0
0

3
1
3
0
0
0

3
1
3
0
0
0

3
1
3
0
0
0

3
5
5
0
0
0

OUTPUTSfa ilu re _ re p o rt
p e r s is te n c e _ c n t
to ta liz e r_ c n t

0
0
0

0
1
1

0
2
2

0
3
3

0
4
4

4
0
4

Problem:Sensor a miscompareson next step.

Sensor a is declared
failed instead of
sensor b!
(failure report “4”)Only one miscompare persistence counter© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Testing vs. Model Checking
•

•

•

•

LM and RC teams start withsame set of requirements andsoftware models
LM: Test
Both teams spent comparable
effort to add enhancements to
RC: MC
their verification framework(support for new blocks,
graphical test case viewer, XML
test case generation)
Measure effort to perform
verification and diagnose
results[FMICS 2007]© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Redundancy Manager(verification effort)
EffortErrors found

X

0

0.7X

12

RC effort
includes fixing
the errors found!

Certification• Legal recognition by the regulatory authority that a product,
service, organization or person complies with the requirements– Type certification: design complies with standards to demonstrateadequate safety, security, etc.
– Product conforms to certified type design– Certificate issued to document conformance• Examples of certification evidence– We used verification tool X to accomplish these objectives.
– These are the reasons why we think the tool is acceptable.
– We ran 1000 tests using the tool, and this is why we think these1000 tests are sufficient.
– And (almost incidentally) here are the test results.

Convincing the relevant Certification Authority that all required steps
have been taken to ensure the safety/reliability/integrity of the system© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Certification and civil aviation• Software is not actually certified• But certification of an aircraft does include “software
considerations”© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

DO-178B:“Software Considerations in Airborne Systems
and Equipment Certification”• Published in 1992
• Developed jointly by industry andgovernments from North America andEurope– Published by RTCA in U.S.
– Published by EUROCAE in Europe as ED-12B• Certification authorities agree that an
applicant can use guidance contained in
DO-178B as a means of compliance (butnot the only means) with federal
regulations governing aircraft certification• What about military aircraft?

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Overview of DO-178B• Primarily a quality document, not safety– Demonstrate that software implements requirements– and nothing else (no surprises)• Requires auditable evidence of specific processes
–
–
–
–
–
–

Software Planning
Software Development
Software Verification
Software Configuration Management
Software Quality Assurance
Certification Liaison© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Overview of DO-178B• Five Software Levels (DAL in other contexts)
A: Catastrophic (everyone dies)
B: Hazardous/Severe (serious injuries)
C: Major (significant reduction in safety margins)
D: Minor (annoyance to crew)
E: No Effect (OK to use Windows)• Objective based– Specifies what is to be achieved, not how• Different objectives and requirements for each SW level– Higher level  more objectives to be satisfied© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Verification in DO-178B• Verification = review + analysis + test
• Requirements-based testing• Traceability among– Requirements– Test cases– Code• How do we know if we have done enough testing?
– Coverage metrics to determine adequacy of testing/requirements• Two complementary objectives– Demonstrate that the software satisfies its requirements.
– Demonstrate with a high degree of confidence that errors which
could lead to unacceptable failure conditions, as determined by thesystem safety assessment process, have been removed.

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Coverage metrics• Defines structural coverage metrics– Statement coverage (A, B, C)• Every statement in the program has been invoked at least once

– Decision coverage (A, B)• and every point of entry and exit in the program has been invoked atleast once, and every decision (branch) in the program has taken on all
possible outcomes at least once

– Modified condition / decision coverage (A)• and every condition in a decision in the program has taken all possible
outcomes at least once, and each condition in a decision has been shownto independently affect that decision's outcome.

• Coverage shortcomings could indicate– Missing requirements– Inadequacy of test cases– Dead or deactivated code

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Problem: discrete nature of software
Goal: provide complete evaluation ofsoftware behavior

DO-178B Verification Objectives (Level A)
SystemRequirements
A-2: 1, 2

A-3.2 Accuracy & Consistency
A-3.3 HW Compatibility
A-3.4 Verifiability
A-3.5 ConformanceA-3.7 Algorithm Accuracy

High-Level
Requirements
A-2: 3. 4. 5

A-4. 8 Architecture Compatibility

A-4.9 Consistency
A-4.10 HW Compatibility
A-4.11 Verifiability
A-4.12 ConformanceA-4.13 Partition Integrity

A-3.1 ComplianceA-3.6 Traceability
A-7.3 CoverA-6.1 Compliance
A-6.2 Robustness
A-4.1 ComplianceA-4.6 Traceability

Design Description

SoftwareArchitecture

Low-Level
Requirements

A-7.1 Procedures
Correct

A-4.2 Accuracy & Consistency
A-4.3 HW Compatibility
A-4.4 Verifiability
A-4.5 ConformanceA-4.7 Algorithm Accuracy

Reqts-based
Tests

A-7.4 Cover

A-2: 6A-5.1 Compliance
A-5.5 Traceability

A-5.2 Compliance
A-5.3 Verifiability
A-5.4 ConformanceA-5.6 Accuracy & Consistency

SourceCode
A-2: 7A-5. 7 Complete& Correct© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

ObjectCode

A-7.5-7 Structural
Coverage
A-6.3 Compliance
A-6.4 Robustness
A-6.5 Compatible
With Target

A-7.2 Results Correct

That was 1992…
• Any changes in software technology since then?
• New SW development technologies– Object-oriented programming languages– Model-based development (MBD)• New verification technologies– Formal methods (FM)• More software!!

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

DO-178C• In late 2004, RTCA & EUROCAE agree to create jointcommittee to update DO-178B and develop DO-178C– Start: 2005
– Finish: 2008 20102011

• Terms of Reference governing update– Minimize changes to core document, yet…
– Update to accommodate 15+ years of SW experience• Strategy: Address new technologies in “supplements”– OO, MBD, FM– Also tool qualification• Other issues– Air/ground synergy (DO-278)– Rationale, consolidation, issues, errata (DO-248)© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

DO-333: Formal Methods Supplement• Objectives– No longer an “alternate method” (as in DO-178B)– Provide basis for communication between applicants & certification
authorities– Focus on verification (DO-178 section 6)– Partial use is OK– What should formal methods evidence look like?
– Define new objectives/activities/documentation (abstractions,assumptions)– Avoid common errors (check false hypotheses)• Key issues– Capturing assumptions used in analysis (constraints, assertions,environment…)– If analysis replaces unit testing, what constitutes “completeness” ofanalysis? (analog of MC/DC coverage metric)– How should formal analysis tools be qualified?

• Keep the bar high enough– Applicants with sufficient expertise© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

NASA DO-333 Case Study project

Theorem Proving
Abstract Interpretation

Model Checking© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

39

What’s next?
Compositional
Reasoning© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

40

Vision: “Integrate, then Build”• Build on success of formal verification of software components• Extend to system level via software architecture models• Goals: Early detection/elimination of bugs
– Cheaper to fix in design vs. integration– High-assurance• Hardware analogy…

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Scale and Composition• Architectural model should not capture implementation details– Component descriptions, interfaces, interconnections– Link to implementations• Assume-guarantee contracts provide the informationneeded from other modeling domains to reason about systemlevel properties– Guarantees correspond to the component requirements– Assumptions correspond to the environmental constraints that wereused in proving the component requirements– Contract specifies precisely the information that is needed to reason
about the component’s interaction with other parts of the system– Supports hierarchical decomposition of verification process• Add contracts to AADL model© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

AADL

system implementation Flight_Guidance_System.Flight_Guidance_System_Impl
subcomponents
FGP: process Flight_Guidance_Process.Flight_Guidance_Process_Impl;
connections
VNAVtoFGP: port VNAV -> FGP.VNAV;ADtoFGP: port AD -> FGP.AD;
AHtoFGP: port AH -> FGP.AH;
NAVtoFGP: port NAV -> FGP.NAV;
FCItoFGP: port FCI -> FGP.FCI;
LSItoFGP: port LSI -> FGP.LSI;
FGPtoLSO: port FGP.LSO -> LSO;
FGPtoGC: port FGP.GC -> GC;
end Flight_Guidance_System.Flight_Guidance_System_Impl;
thread implementation Control_Laws.Control_Laws_Impl
end Control_Laws.Control_Laws_Impl;© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

44

Compositional reasoning follows architecture
1
onOff

onOff

booleantrue_false
mode

2
decelSet

decelSet

1
mode
uint32enum erated

booleantrue_false3
accelResume

Typical Model-Based Design

accelResume

booleantrue_false

4cancelcancelbooleantrue_false

cruiseThrottle

3
cruiseThrottle[brakePosition ]isBrakePressed?

doublepercentage

brakePedal

5

carGearcarGearuint32
enumerated

6
carSpeed

carSpeeddesiredSpeeddoublemiles_per_hour

7validInputs

2
desiredSpeeddoublemiles_per_hour

validInputs

booleantrue_false

CruiseController

o n O ff

1
o n O ff
b o o le a no n _ o ff

1

m ode
u i n t3 2
e n u m e r a te dd e c e lS e t

2
d e c e lS e t
b o o le a no n _ o ff

m ode

3
a c c e lR e s u m em odea c c e lR e s u m eb o o le a no n _ o ff
cancel4
cancelm ode

b o o le a n
tr u e _ fa l s e

5b ra k e P e d a lb ra k e P e d a lb o o le a no n _ o ff

[ c a rS p e e d ]6
c a rG e a r

ca rS p e e dd e s ire d S p e e dd e s ir e d S p e e dd e s ir e d S p e e d

c a rG e a r

c r u i s e T h r o ttl e

2
c ru is e T h ro t t led o u b lep e r c e n ta g e

3

d o u b lem ile s _p e r_h o u r

u i n t3 2
e n u m e r a te ds e tD e s i r e d S p e e ds e tD e s i r e d S p e e d– Models are organized in ahierarchy several (many) levels
deep– Much of the complexity is in theleaf models– Leaf models can often be verified
through model checking

c a rS p e e d7
c a rS p e e d

S e t D e s ire d S p e e d[ c a rS p e e d ]d o u b lem ile s _ p e r_h o u r

G o to8v a l i d In p u t s

v a li d In p u ts

[ c a rS p e e d ]b o o le a n
tr u e _ fa l s e

c a rS p e e d

M o d e L o g ic

Composition of Subsystems

S e t T h ro t t le

– Combines heterogeneousevidence1
o n O ff

o n O ff

b o o le a no n _ o ff

22
d e c e lS e t

m o d ed ece lD e la yb o o le a no n _ o ff

= 1 S e c1m ode
u i n t3 2

desiredSpeeddoublemiles_per_hour

3
carSpeeds ets e tE ve n t

doublemiles_per_hour3a c c e lR e s u m e

doublethrottleDelta%_per_steps e tD e s i re d S p e e dre s u m e

r e s u m e E ve n t

b o o le a n

1mode

b o o le a n
tr u e _ fa l s e

1
cruiseThrottle
doublemiles_per_hour

m o d e _ lo g ic

s a fe t y C o n d i ti o n

c a rG e a r

0.0
c a rS p e e d

NOTHROTTLE
doubled o u b le
m i l e s _ p e r_ h o u r

8va l i d In p u t s

isCruiseActive?

uint32
enumerated

b ra k e P e d a l

u i n t3 2
e n u m e r a te d7
c a rS p e e d<U=100.0><L=0.0>2s e t D e s i re d S p e e d

s a f e ty C o n d i t i o n

b o o le a no n _ o ff

6
c a rG e a r<U=10.0><L=-10.0>= 1 S e ccan ce lb o o le a n
tru e _ fa ls e

5b ra k e P e d a l

StepsPerSeca cce lD e la yb o o le a no n _ o ff

4cancel1.00
thottleDelta%_per_second

va l id in p u ts

s a fe t y C o n d i t io n1z<Init = 0.0>

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

– Assume/guarantee reasoning– Well suited for theorem
provingCompositional reasoning
•

Given

•

Prove

•

Assume-Guarantee Reasoning Environment (AGREE)– Assumptions for system– Assumptions/Guarantees for components (A, P)– System guarantees (requirements)– Automatic translation of model structure, contracts, and verification
conditions– Verify via k-induction model checker (KIND/U. Iowa, Yices/SRI)

Contract compliance:
G(H(A)  P)
Example (to prove)
AS  AA
AS  PA  AB
AS  PA  PB  AC
AS  PA  PB  PC  PS

A

C

Assumption: Input < 20
Guarantee: Output < 2*Input

Assumption: none
Guarantee: Output = Input1+ Input2

B
Assumption: Input < 20
Guarantee: Output < Input + 15

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Assumption: Input < 10
Guarantee: Output < 50

46

HACMS motivation…

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

48

High Assurance Cyber-Military Systems
Network-enabled
UAVs are vulnerable
to cyber-attack

SECURE MATHEMATICALLY-ASSUREDCOMPOSITION OF CONTROL MODELSSMACCM: $18M/4.5 year project funded by DARPA
Information Innovation Office
Objective: Produce a clean-slate, formal methods–
based approach to the development of networkenabled military vehicles to build systems thatprovide the highest levels of dependability and areresistant to emerging cyber threats• Develop a complete, formally proven architecture for
UAVs (and other embedded systems) that provides
robustness against cyber attack• Develop compositional verification tools for
combining formal evidence from multiple sources,
components, and subsystems• Prototype these technologies on an open researchplatform and transfer them to a military platform todemonstrate their practicality and effectiveness• Team includes Boeing, NICTA, Galois, Univ. of MNROCKWELL COLLINS HAS ASSEMBLED A TEAM OF THE WORLD’S LEADING AUTHORITIES ON SOFTWARE VERIFICATION AND HIGHASSURANCE DEVELOPMENT TO CREATE A REVOLUTIONARY NEW WAY OF BUILDING ROBUST AND SECURE MILITARY VEHICLES© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Target: Unmanned Air Vehicles

Security vulnerabilities that can leadto safety hazards© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

50

NASA AFCS

(Assurance of Flight Critical Systems)

SysML-AADL
translation

EnterpriseArchitect

SysML
OSATE:AADL modeling

AADL

Lute:
Structuralverification

EclipseAGREE:
Compositional
behavior verification

LustreKIND© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

53

Composition ofheterogeneous evidence

Avionics
System• Avionics system requirement
Behavior

leader transition
boundedUnder single-fault assumption, GC
output transient response is boundedin time and magnitude– Guarantees provided bycomponents & design patterns– Structural properties of model– Resource allocation feasibility– Probabilistic system-level
failure characteristics

Principled mechanism for“passing the buck”

synchronous
communication

one node
operational

PALS

Rep

Structuretimingconstraints

ASSUMPTIONSGUARANTEES• Relies uponLS

notco-locatedPlatform
Resource

Probabilistic
RT sched& latency

Error
model
54

© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

Compositional reasoning for FCS (example)•

Want to prove a transient response
property
–
–

•

–

•

And guarantees provided bycomponents–•

The sensed aircraft pitch from the air
data system is within some absolutebound and doesn’t change too quickly
The discrepancy in sensed pitch
between left and right side sensors isbounded.

–Flight_Control_System

CSA

AP : Autopilot_System
GC_L

Leader selection: at least one FGS will
always be active (modulo one“failover” step)© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.

GC_R

FGSLtoAP

FGSLtoFDL

FD_L

FGSRtoAPGC

ADLtoFGSL

FM_L

NAV_L

AHLtoFGSLADRtoFGSR

AD

FGSLtoFGSR

AHRtoFGSR

AH

VNAV

FMRtoFGSR

VNAVFGSRtoFGSL

LSI

AH_R

FM_R

LSD
NAVRtoFGSR

NAV

NAVLtoFGSL

AD_R

LSI

AH

FMLtoFGSL

FD_R

FGS_R : Flight_Guidance_System

AD
LSD

AH_L

FGSRtoFDR

GC

FGS_L : Flight_Guidance_System
AD_L

NAV_R

NAV
FCI

FCI

FCItoFGSLFCItoFGSRFCIFCI : Flight_Crew_Interface
THROT_R

THROTL2FCITHROT_L

THROTR2FCI

THROT_L
YOKEL2FCIWhen a FGS is active, it will generate
an acceptable pitch rate

As well as facts provided byarchitecture

CSA

AP2CSA
Flight_Control_System_Impl

The autopilot will not cause a sharpchange in pitch of aircraft.
Even when one FGS fails and the otherassumes control

Given assumptions about theenvironment–

ibd [SysML Internal Block] Flight_Control_System_Impl [Flight_Control_System]

YOKE_L

YOKE_L

YOKE_R

YOKER2FCI

YOKE_R

THROT_R

transient_response_1 : assert true ->abs(CSA.CSA_Pitch_Delta) < CSA_MAX_PITCH_DELTA ;transient_response_2 : assert true ->abs(CSA.CSA_Pitch_Delta - prev(CSA.CSA_Pitch_Delta, 0.0))< CSA_MAX_PITCH_DELTA_STEP ;55

Conclusions• Model-based development has been key to our adoption offormal methods• Current work is expanding the size and scope ofsystems/models that can be analyzed• There are many good reasons to use formal methods forverification and certification…
• But follow the money© Copyright 2012 Rockwell Collins, Inc.
All rights reserved.