File preview
Mats Heimdahl, CASCON 2011
Assurance Cases and Software: Is there any evidence1?
1: Apologies to John McDermid for stealing from “Software Safety: Where is the evidence?”
Mats P. E. Heimdahl
University of Minnesota Software Engineering Center Department of Computer Science and Engineering University of Minnesota 4-192 EE/CS; 200 Union Street SE Minneapolis, MN 55455
Software Engineering Center Software Engineering Center
Domains of Concern
Mats Heimdahl, CASCON 2011
Software Engineering Center
Regulation and Approval Today
Process Based Standards
1. Follow these steps 2. Produce these documents 3. Hope for the best
Mats Heimdahl, CASCON 2011
Software Engineering Center
Does Current Regulation Work?
It Is Not Working (as well as it could)
• Do not necessarily lead to desired quality
– Aircraft accidents and mishaps that should not happen – Excessive number of medical device recalls – Security breaches are rampant
It Clearly Helps
• Certification and approval promotes a “quality” culture
– Helps justify the cost – Balances “get it done” with “get it right”
• Enforces rigorous process
– But limits innovation
• Rigid standards inhibit adoption of new tools and techniques • Questionable correlation between prescribed activities and failure rate • Very costly?
Mats Heimdahl, CASCON 2011
• Self selection of engineers and developers • It is the culture, not the standard or regulation, that produces quality products
Software Engineering Center
Recent Reports
• Software for Dependable Systems: Sufficient Evidence?
• Daniel Jackson, Martyn Thomas, and Lynette I. Millett, Editors, Committee on Certifiably Dependable Software Systems, National Research Council.
• Medical Devices and the Public’s Health: The FDA 510(k) Clearance Process at 35 Years
• Committee on the Public Health Effectiveness of the FDA 510(k) Clearance Process: Institute of Medicine.
Mats Heimdahl, CASCON 2011
Software Engineering Center
FDA 510(k) Process
• Demonstrate that your new device is “substantially equivalent” to a previous predicate device already on the market
Mats Heimdahl, CASCON 2011
Software Engineering Center
Certification
• The process of assuring that a product or process has certain stated properties, which are then recorded in a certificate.
– Certification usually involves assurance by an independent party, although the term is also used analogously for customer (second-party) and developer (first-party) assurance.
Adopted from NRC Report: Software for Dependable Systems: Sufficient Evidence?
Mats Heimdahl, CASCON 2011
Software Engineering Center
Goals
• Explicit claims of dependability
– A system cannot exhibit all desirable properties under all conditions; be explicit on properties, assumptions, environment, etc.
• • • •
Based on sound science Predictable and fair Risk based Facilitate innovation
Mats Heimdahl, CASCON 2011
Software Engineering Center
Claim, Evidence, and Argument
• Explicit Claims
– State explicitly what properties (safety, security, reliability, performance, etc.) the system must possess and under which assumptions
• Supporting Evidence
– Results of observing, analysing, testing, simulating and estimating the properties of a system that provide the fundamental information from which safety can be inferred
• High Level Arguments
– Explanation of how the available evidence can be reasonably interpreted as indicating acceptable dependability
Argument without Evidence is unfounded Evidence without Argument is unexplained
- Tim Kelly, 2008
Mats Heimdahl, CASCON 2011
Software Engineering Center
Assurance Cases
To construct an assurance case we need to: • make an explicit set of claims about the system • produce the supporting evidence • provide a set of arguments that link the claims to the evidence • make clear the assumptions and judgments underlying the arguments • allow different viewpoints and levels of detail.
Mats Heimdahl, CASCON 2011
Software Engineering Center
McDermid: “Software Safety: Where is the evidence?”
• Bring the Evidence!! • What Evidence????
Software meets its safety requirements 1. Inspection 2. Testing 3. Formal Verification
Mats Heimdahl, CASCON 2011
Software Engineering Center
What About Testing??
• Statistical Testing
– Does not work
• Butler and Finelli 20 years ago
• R. W. Butler and G. B. Finelli. “The Infeasibility of Quantifying the Reliability of Life-Critical RealTime Software”
• Coverage Criteria
– Does not work (yet)
• As will be shown
• Engineering Judgment
– Assisted by coverage measures – Not objective!!!
Mats Heimdahl, CASCON 2011
Software Engineering Center
MCDC as Intended in DO-178B
Requirements
Use as guidance for more test Derive Test cases
Last resort
Tests
Run test
Measure coverage
Implementation
Mats Heimdahl, CASCON 2011
Software Engineering Center
MCDC with Automation
Requirements
Use as guidance for more test Derive Test cases
Generate Last resort test data
Tests
Run test
Measure coverage
Implementation
Mats Heimdahl, CASCON 2011
Software Engineering Center
MCDC Effectiveness is Poor
Mats Heimdahl, CASCON 2011
Software Engineering Center
Except When it is Not
Mats Heimdahl, CASCON 2011
Software Engineering Center
Effect of Program Structure of # Faults Found (MCDC)
Mats Heimdahl, CASCON 2011
Software Engineering Center
Testing: We Do Not Know What We Are Doing Testing Artifacts - Relationships
Program
Specification
Oracle
Matt Staats, Michael W. Whalen, and Mats P.E. Heimdahl. Programs, Tests, and Oracles: The Foundations of Testing Revisited.
Mats Heimdahl, CASCON 2011
Test Inputs
Software Engineering Center
What About Formal Verification?
• We can mathematically prove that our program satisfies the requirements
– Requirement R is satisfied in model M
• M models R: M ⊨ R
– Rarely the case
• R is satisfied in M when M is running in the environment E • M∧E⊨R
Mats Heimdahl, CASCON 2011
Software Engineering Center
Model Checking Process
Model SMV Spec. Automatic Translation
Does the system have property X?
Yes!
SMV
Automatic Translation
March 29, 2011
Engineer
Properties
LifeScience Alley
SMV Properties
20
Software Engineering Center
Model Checking Process
Model SMV Spec. Automatic Translation
Does the system have property X?
Counter Example
No!
SMV
Automatic Translation
March 29, 2011
Engineer
Properties
LifeScience Alley
SMV Properties
21
Software Engineering Center
Why? Model Checking Process Guru
Model SMV Spec.
Automatic Translation
Does the system have property X?
?
Automatic Translation Properties
LifeScience Alley
SMV
SMV Properties
22
March 29, 2011
Engineer
Software Engineering Center
What About Formal Verification?
• We can mathematically prove that our program satisfies the requirements
– Requirement R is satisfied in model M
• M models R: M ⊨ R
M′′′ ∧ E′′′ ⊨ R′′ M′′ ∧ E′′ ⊨ R′ M′ ∧ E′ ⊨ R′ M ∧ E ⊨ R′ M∧E⊨R
Software Engineering Center
– Rarely the case
• R is satisfied in M when M is running in the environment E • M∧E⊨R
Mats Heimdahl, CASCON 2011
How we Will Develop Software (in theory)
Concept Formation
Requirements
Properties
Analysis
System
System Test
Specification/Model
Integration Test
Integration
Specification Test
Implementation
March 29, 2011
LifeScience Alley
24
Software Engineering Center
Modeling Frenzy
Concept Formation
Requirements
Properties
Modeling is so much fun
System Specification/Model
How do we know the model is “right”?
Implementation
Integration
March 29, 2011
LifeScience Alley
25
Software Engineering Center
Inappropriate Evidence
• Even perfect tools used inappropriately will harm you
– Testing tools to generate inappropriate and/or useless tests – Verification with inappropriate abstractions, simplifications, and assumptions
• Loss of collateral validation and verification
– Much validation and verification takes place by engineers working hard
• How much? Nobody knows…
Mats Heimdahl, CASCON 2011
Software Engineering Center
So, What Do We Do?
• Back to basic system safety engineering!!!
– Design hazards out of your systems
• Automation key to productivity and dependability
– I am a big supporter of tools and automation – There is still a long way to go – Improper tool use could be catastrophic
• Fundamental testing research needed
– Robust test adequacy metrics – Understand relationships between development artifacts
• Verification support
– IVE: Integrated Verification Environments – Good training materials
• Verification methodologies
Mats Heimdahl, CASCON 2011
Software Engineering Center
Infusion Pump
• When the stop button is pressed, the current pump stroke shall be completed prior to stopping the pump. • We could verify in our software, or…
Not Actual Device
Mats Heimdahl, CASCON 2011
Software Engineering Center
So, What Do We Do?
• Back to basic system safety engineering!!!
– Design hazards out of your systems
• Automation key to productivity and dependability
– I am a big supporter of tools and automation – There is still a long way to go – Improper tool use could be catastrophic
• Fundamental testing research needed
– Robust test adequacy metrics – Understand relationships between development artifacts
• Verification support
– IVEs: Integrated Verification Environments – Good training materials
• Verification methodologies
Mats Heimdahl, CASCON 2011
Software Engineering Center
Discussion
Mats Heimdahl, CASCON 2011
Software Engineering Center
Assurance Cases and Software: Is there any evidence1?
1: Apologies to John McDermid for stealing from “Software Safety: Where is the evidence?”
Mats P. E. Heimdahl
University of Minnesota Software Engineering Center Department of Computer Science and Engineering University of Minnesota 4-192 EE/CS; 200 Union Street SE Minneapolis, MN 55455
Software Engineering Center Software Engineering Center
Domains of Concern
Mats Heimdahl, CASCON 2011
Software Engineering Center
Regulation and Approval Today
Process Based Standards
1. Follow these steps 2. Produce these documents 3. Hope for the best
Mats Heimdahl, CASCON 2011
Software Engineering Center
Does Current Regulation Work?
It Is Not Working (as well as it could)
• Do not necessarily lead to desired quality
– Aircraft accidents and mishaps that should not happen – Excessive number of medical device recalls – Security breaches are rampant
It Clearly Helps
• Certification and approval promotes a “quality” culture
– Helps justify the cost – Balances “get it done” with “get it right”
• Enforces rigorous process
– But limits innovation
• Rigid standards inhibit adoption of new tools and techniques • Questionable correlation between prescribed activities and failure rate • Very costly?
Mats Heimdahl, CASCON 2011
• Self selection of engineers and developers • It is the culture, not the standard or regulation, that produces quality products
Software Engineering Center
Recent Reports
• Software for Dependable Systems: Sufficient Evidence?
• Daniel Jackson, Martyn Thomas, and Lynette I. Millett, Editors, Committee on Certifiably Dependable Software Systems, National Research Council.
• Medical Devices and the Public’s Health: The FDA 510(k) Clearance Process at 35 Years
• Committee on the Public Health Effectiveness of the FDA 510(k) Clearance Process: Institute of Medicine.
Mats Heimdahl, CASCON 2011
Software Engineering Center
FDA 510(k) Process
• Demonstrate that your new device is “substantially equivalent” to a previous predicate device already on the market
Mats Heimdahl, CASCON 2011
Software Engineering Center
Certification
• The process of assuring that a product or process has certain stated properties, which are then recorded in a certificate.
– Certification usually involves assurance by an independent party, although the term is also used analogously for customer (second-party) and developer (first-party) assurance.
Adopted from NRC Report: Software for Dependable Systems: Sufficient Evidence?
Mats Heimdahl, CASCON 2011
Software Engineering Center
Goals
• Explicit claims of dependability
– A system cannot exhibit all desirable properties under all conditions; be explicit on properties, assumptions, environment, etc.
• • • •
Based on sound science Predictable and fair Risk based Facilitate innovation
Mats Heimdahl, CASCON 2011
Software Engineering Center
Claim, Evidence, and Argument
• Explicit Claims
– State explicitly what properties (safety, security, reliability, performance, etc.) the system must possess and under which assumptions
• Supporting Evidence
– Results of observing, analysing, testing, simulating and estimating the properties of a system that provide the fundamental information from which safety can be inferred
• High Level Arguments
– Explanation of how the available evidence can be reasonably interpreted as indicating acceptable dependability
Argument without Evidence is unfounded Evidence without Argument is unexplained
- Tim Kelly, 2008
Mats Heimdahl, CASCON 2011
Software Engineering Center
Assurance Cases
To construct an assurance case we need to: • make an explicit set of claims about the system • produce the supporting evidence • provide a set of arguments that link the claims to the evidence • make clear the assumptions and judgments underlying the arguments • allow different viewpoints and levels of detail.
Mats Heimdahl, CASCON 2011
Software Engineering Center
McDermid: “Software Safety: Where is the evidence?”
• Bring the Evidence!! • What Evidence????
Software meets its safety requirements 1. Inspection 2. Testing 3. Formal Verification
Mats Heimdahl, CASCON 2011
Software Engineering Center
What About Testing??
• Statistical Testing
– Does not work
• Butler and Finelli 20 years ago
• R. W. Butler and G. B. Finelli. “The Infeasibility of Quantifying the Reliability of Life-Critical RealTime Software”
• Coverage Criteria
– Does not work (yet)
• As will be shown
• Engineering Judgment
– Assisted by coverage measures – Not objective!!!
Mats Heimdahl, CASCON 2011
Software Engineering Center
MCDC as Intended in DO-178B
Requirements
Use as guidance for more test Derive Test cases
Last resort
Tests
Run test
Measure coverage
Implementation
Mats Heimdahl, CASCON 2011
Software Engineering Center
MCDC with Automation
Requirements
Use as guidance for more test Derive Test cases
Generate Last resort test data
Tests
Run test
Measure coverage
Implementation
Mats Heimdahl, CASCON 2011
Software Engineering Center
MCDC Effectiveness is Poor
Mats Heimdahl, CASCON 2011
Software Engineering Center
Except When it is Not
Mats Heimdahl, CASCON 2011
Software Engineering Center
Effect of Program Structure of # Faults Found (MCDC)
Mats Heimdahl, CASCON 2011
Software Engineering Center
Testing: We Do Not Know What We Are Doing Testing Artifacts - Relationships
Program
Specification
Oracle
Matt Staats, Michael W. Whalen, and Mats P.E. Heimdahl. Programs, Tests, and Oracles: The Foundations of Testing Revisited.
Mats Heimdahl, CASCON 2011
Test Inputs
Software Engineering Center
What About Formal Verification?
• We can mathematically prove that our program satisfies the requirements
– Requirement R is satisfied in model M
• M models R: M ⊨ R
– Rarely the case
• R is satisfied in M when M is running in the environment E • M∧E⊨R
Mats Heimdahl, CASCON 2011
Software Engineering Center
Model Checking Process
Model SMV Spec. Automatic Translation
Does the system have property X?
Yes!
SMV
Automatic Translation
March 29, 2011
Engineer
Properties
LifeScience Alley
SMV Properties
20
Software Engineering Center
Model Checking Process
Model SMV Spec. Automatic Translation
Does the system have property X?
Counter Example
No!
SMV
Automatic Translation
March 29, 2011
Engineer
Properties
LifeScience Alley
SMV Properties
21
Software Engineering Center
Why? Model Checking Process Guru
Model SMV Spec.
Automatic Translation
Does the system have property X?
?
Automatic Translation Properties
LifeScience Alley
SMV
SMV Properties
22
March 29, 2011
Engineer
Software Engineering Center
What About Formal Verification?
• We can mathematically prove that our program satisfies the requirements
– Requirement R is satisfied in model M
• M models R: M ⊨ R
M′′′ ∧ E′′′ ⊨ R′′ M′′ ∧ E′′ ⊨ R′ M′ ∧ E′ ⊨ R′ M ∧ E ⊨ R′ M∧E⊨R
Software Engineering Center
– Rarely the case
• R is satisfied in M when M is running in the environment E • M∧E⊨R
Mats Heimdahl, CASCON 2011
How we Will Develop Software (in theory)
Concept Formation
Requirements
Properties
Analysis
System
System Test
Specification/Model
Integration Test
Integration
Specification Test
Implementation
March 29, 2011
LifeScience Alley
24
Software Engineering Center
Modeling Frenzy
Concept Formation
Requirements
Properties
Modeling is so much fun
System Specification/Model
How do we know the model is “right”?
Implementation
Integration
March 29, 2011
LifeScience Alley
25
Software Engineering Center
Inappropriate Evidence
• Even perfect tools used inappropriately will harm you
– Testing tools to generate inappropriate and/or useless tests – Verification with inappropriate abstractions, simplifications, and assumptions
• Loss of collateral validation and verification
– Much validation and verification takes place by engineers working hard
• How much? Nobody knows…
Mats Heimdahl, CASCON 2011
Software Engineering Center
So, What Do We Do?
• Back to basic system safety engineering!!!
– Design hazards out of your systems
• Automation key to productivity and dependability
– I am a big supporter of tools and automation – There is still a long way to go – Improper tool use could be catastrophic
• Fundamental testing research needed
– Robust test adequacy metrics – Understand relationships between development artifacts
• Verification support
– IVE: Integrated Verification Environments – Good training materials
• Verification methodologies
Mats Heimdahl, CASCON 2011
Software Engineering Center
Infusion Pump
• When the stop button is pressed, the current pump stroke shall be completed prior to stopping the pump. • We could verify in our software, or…
Not Actual Device
Mats Heimdahl, CASCON 2011
Software Engineering Center
So, What Do We Do?
• Back to basic system safety engineering!!!
– Design hazards out of your systems
• Automation key to productivity and dependability
– I am a big supporter of tools and automation – There is still a long way to go – Improper tool use could be catastrophic
• Fundamental testing research needed
– Robust test adequacy metrics – Understand relationships between development artifacts
• Verification support
– IVEs: Integrated Verification Environments – Good training materials
• Verification methodologies
Mats Heimdahl, CASCON 2011
Software Engineering Center
Discussion
Mats Heimdahl, CASCON 2011
Software Engineering Center