File preview
What Goes Wrong With Software Development And Why?*
John C. Knight
Department of Computer Science University of Virginia
November 10, 2011
*Supported in part by: National Science Foundation, AdaCore
Where Am I From?
Congress
University of Virginia
Department of Computer Science
2
University of Virginia
Software In Operation
A Mixed Record
London Ambulance Service, 1992 Therac 25, 1985-87 Ariane 5, 1996 Korean Air 801, 1997 Mars Polar Lander, 1999 Boeing 777-200, August 2005 Airbus A330, October 2008
Department of Computer Science
3
University of Virginia
What Is The Best We Could Do?
Many accidents and incidents have had software as a causative factor
Why is software imperfect? Would “better” development and analysis techniques help? Is software somehow inherently less dependable than we would like?
Where should we look for issues to address in certification?
Let’s not speculate,
Let’s do an experiment (case study) and see what we can find out
Department of Computer Science
4
University of Virginia
Design of the Case Study – 1
Goal: Develop software to be as dependable as possible
Assurance Based Development
Software
Safety Critical System Software Requirements Rigorous Assurance Argument Ultra Dependability Requirement
Department of Computer Science
5
University of Virginia
Rigorous Assurance Argument
Informally, basis of rigorous argument is:
Systematically document rationale for belief in assurance claim
Assurance deficits: Aspects of the argument where doubt remains
Analyze argument to determine how well we achieved our goal
6
Department of Computer Science
University of Virginia
Design of the Case Study – 2
Safety Critical System Software Requirements
Rigorous Assurance Argument
Rigorous Assurance Argument
Department of Computer Science
7
Assurance Deficits
University of Virginia
Assurance Based Development
The Principle
System Functional Requirements
Software Development Software
Department of Computer Science
8
System Dependability Requirements
Argument Development
Required Evidence
Process Synthesis
Supplied Evidence
Argument
University of Virginia
Assurance Based Development
Development
Success Argument
Fitness Argument
Department of Computer Science
Shrinks
Grows
Obligation
Obligation Synthesized Development Process
Support
Support
Two Arguments
9
University of Virginia
Case Study
Target: Left Ventricular Assist Device
(Joint work with Departments of Mechanical & Aerospace Engineering and Electrical & Computer Engineering)
Department of Computer Science
10
University of Virginia
Example: LVAD
Left Ventricular Assist Device
Aorta
RV
LV
Magnetic bearings Continuous-flow axial design Less blood damage than current models
University of Virginia
Department of Computer Science
11
Magnetic Bearing Control
Compute control updates in hard-real-time (5 kHz)
State-space control model, 16 states
No more than 10-9 failures per hour of operation
12
Department of Computer Science
University of Virginia
Active Mag Bearing Controller
Magnetic bearing controller is part of larger LVAD system. LVAD’s goal: adequately support patient’s circulation. Some responsibility falls on magnetic bearings. Pump housing Pump impeller Coil pair Pump clearance (blood-filled)
w-
w+
Target:
Freescale MPC5554 + custom DACs No system software
13
Department of Computer Science
University of Virginia
LVAD System Requirements
Functionality 1. Trigger and read Analog-to-Digital Converters (ADCs) to obtain impeller position vector u. 2. Determine whether reconfiguration is necessary. If so, select appropriate gain matrices A, B, D, and E. (reconfiguration to cope with coil failure) 3. Compute target coil current vector y and next controller state vector x:
y k = D × x k + E × uk xk+1 = A × xk + B × uk
4. Update DACs to output y to coil controller. Timing Reliability Execute control in hard-real-time with a frame rate of 5 kHz. No more than 10-9 failures per hour of operation.
University of Virginia
Department of Computer Science
14
Overall Development Process
ABD Process Synthesis Development
Bootstrap
Assembly Language
106 lines Implementation SPARK Ada
Device Interfaces
Formal Specification
Echo Verification
Cyclic Executive
Control Calculations
W C E T
AdaCore HI Compiler
Binary Program
2,510 lines
Testing To MCDC
Department of Computer Science
15
University of Virginia
Fitness Argument Fragment
Department of Computer Science
16
University of Virginia
Assurance Deficits
Reliance upon: Correct requirements Reliable human-to-human communication Understanding the semantics of formalisms Reviews or inspections Human compliance with protocols Unqualified tools Tools that lack complete hardware models Testing Human assessment of dependability The unavoidable use of low-level code The ability to verify floating-point arithmetic
17
Department of Computer Science
University of Virginia
Human-To-Human Communication
Problem:
Communication of technical concepts from one individual to another
Systems to software engineer, medical professionals, etc.
Those involved frequently unaware of the error
MBCS manifestations:
Use of documents in English
Formal languages Rigorous use of natural language (CLEAR method)
18
Potential mitigations:
Department of Computer Science
University of Virginia
Verification of Floating Point
Problem:
Comprehensive formal verification unavailable
MBCS manifestations:
Control equations fundamentally computational Verification using SPARK Ada tools assuming real arithmetic in bounded range
Avoid problem areas such as tests for equality Switch to fixed point Fund more research
19
Potential mitigations:
Department of Computer Science
University of Virginia
Unqualified Tools
Tools included:
SPARK Ada tools Commercial WCET analysis tools AdaCore high integrity Ada compiler (Echo verification tools) Assembler PVS Etc.
How trustworthy? How would assurance in tools be established?
Department of Computer Science
20
University of Virginia
Incomplete Hardware Models
Freescale MPC5554:
Powerful processor for embedded applications Based on Power PC Many additional “features” (A/D, timers, coprocessors)
Processor configuration required But no formal semantics of processor extensions:
Natural language definitions and best-effort engineering Significant opportunity for research:
Complex logic Complex interactions
21
Department of Computer Science
University of Virginia
Use of Low-Level Code
Problem:
Direct access to hardware Setting processor states & controlling peripherals Freescale MPC5554 processor control registers PowerPC assembly language with no verification technology Human inspection Testing Tool development and integration
22
MBCS manifestations:
Potential mitigations:
Department of Computer Science
University of Virginia
Conclusion
Assurance of dependability is crucial: We need to “know” that the system will operate properly Case study used the best software technology that we could think of Assurance deficits were many and subtle:
Many were expected, some were not Complete list is surprising Search for sources of assurance deficit Add additional vigilance – be on our guard!
23
In practice, need to:
Department of Computer Science
University of Virginia
Contact
E-mail For
address:
knight@cs.virginia.edu
more information see:
http://www.cs.virginia.edu/knight/ http://dependability.cs.virginia.edu/
Department of Computer Science
24
University of Virginia
Questions?
U.S.
U.K.
Department of Computer Science
25
University of Virginia
John C. Knight
Department of Computer Science University of Virginia
November 10, 2011
*Supported in part by: National Science Foundation, AdaCore
Where Am I From?
Congress
University of Virginia
Department of Computer Science
2
University of Virginia
Software In Operation
A Mixed Record
London Ambulance Service, 1992 Therac 25, 1985-87 Ariane 5, 1996 Korean Air 801, 1997 Mars Polar Lander, 1999 Boeing 777-200, August 2005 Airbus A330, October 2008
Department of Computer Science
3
University of Virginia
What Is The Best We Could Do?
Many accidents and incidents have had software as a causative factor
Why is software imperfect? Would “better” development and analysis techniques help? Is software somehow inherently less dependable than we would like?
Where should we look for issues to address in certification?
Let’s not speculate,
Let’s do an experiment (case study) and see what we can find out
Department of Computer Science
4
University of Virginia
Design of the Case Study – 1
Goal: Develop software to be as dependable as possible
Assurance Based Development
Software
Safety Critical System Software Requirements Rigorous Assurance Argument Ultra Dependability Requirement
Department of Computer Science
5
University of Virginia
Rigorous Assurance Argument
Informally, basis of rigorous argument is:
Systematically document rationale for belief in assurance claim
Assurance deficits: Aspects of the argument where doubt remains
Analyze argument to determine how well we achieved our goal
6
Department of Computer Science
University of Virginia
Design of the Case Study – 2
Safety Critical System Software Requirements
Rigorous Assurance Argument
Rigorous Assurance Argument
Department of Computer Science
7
Assurance Deficits
University of Virginia
Assurance Based Development
The Principle
System Functional Requirements
Software Development Software
Department of Computer Science
8
System Dependability Requirements
Argument Development
Required Evidence
Process Synthesis
Supplied Evidence
Argument
University of Virginia
Assurance Based Development
Development
Success Argument
Fitness Argument
Department of Computer Science
Shrinks
Grows
Obligation
Obligation Synthesized Development Process
Support
Support
Two Arguments
9
University of Virginia
Case Study
Target: Left Ventricular Assist Device
(Joint work with Departments of Mechanical & Aerospace Engineering and Electrical & Computer Engineering)
Department of Computer Science
10
University of Virginia
Example: LVAD
Left Ventricular Assist Device
Aorta
RV
LV
Magnetic bearings Continuous-flow axial design Less blood damage than current models
University of Virginia
Department of Computer Science
11
Magnetic Bearing Control
Compute control updates in hard-real-time (5 kHz)
State-space control model, 16 states
No more than 10-9 failures per hour of operation
12
Department of Computer Science
University of Virginia
Active Mag Bearing Controller
Magnetic bearing controller is part of larger LVAD system. LVAD’s goal: adequately support patient’s circulation. Some responsibility falls on magnetic bearings. Pump housing Pump impeller Coil pair Pump clearance (blood-filled)
w-
w+
Target:
Freescale MPC5554 + custom DACs No system software
13
Department of Computer Science
University of Virginia
LVAD System Requirements
Functionality 1. Trigger and read Analog-to-Digital Converters (ADCs) to obtain impeller position vector u. 2. Determine whether reconfiguration is necessary. If so, select appropriate gain matrices A, B, D, and E. (reconfiguration to cope with coil failure) 3. Compute target coil current vector y and next controller state vector x:
y k = D × x k + E × uk xk+1 = A × xk + B × uk
4. Update DACs to output y to coil controller. Timing Reliability Execute control in hard-real-time with a frame rate of 5 kHz. No more than 10-9 failures per hour of operation.
University of Virginia
Department of Computer Science
14
Overall Development Process
ABD Process Synthesis Development
Bootstrap
Assembly Language
106 lines Implementation SPARK Ada
Device Interfaces
Formal Specification
Echo Verification
Cyclic Executive
Control Calculations
W C E T
AdaCore HI Compiler
Binary Program
2,510 lines
Testing To MCDC
Department of Computer Science
15
University of Virginia
Fitness Argument Fragment
Department of Computer Science
16
University of Virginia
Assurance Deficits
Reliance upon: Correct requirements Reliable human-to-human communication Understanding the semantics of formalisms Reviews or inspections Human compliance with protocols Unqualified tools Tools that lack complete hardware models Testing Human assessment of dependability The unavoidable use of low-level code The ability to verify floating-point arithmetic
17
Department of Computer Science
University of Virginia
Human-To-Human Communication
Problem:
Communication of technical concepts from one individual to another
Systems to software engineer, medical professionals, etc.
Those involved frequently unaware of the error
MBCS manifestations:
Use of documents in English
Formal languages Rigorous use of natural language (CLEAR method)
18
Potential mitigations:
Department of Computer Science
University of Virginia
Verification of Floating Point
Problem:
Comprehensive formal verification unavailable
MBCS manifestations:
Control equations fundamentally computational Verification using SPARK Ada tools assuming real arithmetic in bounded range
Avoid problem areas such as tests for equality Switch to fixed point Fund more research
19
Potential mitigations:
Department of Computer Science
University of Virginia
Unqualified Tools
Tools included:
SPARK Ada tools Commercial WCET analysis tools AdaCore high integrity Ada compiler (Echo verification tools) Assembler PVS Etc.
How trustworthy? How would assurance in tools be established?
Department of Computer Science
20
University of Virginia
Incomplete Hardware Models
Freescale MPC5554:
Powerful processor for embedded applications Based on Power PC Many additional “features” (A/D, timers, coprocessors)
Processor configuration required But no formal semantics of processor extensions:
Natural language definitions and best-effort engineering Significant opportunity for research:
Complex logic Complex interactions
21
Department of Computer Science
University of Virginia
Use of Low-Level Code
Problem:
Direct access to hardware Setting processor states & controlling peripherals Freescale MPC5554 processor control registers PowerPC assembly language with no verification technology Human inspection Testing Tool development and integration
22
MBCS manifestations:
Potential mitigations:
Department of Computer Science
University of Virginia
Conclusion
Assurance of dependability is crucial: We need to “know” that the system will operate properly Case study used the best software technology that we could think of Assurance deficits were many and subtle:
Many were expected, some were not Complete list is surprising Search for sources of assurance deficit Add additional vigilance – be on our guard!
23
In practice, need to:
Department of Computer Science
University of Virginia
Contact
E-mail For
address:
knight@cs.virginia.edu
more information see:
http://www.cs.virginia.edu/knight/ http://dependability.cs.virginia.edu/
Department of Computer Science
24
University of Virginia
Questions?
U.S.
U.K.
Department of Computer Science
25
University of Virginia