Home Jp Yutaka Matsuno's Homepage matsuno

(1)

A Design and Implementa0on of

an Assurance Case Language

IEEE/IFIP DSN 2014, Atlanta, Georgia, USA

Yutaka Matsuno

The University of Electro‐Communica0ons, Japan [email protected]

(2)

Introduc0on

•  System Assurance becomes important

–  Avionics, Rail, Nuclear, Oﬀ‐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‐ﬁnally‐able‐tell‐story.html

(3)

Report on Piper Alpha Disaster

•  Risk Communica0on between design and

development companies were not suﬃcient

•  Risk Communica0on among stakeholders is important

•  Safety Cases (Assurance cases for safety) ^have been recognized as a promising approach for risk communica0on

(4)

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

Argument Structure Ex: System is Dependable

Ex: Fault Injec0on Test

(5)

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

(6)

Graphical Nota0ons for

AC (Assurance Case)

•  Assurance Cases become huge and complex, as target systems become so

–  Wri0ng, maintaining, valida0ng, … , become diﬃcult

–  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

(7)

Problems of GSN

Informal Deﬁni0ons, in par0cular for Pa\ern and Module

•  Pa\ern: Generalizing and reusing successful AC fragments

•  Module: Scalability

(8)

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

(9)

GSN Modules

GSN Community Standard v1.0

No Formal Deﬁni0on

(15)

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

(17)

GSN as Tree

T ::= (g, ♦)|(g, e)|(g, st, (T

₁

, . . . , T

ⁿ

₎₎

“System is dependable”

(g

¹

^{, st}

¹

^, ((g

²

^{, e}

¹

), (g

³

^{, ♦} )))

(18)

Pa\ern Deﬁni0on

Parameter

•  Parameter Context

Deﬁning parameter

“System” of type string

Scope is the sub tree

(19)

Pa\ern Deﬁni0on

Mul0plicity and Choice

•  Choice

•  Mul0plicity

Deﬁne Pa\ern Instan0a0on as a binary rela0on

1 ₂ ₃ ¹ 3

(20)

Pa\ern Deﬁni0on

(Extended from T)

•  Parameter Deﬁni0on

•  Pa\ern Deﬁni0on

d ::= ✏ | [x : ⌧ = v]

P ::= (g, ♦, d) | (g, e, d)

| (g, st, (P

₁

, . . . , P

ⁿ

_{), d)}

| (g, st, c(P

₁

, . . . , P

ⁿ

_{), d)}

| (g, st, m(P ), d)

| µα.P

Choice

Mul0plicity Loop

(21)

Some Pa\ern

Instan0a0on Rela0on

(g, e, [x : τ = ⊥]) ^−→

^v

(g[v/x], e[v/x], [x : τ = v])

Parameter Instan0a0on

(g, st, c(P₁, . . . , P_n_{), d)} ^{s¹^−→^,...,s^k^} _{(g, st, (P}_s₁, . . . , P_s_k _{), d)}

Choice Instan0a0on

(g, st, m(P ), d) ^−→

^k

(g, st, (P, . . . , P ), d)

Mul0plicity Instan0a0on

k copies

(22)

Pa\ern Instan0a0on Example

Automobile

−→

(g, st, m(P ), d)

3

−→

(g, st, (P, P, P ), d)

(“[]

^x

is dependable”, ♦, [x : string = ⊥])

(“[Automobile]^x is dependable”, ♦, [x : string = Automobile])

(23)

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 not

P −→

_∗

I I

I P

(24)

Pa\ern Instan0a0on Algorithm

Π(P) =

case P of

(g, ♦, #) =⇒ (g, ♦, #) (g, e, #) =⇒ (g, e, #)

(g, st, (P₁, . . . , P_n), #) =⇒ (g, st, (Π(P¹), . . . , Π(Pⁿ^{)), #)} (g, ♦, [x : τ = ⊥]) =⇒ (g[v/x], ♦, [x : τ = v])

(g, e, [x : τ = ⊥]) =⇒ (g[v/x], e[v/x], [x : τ = v]) (g, st, (P₁, . . . , P_n), [x : τ = ⊥]) =⇒

(g[v/x], st[v/x], (Π(P¹[v/x]), . . . , Π(Pⁿ[v/x])), [x : τ = v]) (g, st,^c[i, j](P₁, . . . , P_n), d) =⇒ Π((g, st, (P¹, . . . , P_k), 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

(25)

Module Deﬁni0on

•  A module M contains one GSN tree

•  GSN deﬁni0on with Module extensions

•  Module System

T ::= ♦ | (g, ♦) | (g, e) | (g, st, (T₁, . . . , Tⁿ)) M | ref(M ) | away(M.g)

Sub

Module

Module Reference

Away Goal

M

M ::= {M₁, . . . , Mⁿ}

(26)

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

(28)

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 modiﬁca0ons

www.dcase.jp/pdf/pa\ernLibrary.pdf

(29)

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

(g₁^{, st}₁_{, m(g}₂^{, ,} [Y : string = ⊥]), [X : string = ⊥])

(30)

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

–  Deﬁne GSN as unstructured control ﬂow graph

–  Deﬁni0on and instan0a0on algorithm are complex

(31)

Concluding Remarks

•  The ﬁrst 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

Home Jp Yutaka Matsuno's Homepage matsuno

A Design and Implementa0on of

an Assurance Case Language

Introduc0on

Report on Piper Alpha Disaster

Assurance Case

Current Status

Graphical Nota0ons for

AC (Assurance Case)

Problems of GSN

Our Contribu0on

Contents

GSN

(Goal Structuring Nota0on)

EUROCONTROL RVSM

Pre‐implementa0on GSN (2001)

GSN Pa\erns

Parameter, Mul0plicity, Choice

No Formal Deﬁni0on

GSN Pa\erns

Loop

No Formal Deﬁni0on

GSN Modules

No Formal Deﬁni0on

Contents

Design Ra0onale

GSN as Tree

T ::= (g, ♦)|(g, e)|(g, st, (T

, . . . , T

))

(g

, st

, ((g

, e

), (g

, ♦ )))

Pa\ern Deﬁni0on

Parameter

Pa\ern Deﬁni0on

Mul0plicity and Choice

Pa\ern Deﬁni0on

(Extended from T)

d ::= ✏ | [x : ⌧ = v]

P ::= (g, ♦, d) | (g, e, d)

| (g, st, (P

, . . . , P

), d)

| (g, st, c(P

, . . . , P

), d)

| (g, st, m(P ), d)

| µα.P

Some Pa\ern

Instan0a0on Rela0on

(g, e, [x : τ = ⊥]) −→

(g[v/x], e[v/x], [x : τ = v])

(g, st, m(P ), d) −→

(g, st, (P, . . . , P ), d)

Pa\ern Instan0a0on Example

−→

(g, st, m(P ), d)

−→

(g, st, (P, P, P ), d)

(“[]

is dependable”, ♦, [x : string = ⊥])

Rela0onship of

Pa\ern and Its Instance

(g, e, ✏)

(g, e, m(P ), d)

P −→

I I

I P

Pa\ern Instan0a0on Algorithm

Π(P ) = I

If

Then is an

Instance of

I

P

Module Deﬁni0on

₎₎

^{, st}

^, ((g

^{, e}

^{, ♦} )))

_{), d)}

_{), d)}

(g, e, [x : τ = ⊥]) ^−→

(g, st, m(P ), d) ^−→