A Design and Implementa0on of
an Assurance Case Language
IEEE/IFIP DSN 2014, Atlanta, Georgia, USA
Yutaka Matsuno
The University of Electro‐Communica0ons, Japan matsuno@is.uec.ac.jp
Introduc0on
• System Assurance becomes important
– Avionics, Rail, Nuclear, Off‐shore drilling plaUorm,
• Recent serious disasters
– Piper Alpha (1988), 167/229 people dead
h\p://www.dailymail.co.uk/news/ar0cle‐1031994/The‐day‐sea‐caught‐20‐years‐Piper‐Alpha‐explosion‐survivors‐finally‐able‐tell‐story.html
Report on Piper Alpha Disaster
• Risk Communica0on between design and
development companies were not sufficient
• Risk Communica0on among stakeholders is important
• Safety Cases (Assurance cases for safety) have been recognized as a promising approach for risk communica0on
Assurance Case
A structured argument, supported by a body of evidence that provides a compelling,
comprehensible and valid case that a system is dependable for a given applica0on in a given environment
Goal
Evidence
Evidence
Evidence
Argument Structure Ex: System is Dependable
Ex: Fault Injec0on Test
Current Status
• Standards: EUROCONTROL, Rail Yellow Book, MoD Defense Standard 00‐56, ISO 26262:
Func0onal Safety for Automobile, …
• “Using safety cases in industry and health care”, UK Health Founda0on, 2012.12
– Avionic, Automobile, Defense, Nuclear, Plant、 Railway, Medical Device
• USA
– Safety Case for Infusion Pomp is required by FDA
Graphical Nota0ons for
AC (Assurance Case)
• Assurance Cases become huge and complex, as target systems become so
– Wri0ng, maintaining, valida0ng, … , become difficult
– Currently, mostly wri\en in huge amount of
unstructured document by e.g., Microsom Word
• Graphical Nota0ons
– GSN (Goal Structuring Nota0on) by U of York, UK – CAE (Claim, Argument, Evidence) by Adelard, UK
Problems of GSN
Informal Defini0ons, in par0cular for Pa\ern and Module
• Pa\ern: Generalizing and reusing successful AC fragments
• Module: Scalability
Our Contribu0on
• Formally Design and Implement an AC
language based on GSN and its pa\ern and module extensions
• Show applicability of the language with exis0ng GSN examples
Contents
• Introduc0on
• GSN and Its Pa\ern and Module Extensions
• Design of AC Language
• Implementa0on of AC Language
• Related Work
• Concluding Remarks
GSN
(Goal Structuring Nota0on)
Goal
Context Strategy
Evidence
Undeveloped
EUROCONTROL RVSM
Pre‐implementa0on GSN (2001)
• RVSM: Reduced Ver0cal Separa0on Minimum
h\p://dependability.cs.virginia.edu/research/safetycases/EUR_RVSM.pdf
A- 1 Overall argument
G0
Claim that Collision Risk under RVSM is tolerable
Cr0001
1. Meet TLS for vertical risk 2. Overall risk not to increase
G1
Safety Reqts for Vertical Separation (under RVSM) are complete and correct
G2
Safety Reqts are fully realised in Concept
G3
Safety Reqts will be fully realised in Implementation of the Concept
G4
'Switchover' to RVSM will not endanger the ongoing ATS J0001
RVSM is being introduced to meet a legitimate business need
J
A0001
Pre-RVSM risk is tolerable
Top Structure of
RVSM Safety Case in GSN
GSN Pa\erns
Parameter, Mul0plicity, Choice
-+&'!.
&
%(!"'#)%
&'+% '
("'#"#&+&'!
-("'#".
&
"'%'#"&
'*"&+&'!
("'#"&%
"#",%#(&
&+&'!
("'#"&%
"$""'
"#"'%'#"&
'+ '
("'#"&#-+&'!.
"("'#"&
%#)&-("'#".
"
"'&
'#!"+
% '#"&$&
#
"'&
#
"'&''
!"'
%!"&'#
"&'"''
Parameter
Mul0plicity Choice
No Formal Defini0on
GSN Pa\erns
Loop
Figure 4 - The structure of the software contribution safety argument pattern
No Formal Defini0on
GSN Modules
GSN Community Standard v1.0
No Formal Defini0on
Contents
• Introduc0on
• GSN and Its Pa\ern and Module Extensions
• Design of AC Language
• Implementa0on of AC Language
• Related Work
• Concluding Remarks
Design Ra0onale
• Basic and General Design, which can be implemented easily
– Try to make GSN and its Pa\ern and Module extensions formal
• Func0onal Programming Framework
– The most basic and general framework in Programming Language
GSN as Tree
T ::= (g, ♦)|(g, e)|(g, st, (T
1, . . . , T
n))
“System is dependable”
(g
1, st
1, ((g
2, e
1), (g
3, ♦ )))
Pa\ern Defini0on
Parameter
• Parameter Context
Defining parameter
“System” of type string
Scope is the sub tree
Pa\ern Defini0on
Mul0plicity and Choice
• Choice
• Mul0plicity
Define Pa\ern Instan0a0on as a binary rela0on
1 2 3 1 3
Pa\ern Defini0on
(Extended from T)
• Parameter Defini0on
• Pa\ern Defini0on
d ::= ✏ | [x : ⌧ = v]
P ::= (g, ♦, d) | (g, e, d)
| (g, st, (P
1, . . . , P
n), d)
| (g, st, c(P
1, . . . , P
n), d)
| (g, st, m(P ), d)
| µα.P
Choice
Mul0plicity Loop
Some Pa\ern
Instan0a0on Rela0on
(g, e, [x : τ = ⊥]) −→
v(g[v/x], e[v/x], [x : τ = v])
Parameter Instan0a0on
(g, st, c(P1, . . . , Pn), d) {s1−→,...,sk} (g, st, (Ps1, . . . , Psk ), d)
Choice Instan0a0on
(g, st, m(P ), d) −→
k(g, st, (P, . . . , P ), d)
Mul0plicity Instan0a0on
k copies
Pa\ern Instan0a0on Example
Automobile
−→
(g, st, m(P ), d)
3
−→
(g, st, (P, P, P ), d)
(“[]
xis dependable”, ♦, [x : string = ⊥])
(“[Automobile]x is dependable”, ♦, [x : string = Automobile])
Rela0onship of
Pa\ern and Its Instance
• Normal Form: Pa\ern which can not be instan0ated anymore
• If and is normal form, then is an instance of
(g, e, ✏)
is normal form, but(g, e, m(P ), d)
is notP −→
∗I I
I P
Pa\ern Instan0a0on Algorithm
Π(P) =
case P of
(g, ♦, #) =⇒ (g, ♦, #) (g, e, #) =⇒ (g, e, #)
(g, st, (P1, . . . , Pn), #) =⇒ (g, st, (Π(P1), . . . , Π(Pn)), #) (g, ♦, [x : τ = ⊥]) =⇒ (g[v/x], ♦, [x : τ = v])
(g, e, [x : τ = ⊥]) =⇒ (g[v/x], e[v/x], [x : τ = v]) (g, st, (P1, . . . , Pn), [x : τ = ⊥]) =⇒
(g[v/x], st[v/x], (Π(P1[v/x]), . . . , Π(Pn[v/x])), [x : τ = v]) (g, st,c[i, j](P1, . . . , Pn), d) =⇒ Π((g, st, (P1, . . . , Pk), d)) (g, st,m[i, j](P), d) =⇒ Π((g, st, (P, . . . , P), d))
µα.P =⇒ Π(P[µα.P/α]) if u = µ µα.P =⇒ ♦ if u = ♦
Π(P ) = I
If
Then is an
Instance of
I
P
Module Defini0on
• A module M contains one GSN tree
• GSN defini0on with Module extensions
• Module System
T ::= ♦ | (g, ♦) | (g, e) | (g, st, (T1, . . . , Tn)) M | ref(M ) | away(M.g)
Sub
Module
Module Reference
Away Goal
M
M ::= {M1, . . . , Mn}
Contents
• Introduc0on
• GSN and Its Pa\ern and Module Extensions
• Design of AC Language
• Implementa0on of AC Language
• Related Work
• Concluding Remarks
Implementa0on
• Pa\ern and Module are implemented in
D‐Case Editor, an open source, Eclipse based GSN editor
h\p://www.dcase.jp/editor_en.html
Applicability to
Exis0ng GSN Pa\erns
Pattern Name
High-Level Software Safety Argument [13] Software Contribution Safety Argument [13] SSR Identification Software Safety Argument [13] Hazardous Contribution Software Safety Argument [13] SW Contribution Safety Argument with Grouping [13] Hazard Avoidance Pattern [18]
Fault Free Software Pattern [18]
ALARP (As-Low-As-Reasonably-Practicable) Pattern [18] Component Contributions to System Hazards [41]
Hazardous SW Failure Mode Decomposition Pattern [41] Hazardous Software Failure Mode Classification Pattern [41] Software Argument Approach Pattern [41]
Absence of Omission Hazardous Failure Mode Pattern [41] Absence of Commission Hazardous Failure Mode Pattern [41] Absence of Early Hazardous Failure Mode Pattern [41]
Absence of Late Hazardous Failure Mode Pattern [41] Absence of Value Hazardous Failure Mode Pattern [41] Effects of Other Components Pattern [41]
Handling of Hardware/Other Component Failure Mode [41] Handling of Software Failure Mode [41]
At Least As Safe Argument [4] Requirements Breakdown Pattern [7]
[13] R. Hawkins and T. Kelly. A software safety argument pattern catalogue. Technical report, The University of York, 2013. http://www-users.cs.york.ac.uk/∼rhawkins/pubs.html.
[18] Tim Kelly and John McDermid. Safety case construction and reuse using patterns. In In Proceedings of 16th International Conference on Computer Safety, Reliability and Security (SAFECOMP’97), 1997.
[41] Robert Andrew Weaver. The Safety of Software - Constructing and Assuring Arguments. PhD thesis, Department of Com- puter Science, University of York, 2003.
[4] Robert Alexander, Tim Kelly, Zeshan Kurd, and John McDer- mid. Safety cases for advanced control software: Safety case patterns. Technical report, Department of Computer Science, University of York, 2007.
[7] Ewen Denney and Ganesh Pai. A formal basis for safety case patterns. In SAFECOMP, pages 21–32, 2013.
Implemented 22 GSN pa\erns with a few modifica0ons
www.dcase.jp/pdf/pa\ernLibrary.pdf
Hazard Avoidance Pa\ern
Tim Kelly and John McDermid. Safety case construc0on and reuse using pa\erns. In In Proceedings of 16th Interna0onal Conference on Computer Safety, Reliability and Security (SAFECOMP’97), 1997.
System (X) is parameterized
Each
hazard (Y)
is parameterized
(g1, st1, m(g2, , [Y : string = ⊥]), [X : string = ⊥])
Related Work
• M.Takeyama. D‐Case in Agda
– Agda is a proof assistant/func0onal programming lang – D‐Case in Agda lets user to write AC in Agda
• User needs to understand Agda
• How much formalism should an AC lang. have?
• E.Denny, G.Pai. A Formal Basis for Safety Case Pa\erns, SAFECOMP2013
– Define GSN as unstructured control flow graph
– Defini0on and instan0a0on algorithm are complex
Concluding Remarks
• The first formal design and implementa0on of AC language with Pa\ern and Module
– Basic, General, and Easily implemented
– First Step toward Language for System Assurance
• Challenges include
– Use for real systems
– Consistency between AC and the target system
• Please visit
– h\p://www.dcase.jp/editor_en.html