Home

justifying software systems safety using arguments

1. Java EE dcaseTest test dcase_diagram Eclipse Users yutaka Documents workspace Pie 04 GG qe 2 Q 14 Sr o ES el java EE Tahoma sem Bie Bo Sao Project E 22 B testdcase diagram 12 d ET2011_D_Case2011090 4 T2011_D_Case2011092 4 ET2011 dcase_diagram y 2 b 2 4 6 8 WY TV i i i 16 1 Palette b uz dcase RAAD gt 13 D CaseTemplate example dcase_model gt 3 dcaseTest Nodes functionality dcase_model D Coal reliability dcase_model Context C_1 Strategy Operational Range of O Evidence Response time delay Response Time failures can be monitored and 0 50ms Normal im Monitor recovered 0ms Failure Undeveloped Context CD justificar S System Policy gt Option Nodes userdef001 Userdefoo2 O casic E Userdef003 Response time uz O Userdetoos failure can be Ti print O Seripe O Userdetoos Userdef006 Links K unk im Monitor M_1 ff Unk Test Result Link Log Analysis N Link Figure 3 3 D case editor tool screenshot A tool for integrating informal and formal reasoning has been proposed in 3 The focus is on tracing requirements from natural language representation towards formal prop erties verified using model checking The tool is a plugin for Eclipse developed on top of ProR plugin for tracing natural language requirements and Rodin for modelling properties in the Event B language For implementing the reasoning feature of
2. TBOX We translate the GSN standard into description language representing the Tbox and for each diagram builded the user can transform the diagram into description language representing the A box part Both parts are loaded in the RacerPro reasoning engine which will be used used by our tool to query and validate the Abox against the GSN Tbox Querying the Diagram Scenario The flow of this action is represented in figure 4 8 Below is presented the steps necessary without interruptions for querying from console a selected diagram Happy flow 1 User opens or creates a diagram 2 Select translating the diagram in abox 3 System returns the racer file contaning the abox 4 User loads the diagram 38 CHAPTER 4 ANALYSIS AND THEORETICAL FOUNDATION 5 User selects the command console 6 User enters query in console 7 System displays the results in the console In the extended flow are presented the interruptions that might occur when trying to complete this action Extended flow 4 1 Racer engine is not found 4 1 1 System notifies the user that RacerPro was not found 4 1 2 The user starts manually the engine 6 1 Console is not visible 6 1 1 User open window gt show perspectives gt console 6 1 2 System displays the console view 6 1 3 User selects Command Console from the console view 6 1 4 System displays the command console 6 1 Racer engine stopped working 6 1 System notifies the user that RacerPro was not f
3. 18 18 18 18 19 19 20 22 28 28 29 31 31 34 35 37 37 38 40 40 5 2 Implementation details PE od Aa ge a a es a es eed 521 GSN PlugIns A eek ala ee he ee ek 5 2 2 GSN ontology plug ins ee OR e ee E 3 A A SY S Q SUS Chapter 6 Testing and Validation 6 Testing the tool ce dank oe rn to wae le le U a s e fe Chapter 7 User s manual 7 1 System Installation assi dd dale s dele Be deh dok r Users Manual rria is as Pala ads date DO b ici Chapter 8 Conclusions 8 1 Contributions and Achievements 22 Bibliography Appendix A Published papers 15 63 63 64 67 67 68 69 71 Chapter 1 Introduction Chapter 1 describes the problem statement and its solution In the past few years the number of safety critical systems has grown the question is how do we know if they are safely made and secure any system that presents a certain level of risks must prove that its behavior should be trusted Nowadays software safety assurance is often demonstrated by compliance with national or international safety standards The assurance cases are used to decide if the system is safe and secure solely from the provided evidence Their usage has grown in the last years and in certain domains like the nuclear field it is mandatory to build a safety case This proves that currently assura
4. 7 1 Autonomous vehicle scenario 7 2 Command Console Contents List of Tables List of Figures Chapter 1 Introduction 1 1 Organization of the paper nti ira a E cat Chapter 2 Project Obectives and Specifications 2 1 Problem Statement and Solution eo ou ela E ES E aya 2 2 Goals and Objectives o a ee we ee A 2 2 1 Bussiness Goals and Objectives aa m S p ul eg wk 2 2 2 Project Goals and Objectives s 4 D eo ds 2 3 Functional requirements 2 4 ira eee bees PEA ey i 2 4 Non functional requirements Chapter 3 Bibliographic research Chapter 4 Analysis and Theoretical Foundation 41 Safety Case s s b nd os a s SA ONS a lat ae s Ab 1500260202 staridard pis ra s edi NAB DAR a 42 Goal Structuring Notification vasi i446 ig 46 eke 46 eka ees 42 1 Elements of GSN we eS 4 3 Description Language vena Gude So de See ie Se a ie la e Gee d 4 4 Modeling the GSN Standard in Description Logic 4277 F ncHonality x Lia ili i s eR eee MT 45 1 Diagram translation and Reasoning in safety arguments 45 2 Validating the Safety Case 2 araz dab oh Pia AN s y R Hava 4 5 3 Generation of Safety Case Metrics 4 5 4 Generating Natural Language Reports on the Safety Case Chapter 5 Detailed Design and Implementation 5 1 System Architecture ay ata E A MES i AGNESE i RR DE aaa 11 16 17
5. e accomplish project business goals and objectives e supports automated construction and assessment of safety cases e that can be used to justify the correctenes of the users critical systems and if systems obeys the international standards e translates the safety case into description logic e uses reasoning services for better assesment of safety cases e validates the safety case e generates documentation and reports for the safety case 2 3 Functional requirements In the use case diagram from figure 2 1 we have captured the requirements of the system Using our tool the user should be able to 1 2 build and edit safety case diagram export any diagram as image jpg or png get a file conatining the translated the diagram into A box load or set the current Abox for querying query the diagram from a special console used only for this 20 CHAPTER 2 PROJECT OBECTIVES AND SPECIFICATIONS E ma a gt Generate reports Figure 2 1 System usecase 6 validate his safety case and get a file with the status of the validation 7 Generate documentation and reports 2 4 Non functional requirements Usability The user interface shall be very easy to use and intuitive Two goals should be strived for one click away functionality intuitive interface zero training Also the system should prevent the user before making errors and if the errors are made the the user will we notified about the errors
6. lucrare nu contine portiuni plagiate iar sursele bibliografice au fost folosite cu respectarea legislatiei romane si a conventiilor internationale privind drep turile de autor Declar de asemenea c aceast lucrare nu a mai fost prezentat n fata unei alte comisii de examen de licent In cazul constat rii ulterioare a unor declaratii false voi suporta sanctiunile admin istrative respectiv anularea examenului de licen Data Nume Prenume Semn tura 2 1 4 1 4 2 6 1 6 2 6 3 6 4 List of Tables Problem Statement and Solution 18 Syntax and semantics OF ALC ss e ze hogs SE a ste ai a oh LA 34 Retrieving information about the safety case 39 Retrieving some information about the safety case represented in figure 6 1 54 Retrieving some information about the safety case represented in figure 6 4 57 Retrieving some information about the safety case represented in figure 6 6 59 Tools Comparison Table ok a ay heey tas SOR deus oe berm oon Babess 62 2 1 3 1 3 2 3 3 4 1 4 2 4 3 4 4 4 5 4 6 4 7 4 8 4 9 5 1 5 2 5 3 5 4 5 9 5 6 5 7 5 8 6 1 6 2 6 3 6 4 6 5 6 6 6 7 List of Figures System us cas A og te Spoke Sb fe Re Le a 20 Acedit tool screenshot Leto ly ina ea ye sa RSE riot ea Bao eee z 22 AdvoCATE tool screenshot 23 D case editor tool screenshot cu soc ataca a ae a de 24
7. Elements of a safety case PAS A Se ee ri 29 Goal Structuring Notation elements n 30 Partial goals structure aid s mi TOS dos e e hee mg ld 30 Goal structure for the process based argument 31 Goal structure for the product based argument 32 Example of safety case represented using GSN 33 System Architecture pes s su eli hoa uC dee e ile 37 Flow Chart Querying the diagrama as ai ee WRG ee ASALA A 41 Flow Chart for validating the diagram 42 Systemi Arehteeture Segr a s E aa ro a 43 Component Diagram a ale ana 44 Component Dr a ds len dan Ata m dial A E 45 Class diagram for console plug in post Li Perde Yad dee ea 47 Class diagram for ontology actions plug in 48 Glass diagram tor parser plug in 2 4 4 a Sack a deg da 49 Class diagram for ontology plug in wie s l boo d So x Se Bowe u 50 Application Interface asia sala S Re EE ea 6465 52 Autonomous vehicle scenario sadico da els Ses Saha a AA 54 Translating the GSN diagram in a description logic Abox 55 Translating the GSN diagram in Abox using our tool 56 Therac 25 safety case x A as E s s s e s Aa 58 Translating the Therac 25 safety case in a description logic Abox 59 Airspace system safety case 60 Airspace system safety case translated in Abox using our tool 61 11
8. The corresponding strategy s used to support the goal g is to dynamically assess the risk The sub goals g 93 ga and gs are used to fulfill the strategy sj For instance the sub goal g claims the correctness of the model statement that is supported by various pieces of evidence including formal verification e The diagram from Fig 6 1 is translated into the description language in Figure 6 2 and the result of translation into Abox using Racer syntax by our tool is shown in figure Figure 6 3 Here the facts fg to f aa assert the individuals to their corresponding GSN core elements The structure of the GSN diagram based on the two relationships supportedBy and inContextOf is formalised by the facts fes to f72 The natural language text describing claims solutions contexts or evidences are encapsulated as concrete attributes 5 in Racer syntax assertions f73 to fso The table 6 1 contains the results of some basic queries run on the abox from 6 2 It can be seen that the obtained results are very helpful because it spares the safety engineer time which has to look for manually for them if such an assesment feature like querying the diagram is not available 53 54 c3 Situation avvareness SAW model EI Hazard analysis results analysis of kinematic model and accident sequence CHAPTER 6 TESTING AND VALIDATION G1 Autonomous Vehicle maintains safety when operating in the environment s1 Argument by a
9. goal goal7 goal has evidence Undeveloped Goals concept instances UndevelopedGoals nil Check if Abox is consistent aboz consistent t Get all contexts of a specific individual fillers strategyg inConteztOf nil goal 60 CHAPTER 6 TESTING AND VALIDATION Definition of safe q The Airspace is safe Basic ATM rules are implemented safely Basic ATM rules are sale Basic ATM rules implemented safely in each area Evidence that basic ATM rules implemented safely in each area cannot violate sate assumptons Outofarea events known do not violate safety assumpfons Whole airspace events known do not violate safety assumpfons Evidence that whole airspace events known do notviolate safe umpt Figure 6 6 Airspace system safety case In table 6 4 we presents the conclusion after building the safety cases presented above in our tool and two other tools More detailed comparison between our tool and other tool can be found in Bibilographic Research Chapter From the table we can resume that our tool is better at the management of a safety case having a plus at validation 6 1 TESTING THE TOOL 61 1 in abox safetyATM racer GSN 2 instance G1 Goal 3 attribute filler 61 The Airspace is safe claims 4 related 61 51 supportedBy 5 related 61 1 inContextof 6 instance S1 Strategy 7 attribute filler S1 Ba
10. Introduction Project Obectives and Specifica tions Bibliographic research Analysis and Theoretical Foundation Detailed Design and Implementation Testing and Validation User AZs manual Conclusions and Further Work Bibliography Appendices 3 Place of documentation Technical University of Cluj Napoca Computer Science Department 4 Consultants Lect dr eng Adrian Groza 5 Date of issue of the proposal November 1 2014 6 Date of delivery July 3 2014 Graduate Nicoleta Catalina Marc Supervisor Lect dr eng Adrian GROZA MINISTRY OF NATIONAL EDUCATION ur TECHNICAL UNIVERSITY OF CLUJ NAPOCA FACULTY OF AUTOMATION AND COMPUTER SCIENCE COMPUTER SCIENCE DEPARTMENT Declaratie pe proprie r spundere privind autenticitatea lucr rii de licent Subsemnata Marc Nicoleta Catalina legitimat cu seria AX nr 377045 CNP 2911205012661 autorul lucr rii Justifying software systems safety using arguments elaborat n vederea sustinerii examenului de finalizare a studiilor de licent la Facultatea de Automatic si Calculatoare Specializarea Calculatoare in limba Engleza din cadrul Universitatii Tehnice din Cluj Napoca sesiunea Iulie a anului universitar 2013 2014 declar pe proprie r spundere c aceast lucrare este rezultatul propriei activit ti intelectuale pe baza cercet rilor mele si pe baza informatiilor obtinute din surse care au fost citate n textul lucr rii si n bibliografie Declar c aceast
11. all checkboxes Click next Accept Sofware license Click finish 63 64 CHAPTER 7 USER S MANUAL 7 2 User s Manual T 8 Creating a project and add diagram to it steps select File gt New gt Projectselect General gt Project select next and give a name to your project select finish press right click in the created project select New gt Other in the pop up wizard type GSN select GSN1 diagram select Next gt Finish This action will add a new project to the workspace and the diagram in it 1 2 3 4 Transform diagram in A box after diagram file is created select diagram file press right click on files select Ontology next select Transform A box The output of this action will be a new file having the same name as the diagram and the extension racer located in the same project folder as the diagram The file is not loaded in the Racer engine de 2 3 4 Load diagram only if the racer file has been generated select diagram file press right click on files select Ontology next select Load A box This action adds the A box to the T box in the Racer and will set it as main A box 1 Validate diagram select diagram file 7 2 USER S MANUAL 65 2 press right click on files 3 select Ontology 4 next select Validate A box The action will write the results of the validation in validate log file this file will also contain the results of the prev
12. atomic concepts Table 4 1 Syntax and semantics of ALC Constructor Syntax Semantics negation aC AINGI conjunction cab CoD disjunction Cup Ctup existential restriction 3r C x e Ay x y rT Ay C value restriction Vr C z Af Vy x y er y C individual assertion a C a e CT role assertion a b r a b An ontology consists of terminologies or TBoxes and assertions or ABoxes Defini ie A terminology TBox is a finite set of terminological axioms of the forms C Do CCED Defini ie An assertional box A Boz is a finite set of concept assertions a C or role as sertions a b r where C designates a concept r a role and a and b are two individuals Usually the unique name assumption holds within the same A Box A concept C is satisfied if there exists an interpretation I such that C Z 0 The concept D subsumes the concept C represented by CE D if C D for all interpre tations I Constraints on concepts i e disjoint or on roles domain range of a role inverse roles transitive properties number constraints max min role inheritance parent role can be specified in more expressive description logics This paper provides only some basic terminologies of description logics to make it self contained For a detailed explanation about families of description logics the reader is referred to 4 44
13. console will look like this Tasks E Console 2 Command Console concept instances Goal G1 G2 G3 G4 G5 concept instances TopLevelGoal G1 retrieve individual fillers G2 has evidence E1 E3 E4 E2 retrieve individual fillers G1 has evidence nil abox consistent Figure 7 2 Command Console Chapter 8 Conclusions 8 1 Contributions and Achievements From this paper we can deduce that it is very necessary to be sure that a system has a correct behavior and can be operately successfully so it is very important to build a safety case that describes the real level of safety that the system assures Assurance cases have evolved from the concept of safety cases being a requirement in many international standards It is very important to build well structured and coherent safety cases because wrong construction and reasoning in safety arguments can undermine a systems safety claims and lead to failures of the system Like in case of Therac25 not building a simple assurance case that would have lead to discover several faults resulted in death of people All the elements of a safety case are part of the causal chain of hazard The safety case is based on claims any claim is broken into sub claims until is reached a point when the claims can be proved by the development or assessment of an artefact as evidence Every claim and strategy adopted to support the claim shoulf be very clearly formulated and state the conte
14. constructed by using a drag and drop pallet top right The built in actions performed on the diagram are visible when clicking right on the diagram or model file The command console bottom center shows the reasoning performed on the active 5 3 USER INTERFACE 51 diagram above In the command line specific queries for interrogating ontologies can be added and the reasoning engine will return the results for each query The syntax of the queries corresponds to the RacerPro tool In Fig 5 8 the four queries exemplified are e retrieving all the goals in the diagram e identifying the top level goal e listing all pieces of evidence supporting the goal g and e checking the consistency of a diagram with respect to the GSN standard encoded as axioms in description logic In the bottom left corner the red rectangle represent the view part of the diagram visible in the main window CHAPTER 5 DETAILED DESIGN AND IMPLEMENTATION 52 oerr uy uomeoddy g c 910314 weybeip Lus6 z3 nejap olseuars 122 pj m a qof peas ajosuo 1 ua sTsuod xoge TIU a2uapTAa sey 19 SJSTTTJ TENPIATPUT 2A3T4331 23 va 3 13 aduaptaa sey Z9 SJATTT4 TENPIATPUT 2A3T4331 19 saduejsut 3d33u0 gt S9 po 29 29 19 1809 s uEqsuT 3d uo2 o0suo2 puEululo2 mi el pl H m x 3 OSUO FR SASEL EZ anpowpenuoo ampowzuaunbiy JEIN
15. description logic handbook theory implementation and applications Cambridge university press 2003 V Haarslev K Hidde R M ller and M Wessel The racerpro knowledge represen tation and reasoning system Semantic Web vol 3 no 3 pp 267 277 2012 J K Richard Hawkins Tim Kelly and P Graydon A new approach to creating clear safety arguments 2011 T P Kelly Arguing safety a systematic approach to managing safety cases 1998 T P K Patrick J Graydon Using argumentation to evaluate software assurance standards Information and Software Technology vol 55 no 9 pp 1551 1562 2013 A Wardzi ski Safety argument strategies for autonomous vehicles R Palin D Ward I Habli and R Rivett Iso 26262 safety cases compliance and assurance 2011 J Birch R Rivett I Habli B Bradshaw J Botham D Higham P Jesty H Monkhouse and R Palin Safety cases and their role in iso 26262 functional safety assessment in SAFECOMP 2013 pp 154 165 E M B Melkild Goal and evidence based dependability assessment p 53 2013 M Conrad P Munier and F Rauch Qualifying software tools according to iso 26262 in MBEES 2010 pp 117 128 69 70 BIBLIOGRAPHY 14 R Dardar B Gallina A Johnsen K Lundqvist and M Nyberg Industrial experi ences of building a safety case in compliance with iso 26262 in Software Reliability Engineeri
16. our system we studied about descrip tion logics from the book 4 It presents description logic plus modelling and technical details the syntax of knowledge bases of the description logic SROZO presents the ALC description logic In paper 5 is presented the RacerPro system a knowledge representation system based that implements a highly optimized tableau calculus for a very expressive description logic Advantages of using this engine is that it offers reasoning services for multiple T boxes and for multiple A boxes as well and it provides us an API with Racer Client for Java For safety cases building and assesment we studied the following articles 6 and 7 In the paper 6 is presented a new way to structure assurance cases using assured safety arguments According to the authors any safety arguments has two components 25 e a safety argument that documents the arguments and the evidence used to establish direct claims of system safety e a confidence argument that justifies the sufficiency of confidence in this safety argu ment This decomposition gives greater clarity of purpose and helps avoiding the introduction of unnecessary arguments and evidence Many difficulties are encountered when having a single argument elements that documents both direct arguments of risk mitigation and supporting arguments for example e Because there is too much information in just one argument the arguments will become to large and and unw
17. terms A safety case should communicate a clear comprehensive and defensible argument that a system is acceptably safe to operate in a particular context Assurance cases are build using safety arguments each safety arguments should focus on identifying and reducing the hazards associated with the system The safety argument is based on claims any claim is broken into sub claims until is reached a point when the claims can be proved by the development or assessment of an artefact as evidence Every claim and strategy adopted to support the claim shoulf be very clearly formulated and state the context in which the argument is made so that the graphical representation of the safety case will be well structured The elements of any safety case are represented in figure 4 1 they are e Claim the statement or assertion e Evidence represents the provided evidence facts assumptions or subclaims to sup port the claim e Argument it is the linkage between the claim and the evidence e Inference the mechainsm providing the transformational rules for the argument The most important aspects of an safety case are e argument any safety case builds an argument based on the provided evidence ac cording to this argument someone can reasonably determine that the system is rela tively safe 28 4 1 SAFETY CASE 29 Inference rule Inference rule Argument Structure Figure 4 1 Elements of a safety case e clear any safet
18. with the RacerPro engine The class called OntologyConnection is build following Singleton pattern and is used to create a racer client and establish a connection to the racerPro reasoner using the JRacer java library provided by Racer For creating the connection we need to check if the engine is started for this we have the class RacerProcess which checks if there exist any process of the engine if not then locates the execution file of the racer and starts a new process If no file has been found then the user will be shown a message with the location from where he can download the engine This OntologyConnection class makes it possible interrogating the buid A box file mainly by receiving the text command from the console and calling answerQuery String 48 CHAPTER 5 DETAILED DESIGN AND IMPLEMENTATION Figure 5 5 Class diagram for ontology actions plug in command method which will return the result of the sent query Also this class has the method getTboxFile which instantiates an GSNTbox object and aks for creating the t box file modeled on GSN standard 5 2 IMPLEMENTATION DETAILS 49 Figure 5 6 Class diagram for parser plug in The GSNTbox class is a class that builds the T box part of the ontology It has static methods where all the concept roles and attributes are defined returning list of strings that are merge in the getContent method of the class A new file is generated with all this info and it will be save
19. 002 sis jeuy LL yney Jea s d 0 Tx gt EH pJezeH Ayiqeqoid aya duo gt pue 3981109 SI juswuolpodde 715 ir VH3 Woy p unu pi 5 2 gt ayes Ajqeydeooe si wajsAs 104002 LD Jes sad 9 0 TXT gt Bulun220 ZH 2 Ayyiqeqoudg pJezey p unu pi yes 4 AO jusunbiy is Ajjuaioyjns Jo u q saey sp ezeu Payizuapi Y UOHE LL A jewo INS pazeuiwija useq sey TH 2 vo p unu pi u q BABY SPIEZEY lv Z 7 3x 2uo2 pue ajo1 Bunes do D 34 CHAPTER 4 ANALYSIS AND THEORETICAL FOUNDATION 4 3 Description Language DLs are based on a vocabulary also called signature containing individual names concept names unary predicates and role names binary predicates In the description logic ALC concepts are built using the set of constructors formed by negation conjunction disjunction value restriction and existential restriction 4 as shown in table 4 1 Here C and D represent concept descriptions while r is a role name The semantics are defined based on an interpretation J A where the domain A of I contains a non empty set of individuals and the interpretation function maps each concept name C to a set of individuals C AT and each role r to a binary relation rl Al x Al The last column of table 4 1 shows the extension of for non
20. 26 instance C1 Context 27 attribute filler C1 Environment profile definition claims 28 instance C2 Context 29 attribute filler C2 Situation awareness 30 SAW model claims 31 instance Assumption 32 instance C3 Context 33 attribute filler C3 Situation awareness SAW model claims 34 instance El Evidence 35 attribute filler El Hazard analysis results analysis of kinematic model and accident sequence claims 36 instance E2 Evidence 37 attribute filler E2 Evidence based on simulation claims 38 instance E3 Evidence 39 attribute filler E3 Evidence based on the analysis of simulated and recorded real scenarios claims 40 instance E4 Evidence 41 attribute filler E4 Evidence based on operational system performance statistics claims 42 realize abox 43 set current abox default2 racer GSN Figure 6 3 Translating the GSN diagram in Abox using our tool The main statement is represented by top level goal Goal and states that the ma chine is fault free and can be used Two strategies have been adopted for proving this goal the first strategy represented by Strategy proposes argumentation by satisfaction of sys tem s safety while the second strategy represented by Strategy proposes argumentation by omission of all identified software hazards supposing we have identified the software hazards context represented by node Context The first strategy is divided into two sub claims the syst
21. By ae ae ae ae ae Figure 6 5 Translating the Therac 25 safety case in a description logic Abox The third safety case is for a whole airspace system divided into several georgraph ical regions plus a region of en route airspace for which ATM rules are applied and imple mented on an are by area basis Georgraphical regions that interacts with each other and also with the airspace wide system The safety case structure for the system is represented in figure 6 6 The main goal represented as Goall states that the airspace is safe for using in the context of defining the safe term in case of the system The strategy adopted by proving the goal is to prove that ATM rules are safe respectively that the rules have been implemented safely The second strategy is also divided in two it is state that the rules are implemented safely in every area and each area assumption can t be violated Evidence for each sub goal is provided as is shown in the diagram Figure 6 6 represents the translated Abox into Racer syntax it can be seen that the goal structure is keep in the A box Table 6 3 Retrieving some information about the safety case represented in figure 6 6 Query RacerPro query RacerPro answer Top level goal concept instances TopLevelGoal gl Support goals concept instances SupportGoal 92 93 94 95 96 gT Evidence supporting retrieve individual fillers e3
22. C AON S al sana ds I acuzare N War dt da Cs ia e I cia cia SA S Esa A ia e SU xl dedi dA gt Gee GG GP GP Z PPP PP PP PP PP S S S ee S M Seat E s x x azar ES a E Dit e Za x Figure 6 2 Translating the GSN diagram in a description logic Abox 56 CHAPTER 6 TESTING AND VALIDATION 1 in abox default2 racer GSN 2 instance G1 Goal 3 attribute filler G1 Autonomous Vehicle maintains safety when operating in the environment claims 4 related 61 51 supportedBy 5 related G1 C1 inContextOf 6 related G1 C2 inContextof 7 instance G2 Goal 8 attribute filler G2 SAW model is correct sufficient and assures vehicle safety claims 9 related 62 E2 has evidence 10 related G2 E4 has evidence 11 related G2 E3 has evidence 12 related G2 E1 has evidence 13 related G2 C3 inContextof 14 instance G3 Goal 15 attribute filler G3 Vehicle maintains situation awareness claims 16 instance G4 Goal 17 attribute filler G4 Vehicle performs optimal safe actions according to the vehicle policy claims 18 instance G5 Goal 19 attribute filler G5 Environment profile assumptions are not violated claims 20 instance S1 Strategy 21 attribute filler S1 Argument by application of dynamic risk assessment claims 22 related S1 62 supportedBy 23 related 51 63 supportedBy 24 related S1 G4 suppor tedBy 25 related S1 G5 supportedBy
23. Extensibility Take into consideration further work extending and adding product features Documentation An Administration Guide and a User Guide should be developed in pdf format 2 4 NON FUNCTIONAL REQUIREMENTS 21 Operating constraints Reasoning engine RacerPro are needed in querying the safety case plus java jRacer library for creating a java racer client connection to the engine NaturalOwl engine is used to generate documentation of de description logic in natural language Reusability Ontology code should be in a separate plug in so that it can be reused Do the same for the command console code Chapter 3 Bibliographic research In order to build the tool we have studied several tools used for building safety cases among them ACedit 1 and AdvoCATE 2 Both tools are used to create safety cases and use the GSN for structuring the safety arguments ACedit 1 is an open source editor used to create Assurance Cases based on the Goal Structuring Notation standard and the OMG Argumentation Metamodel The tool can be used only for creating and editing a safety case it lacks at the assessment of the safety case Out tool is an improvement of this tool being added new features like the option of querying the diagram using ontologies better validation creation of reports and documentation usage of safety metrics for the assessment of the safety cases Figure 3 1 represents a screenshot of this tool Figure 3 1 Acedit t
24. Fig 4 4 The goal claims that the process adopted to develop the product is correct and successfully completed Goal2 is di vided taking in account the roles Strategy1 and activity steps Strategy2 in 3 sub goals 30 CHAPTER 4 ANALYSIS AND THEORETICAL FOUNDATION Goal Name Claim goal Solution Name Evidence supporting a claim Strategy Name Strategy used for decomposing argument into additional claims Context Name Context of a claim Justification Name Assumption Name Statement assumed but not demonstrated to be true Explanation why a solution satisfies a goal Figure 4 2 Goal Structuring Notation elements Goal1 hazards have been identified and analyzed Goal2 Goal6 the required process the product behaviour activity has been carried has been analyzed out Figure 4 3 Partial goals structure Goal3 Goal4 and Goal5 Goal claims that the hazards regarding the adapted process of building the product have been identified and classified using the Hazard identifica tion and analysis using HAZOP technique HAZard and Operability analysis to provide the evidence representing Evidence node while Goald claims that all the hazard have been carefully analyzed backward and forward providing as solution hazard identification and analysis using HAZOP technique HAZard and Operability analysis represented as Evidence3 and Failure Modes and Effects Analysis FMEA procedure and Fau
25. MINISTRY OF NATIONAL EDUCATION ur TECHNICAL UNIVERSITY OF CLUJ NAPOCA FACULTY OF AUTOMATION AND COMPUTER SCIENCE COMPUTER SCIENCE DEPARTMENT JUSTIFYING SOFTWARE SYSTEMS SAFETY USING ARGUMENTS LICENSE THESIS Graduate Nicoleta Catalina MARC Supervisor Lect dr eng Adrian GROZA 2014 MINISTRY OF NATIONAL EDUCATION up TECHNICAL UNIVERSITY OF CLUJ NAPOCA FACULTY OF AUTOMATION AND COMPUTER SCIENCE COMPUTER SCIENCE DEPARTMENT DEAN HEAD OF DEPARTMENT Prof dr eng Liviu MICLEA Prof dr eng Rodica POTOLEA Graduate Nicoleta Catalina MARC JUSTIFYING SOFTWARE SYSTEMS SAFETY USING ARGUMENTS 1 Project proposal In safety critical applications it is necessary to justify the soft ware conformance with specifications and standards Certification bodies require the construction of assurance cases that contain claims supported by evidence obtained during development and testing of the system It is important to build well structured and coherent safety cases because wrong construction and reasoning in safety argu ments can undermine system s safety claims and lead to failures We developed a tool that facilitate the construction and assessment of safety cases The tool sup ports the Goal Structuring Notation standard for creation of safety arguments The GSN diagrams are translated in description logic in order to formally check various properties of the safety case 2 Project contents Presentation page
26. MODELING THE GSN STANDARD IN DESCRIPTION LOGIC 35 4 4 Modeling the GSN Standard in Description Logic The relationship supportedBy allows inferential or evidential relationships to be documented The allowed connections for the supportedBy relationship are goal to goal goal to strategy goal to solution strategy to goal Axiom A specifies the range for the role supportedBy Ai T E VsupportedBy Goal U Strategy U Solution Axiom A specifies the domain of the role supportedBy axiom Az introduces the inverse role supports and Ay constraints the role supportedBy to be transitive AsupportedBy T E Goal U Strategy supportedBy supports supportedBy supportedBy define primitive role supportedBy domain or Goal Strategy range or Goal Strategy Solution inverse supports transitive t define primitive role inContextOf domain or Goal Strategy range or Context Justification Assumption Inferential relationships declare that there is an inference between goals in the ar gument Evidential relationships specify the link between a goal and the evidence used to support it Axioms A and Ag specify the range of the roles hasInference respectively hasEvidence while Ag and Ag the domain of the same roles Definitions 4 and Ajo say that the supportedBy is the parent role of both hasInference and hasEvidence thus inheriting its constraints As L VhasInference Goal Ag T VhasEuide
27. Pow NSD JOIAS IST 2 gt x m A Agpanjos c SAIYSUONE 3J NSD Z Te o 1 3402 uondunssv h 3102 NSD 2 Mv 4 22 uma q m led s o mi x wesbeip Lusb z neJap P Enq q sk E b a Si A fo a Rz a e O sn x umno 52 J33eJ 23neJ9p El wesbeip Lusb z3nejap i 5 22 Bj OPUS IDA A O a a sm a a JaJo dxa pafosd 9 3 2puy a 11 Chapter 6 Testing and Validation 6 1 Testing the tool To test if the application has the desired behaviour and it is well build we have taken well structured or incomplete safety cases from different domains builded and validated within our tool More details about each safety case can be found in the Bibliographic research chapter The first safety scenario is taken from from the autonomous driving domain and represents in the case is claimed that any autonomous vehicle should ensure safety when operating in the environment A GSN diagram built in our SafeEd tool is represented in Fig 6 1 The top level goal g states that any autonomous vehicle should ensure safety when operating in the environment The goal holds in two contexts the existence of an environ ment formalisation context respectively the existence of a mechanism providing situ ation awareness One solution for ensuring safety is dynamic risk assessment approach 9
28. actions plug in adds in the diagram s file menu all the actions that can be done with the file transforming into A box validate it load it in the racer engine generate to do report and documentation It is composed of two packages one is containing the popup actions and the second one contains their core functionality of the popup actions from the menu The actions have a corresponding class from the gsn actions package and action in the extension point extending the org eclipse ui popupMenus class from the plugin xml file in order to be visible in the view Their core functionality has been separated from the interface all classes being implemented in the package gsn actions core All the 3 types of actions for creating reports use the same class DocumentationActionCore which has a separated method for each one of them because they don t have the same template All the others actions are linked to a class implementing the action functionality In figure 5 6 are represented all the classes and the relations between them from this plug in The GSN parser plug in is the eclipse plug in used to translate the builded safety case diagram into the A box part We have a class called XMLparser that has methods for parsing each node from the diagram model file which is a xml file transforms it into a concept instance or relation between two instances or adds an attribute and at the end saves all data into a file representing the an A box Because each n
29. and providing evidence According to GSN standard the main elements of an safety argument are goal strategy solution context assumption justification The Goal represents the statement that needs to be proved it can be divided in sub goals until its reached the level where the 32 CHAPTER 4 ANALYSIS AND THEORETICAL FOUNDATION Goal the product behaviour has been analyzed Goal7 Goals H identified amp Effects and causes of classified hazardous events Evidence2 Evidence3 Evidence Adapted HAZOP FMEA FTA Figure 4 5 Goal structure for the product based argument sub goal can be supported by evidence Strategy element is used to describe the method aproached by the system to prove the claim A Solution node provides the evidence or references to the evidence supporting the goal Context element provides information relevant for the corresponding goal while the assumption element will provide statements that are already true Justification elements is used to explain why the provided evidence is enough to prove the goal These elements can be related to each other using two relations inContextOf only between goal and context and solvedBy Figure 4 2 contains elements of the GSN standard represented as follows goals with rectangular strategies with paralelograms evidence and solutions are represented by circle assumptions and justifications with ellipse context by a rectangular with rounded corners The supportedBy relation
30. basic queries run on the abox from 6 5 It can be seen that the obtained results are very helpful because it spares the safety engineer time which has to look for manually for them if such an assesment feature like querying the diagram is not available Table 6 2 Retrieving some information about the safety case represented in figure 6 4 Query RacerPro query RacerPro answer Top level goal concept instances TopLevelGoal goal Support goals concept instances SupportGoal goal goals goala goals goals goals Evidence supporting retrieve individual fillers solutions goal goal goal has evidence solutiona Undeveloped Goals concept instances UndevelopedGoals nil Check if Abox is consistent aboz consistent t Get all contexts of a specific individual fillers strategyg inConteztOf context goal TESTING AND VALIDATION CHAPTER 6 58 synsau 1s 1 2 y uonnlos aJnjiej jusuoduos jo ynsaJ e se 22 fjuo ues sapow Buoum Bun y s Jaynduos 1202 spuezey aJemyos payijuapi Laxaquo SR Ajoyes GZ WIL p 9 AMITA sis jeue 381 nea uonn os Jusuodwos jo ynsa e se 1n220 Ajuo ues AbJaua BuoJm 9 600 spuezey SJEMYOS p unu p IIE jo uoissiuo Aq quawnbiy 7 K623ens 33 4 ne 5142 deJayl Veoo 5 ayes Z uonnlos abessa
31. ck release are used has Text fs fs gu UncertaintyGoal fe gu The item has a reliability of 95 hasText Intermediate explanatory steps between goals and the evidence include statements references justifications and assumptions 420 Explanation E Statement O Reference Justification U Assumption where these top level concepts are disjoint A21 Statement Reference A22 Statement Justification A23 Statement Assumption A24 Reference aJustification A25 Reference 7Assumption A25 Justification Assumption The evidences or solutions form the foundation of the argument and will typically include specific analysis or test results that provide evidence of an attribute of the system In our approach the evidence consists in model checking the verification for a specification of the system A not verified goal is a goal which has at least one piece of evidence that is not formally proved A27 NotVerifiedGoal Goal NdhasEvidence Not VerifiedEvidence 4 5 FUNCTIONALITY 37 Ags NotVerifted Evidence Evidence M Shas TestResult False M Unknown 4 5 Functionality 4 5 1 Diagram translation and Reasoning in safety arguments The main idea of translating the builded safety case diagram into A box is presented in figure 4 7 GSN plug ins GSN editor GSN model Ontology plug in Validator Quey Figure 4 7 System Architecture ABOX
32. cular reasoning identified by the RacerPro engine in the form of cycle concepts Validating the Diagram Scenario The flow of this action is represented in figure 4 9 Below is presented the steps necessary without interruptions for validating using Racer the selected diagram Happy flow 1 User opens or creates a diagram 2 User select from ProjectExplorer tab the selected diagram 3 Selects validation of the wanted diagram 4 Systems returns the results in validation log file In the extended flow are presented the interruptions that might occur when trying to complete this action Extended flow 3 1 File containing diagram translation is not found 3 1 1 System notifies the user that racer file was not found 3 1 2 The user selects translating the diagram 3 1 3 User ree selects validation 3 2 Racer engine is not started 3 2 1 System notifies the user that RacerPro was not found 40 CHAPTER 4 ANALYSIS AND THEORETICAL FOUNDATION 3 2 2 The user starts manually the engine 3 2 Diagram is not loaded 3 2 1 System notifies the user that diagram is not loaded 3 2 2 The user loads the diagram in racer engine 4 5 3 Generation of Safety Case Metrics Complementarily to supporting semantic reasoning our system provides also quan titative assessment of a safety case through several metrics developed The metrics are developed with the LISP API of RacerPro system For instance the number of not verified goals for safety ca
33. cure through the sufficient solutions and evidence are provided for each stated claim in the safety case The found solution is using ontology reasoning serivices because the ontology provides a source of well defined terms that can be used in descriptions of safety case nodes The safety case knowledge can be represented as a ontology and after queries can be run on that ontology Table 2 1 Problem Statement and Solution The problem of building incomplete safety cases because of bad safety case assessment affects system s safety and the safety engineer the impact of which is incomplete description of systems assurance a successful solution would be improve the assement of the tool using reasoning services 2 2 Goals and Objectives 2 2 1 Bussiness Goals and Objectives Nowadays many international standards require for systems that present a certain level of risk to justify prior to deployment why software behavior is to be trusted Because 18 2 3 FUNCTIONAL REQUIREMENTS 19 of this the bussiness goals and objectives for this project will focus on implementing a tool that e improves assement of safety cases e reduces the risks of not building well structured and complete assurance cases e is easy to use e eases the work of the safety engineer e enables the evaluation of the realism of the cases 2 2 2 Project Goals and Objectives The project main goal is to develop a system that
34. d at running in the eclipse main folder In figure 5 7 are represented all the classes and the relations between them from this plug in This plug in is used in all the other plug ins excepting the parser plug in The GSN reporting plug in contains three types of reports validation ToDo and documentation reports generated in natural language All three reports are pdf type and are generated using iText library This library is used to creare adapt inspect and maintain pdf files The data from the reports is taken using Lisp Racer Cilent library provided by Racer is used for generating metrics in the reports and by directly interogating the A box with fixed queries depending on each report type Each report has a different template The validation report contains the same output of the validation action the differ ence is that it is saved in a new file and not in a log file The To do report contains what has been done what still needs to be done and what is missing from the safety case diagram 50 CHAPTER 5 DETAILED DESIGN AND IMPLEMENTATION racer RacerClient instance OntologyConnection Boolean false ing home catalina licenta gsn racer lt lt create gt gt OntologyConnection setFilePath filePath String getInstance OntologyConnection openConnection addAbox aboxpath String filename String answerQuery query Sting String 2 7 setCurrentAbox abox String String A getProvedGoal
35. dd new functionality Being build as a set of eclipse plug ins that need the eclipse platform to run on the bigest improvement would be to get rid of this and run the tool as a standalone application by creating a Rich Client Platform RCP application for the tool We choose this because it will improve the protability of the tool RCP can run as standalone applications by including a minimal set of eclipse plugin Other future improve ments e reverse the process of translation from an A box build accordingly to the T box the user should be able to transform it into diagram This will ease a lot more the work of the safety engineer e import and export diagrams from other editors e improve the user interface the metamodels should be colored distinctly from the start e the generated reports should provide more information e add the possibility to extend the metamodels u Bibliography G Despotou A Apostolakis and D Kolovos Assuring dependable and critical systems Implementing the standards for assurance cases with acedit Department of computer Science University of York UK 2012 E Denney G Pai and J Pohl Advocate An assurance case automation toolset in Computer Safety Reliability and Security Springer 2012 pp 8 21 S Hallerstede M Jastram and L Ladenberger A method and tool for tracing requirements into specifications Science of Computer Programming 2013 F Baader The
36. em will halt in case of errors statement represented by Goals and that exceeding radions limit will abort the operation statement represented by Goals Goal is supported by Goal which claims that when a fault occurs the system cannot be resumed a solution to this would be Black Box testing Solution Both Goal and Goals are supported by the Goals which claims that any failure operation will include explana tory error message a solution for this is declaring and using safe states Solutions The 6 1 TESTING THE TOOL 57 second adopted strategy is solved by two statements computer giving a wrong amount of energy occurs as a result of component failure Goals and computer selecting wrong mode can only occur as a result of component failure Goal Both goals are solved by making fault tree analysis Solutions and analysing the results of hazard test Solutions This case could have been applied when developing the Therac 25 system leading to discovering of several faults that could have saved lives The diagram in Fig 6 5 is translated into the Abox represented in Fig 6 2 Here the facts assert the individuals to their corresponding GSN core elements The structure of the GSN diagram based on the relationships has evidence supportedBy and inContertOf The natural language text describing claims solutions contexts or evidences are encapsu lated as concrete attributes 5 in Racer syntax The table 6 2 contains the results of some
37. ementing the console and gsnl racercommands is the one which deals with the processing and execution of the commands We create a new type console called Commands Console implemented in class CommandConsole This class extends the IOConsole class provided in org eclipse ui console package The console will display text from the I O streams It can have multiple output streams connected to it and only one input stream connected to the keyboard In the plugin xml file we declare a new extension point that contributes to the org eclipse ui console consoleFactories factory extending that plug in with the console fac tory class called Factory The console factory extension is responsible for openining a console in the console view Extensions appear on a menu in the console view and are opened when their openConsole method is called The gsn console package that contains the console was developed so that it can be re used by developers for building I O consoles having other purposes For processing the commands and queries from the console we applied the Factory pattern There is the factory class called CommandFactory and the interface Command implemented by each command The StartCommand class deals with starting a new RacerPro process if at that moment there s no process of the engine The QueryCommand class is used to send a query to the racer engine and process the results The class diagram of this plug in can be seen in figure 5 4 The GSN
38. hanges introduced by the new machine they didn t go throug all phases of the project development residual software errors have been omitted from the analysis many hardware safety stops were removed because they thought that the software was better Another bad practice commited by them not performing risk assessment for the software reuse of older machine s software without checking for faults and making the system hard to use by the others the error messages were very difficult to understand because they didn t specified the exact cause they were like MALFUNCTION 47 OR VILT and therefore the errors were ignored by the practitioners The case presented by the author is just a start because it doesn t 27 contain very detailed the system requirements hazard identification and a risk analysis haven t been performed but a top level safety case can be build The most important requirements established by the author are more detailed error messages the maximum limit for MeV electron treastments should be set occurence of errors should stop the ma chine the computer should select the correct energy and modes Chapter 4 Analysis and Theoretical Foundation 4 1 Safety Case Safety cases are used in risk safety domain in case of systems that presents a certain level of risks in order to prove that the system requirements are complete and satisfied by evidence In this thesis the safety case is defined in the following
39. ict shall information rement The aut maintain accurate state E Properties et Base Properties Identifier N48087573 Description Avionics software satisties safety requirements applicable during descent Attributes Comment Color Blue 14 O ToBelnstantiated O ToBeDeveloped s Bao Figure 3 2 AdvoCATE tool screenshot The novelty of our approach is that the assurance case is automatically translated in description logic The advantage is that the specific reasoning services of description logic are enacted to verify the compliance of the case with the GSN standard and also to signal possible argumentation flaws The difference between our tool and this one is the fact that using ours the user will be able to build simple or complex queries for interrogating the diagram at any time during the development and not being limited only to metrics this is a plus at the assessment of the diagram D case Editor is another tool for constructing safety cases developed by DEOS Dependeble Embedded Operating System for Practical Uses Similar to our tool it is an Eclipse plugin based on the Eclipse GMF framework and supports GSN standard It is a prototype of a dependability case editor and has a 24 CHAPTER 3 BIBLIOGRAPHIC RESEARCH GSN pattern library function and ptototype checking function Figure 3 3 represents a scrrenshot of this tool
40. ieldy leading to difficulty in reviewing them because of the size and lack of focus e It is more difficult to see the incompleteness or poor structure in the safety argument e Arguments tend to be indirect and unfocused and the link between elements of the argument and risk is often lost e Arguments become difficult to build and weaknesses of the argument are sometimes not evident and so are easily overlooked These difficulties are serious since they all detract from the basic purposes of us ing safety cases Linking the two arguments provides a mechanism for guiding analysis of the interrelationship between safety and confidence Both papers 6 and 7 claim that any safety argument should focus on identification management and mitigation of hazards associated with the system All the elements of a safety case are part of the causal chain of hazard The safety case is based on claims any claim is broken into sub claims until is reached a point when the claims can be proved by the development or assessment of an artefact as evidence Every claim and strategy adopted tu support the claim shoulf be very clearly formulated and state the context in which the argument is made The solution proposed by the authors for this is to represent graphically the safety argument because it is clearer than through narrative text because in a narrative text is more difficult for the reader to identify the individual elements and structure of the argument I
41. igure 5 3 Component Diagram 5 2 Implementation details 5 2 1 GSN plug ins In this set of plug ins is implemented GSN editor functionality and interface using specific eclipse frameworks designed for this Eclipse Modeling Framework EMF is a Java framework and code generation facility provided by Eclipse for building tools based on a domain model The framework provides the EMFatic language with which the domain models can be turned into efficient correct and easily customizable code EMFatic language is similar to Java syntax and is designed to support navigation and editing of Ecore models In our case the GSN metamodels are defined using the EMFatic language Graphical Editing Framework GEF is a framework provided by Eclipse for creating graphical editors for various diagrams It is used to represent graphically a safety case and also it permits the addition and manipulation of a safety case providing a visual representation of the relationships between the safety case model elements Graphical Modelling Framework GEF is an Eclipse framework used for de veloping graphical editors based on EMF and GEF This has been used to develop the runtime infrastructure of our tool 46 CHAPTER 5 DETAILED DESIGN AND IMPLEMENTATION 5 2 2 GSN ontology plug ins The GSN console plug in contains the implementation of the console used to run queries on the diagram called Command Console It consist of two packages gsn1 console is the package impl
42. ious validations of this or other files An example of this report is shown in figure 7 1 2 3 4 ALL the nodes have claims Evidence or solution must be provided for the following goals G3 G4 G5 G3 goal parents Gi G4 goal parents G1 G5 goal parents G1 G1 goal has undeveloped childs ALL goals are linked to the top level goal Figure 7 1 Autonomous vehicle scenario Generate Validation report select diagram file press right click on files select Reports next select Validation report The action is similar to validation action the difference is that the report contains info only about this file The generation of documentation and todo reports is the same as this The gener ated file are of pdf type 1 2 Generate ToDo report select diagram file press right click on files 3 select Reports 66 CHAPTER 7 USER S MANUAL 4 next select ToDo report Generate Documentation 1 select diagram file 2 press right click on files 3 select Reports 4 next select Documentation The user can query a diagram by following the next steps 1 if the command console is not visible then add it in the view e select window gt perspective gt other e select console from the view 2 Write start and press enter to activate the console 3 select Ontology gt Load Abox to be sure that the diagram si loaded or write set current abor diagramName 4 write the query and press enter The
43. is rendered as an arrow with the solid and allows inferen tiol or evidential relationships to be documented It is used to establish the following con nections goal to goal goal to strategy goal to solution strategy to goal goal to solution goal to justification The inContextOf relation is represented by an arrow with empty head and is used to declare a contextual relationship This relation permits connection between goal or strategies with context justification or assumption elements In figure 4 6 we have an example of goal structure composed with GSN elements It can be seen that we have a main goal the top level goal which is solved by other goals the support goals and strategies Each goal in turn can happen in different contexts or different assumptions about the goal can be made and the goal could be divided in ther sub goals strategies or could be supported by evidence 33 GOAL STRUCTURING NOTIFICATION 4 2 NS Sursn poquosoIdoI aseo 6 Jo o durexy 9 p 910314 2115 404 u piA 55920 4 NS 2115 0 1u uido A q wajs s uoh old Mepuooas SpJezey siemyos p unu pi 92 s ss old pue auljapino 115 52 PIS 104 souspina 55920 4 ENS Pus padojanag ul s4s Uu011 2 101d MEW 19 sjusws a uepuodas pue Meus 40 11S Pp e olle Jano jua unbiy 25 spJezey ayeidoidde 115 u q sey lajs s 1044002 ayy ul aJempos uoluyeq wayshs 04
44. l s n Kio eueldex pnioul IM uoiesado aunje4 5 609 uolesedo BY ode pes 002 buissed 3uaw ea U01 93 8 ASW 1205 Ky es sz delay Il JO uoipeysies Aq yuaunbiy V A5 ens 1591 xiq 9818 V uonn os pawnsal aq jouue wuajzs s ay San220 Ynez e USUM r 1205 yey 0 l s4s asne gt 40143 JUBW ESIL z 1600 6 1 TESTING THE TOOL 59 in aboz default racer GSN instance Goal Goal related Goal Strategy supportedBy related Goal Strategyg supportedBy instance Strategy Strategy related Strategy Goalg supportedBy related Strategy Goal supportedBy instance Strategus Strategy instance Goalg Goal related Strategy Goalg supportedBy related Goalg Solutions has evidence related Goalg Solution has evidence instance Goal Goal related Goal Solution has evidence instance Goaly Goal related Goaly Solutions has evidence related Goal Solution has evidence instance Goals Goal related Goals Solutiong has evidence instance Solution Evidence instance Solutiong Evidence instance Solutions Evidence instance Solution Evidence related Strategy Goal supportedBy related Strategy Context inContextOf instance Context Context instance Goalg Goal related Goals Goal supportedBy related Goalg Goals supportedBy instance Goals Goal related Goals Goals supported
45. lt Tree Analysis technique as Evidence4 The product based goal Goal6 is justified in Fig 4 5 This claims that the system has the required safe behavior if something fails then the system should be able to fail in a safe way The goal is divided in two goals Goal7 and Goal8 Goal7 claims that all the hazards regarding the product have been found while Goal8 states that the the effects and causes of hazardous events have been analyzed The goals have as solution techniques 4 2 GOAL STRUCTURING NOTIFICATION 31 Goalz Context1 the required process activity has been carried ISO 26262 out Concept Phase Strategy1 Strategy2 Argument over Argument over roles Aztivity s steps Goal4 Context2 Goals Goal3 identification E Forward backward 57 amp classification H analysis qualified Evidence2 Evidence3 Evidences Evidence1 Adapted FMEA FTA Training amp HAZOP Education Figure 4 4 Goal structure for the process based argument the same nodes Evidence2 Evidence Evidences 4 2 Goal Structuring Notification Our tool uses Goal STRucturing Notation to represent assurance cases structure mainly because inn last years GSN has been more and more used in risk based safety domain GSN presents a new argumentation notation for structuring and representing graphically safety arguments 4 2 1 Elements of GSN Having a well defined structured GSN standard increases the chance of identifying gaps in proving the goal
46. n paper 8 the authors propose a method for assessing software safety and security standards by capturing and criticising their arguments This method assumes following three steps argument capture argument criticism and issue sentencing In the first step argument capture the standard requirements are ideentified through analysis and also the specific claims assumed by those requirements and the evidence supporting the claims The standard s text should be used in the captured argument as much as practical Throughout this process the standard should be captured as accurately as possible The second step called argument criticism focuses on reviewing the fragments of argument by following the next phases 1 Take into consideration misinterpretations of the argument 26 CHAPTER 3 BIBLIOGRAPHIC RESEARCH 2 Try to draw out implicit or explicit assumptions 3 Judge the necessity of each assumption 4 Search for errors the argument 5 Identifies where independent lines of reasoning depend upon common sub arguments 6 Take into account strengthening the argument 7 Determines whether negative experience with similar systems might provide coun terevidence 8 Judges the strength of the argument In the last step issue sentencing the analyst shoul re examines each identified issue to de termine what hazards from the standard are reflected More about safety argument strategis have been studied from paper 9 In his papers he inves
47. nce Evidence As 3haslnference E Goal 3hasEvidence T E Goal A7 hasInference supportedBy Ajo hasEvidence supportedBu define primitive role has inference parent supportedBy domain Goal range Goal define primitive role has evidence parent supportedBy domain Goal range or Evidence solution Goals and sub goals are propositions that we wish to be true that can be quantified as quantified or qualitative provable or uncertainty A QuantitativeGoal E Goal A13 ProvableGoal E Goal A12 QualitativeGoal E Goal A14 UncertaintyGoal E Goal 36 CHAPTER 4 ANALYSIS AND THEORETICAL FOUNDATION A sub goal supports other high level goals Each safety case has a top level Goal which does not support other goals Ais SupportGoal Goal N Asupports T Ai TopLevelGoal GoalN SupportGoal equivalent SupportGoal and Goal some supports top equivalent TopLevelGoal and Goal not SupportGoal For each safety argument the elements is instantiated and a textual description is attached to that individual by enacting the attribute has Text with domain Statement and range String A17 al Aig 3hasText Statement Vhas Text String Three individuals gt gp and gu of type goal and their textual descriptions are instantiated by assertions f to fe fi gt TopLevelGoal fa gt The system meets its requirements hasText f3 gp ProvableGoal fa gp Qui
48. nce cases are the answer to our question Assurance cases have evolved from the concept of safety cases and they contain claims supported by the evidence obtained during development and testing of the system It is very important to build well structured and coherent safety cases because wrong construction and reasoning in safety arguments can undermine a systems safety claims and lead to failures of the system Over the last years many documents have appeared about how to describe and graphically structure an assurance case One of these documents is the Goal Structuring Notation also known as GSN The Goal Structuring Notation is an argumentation notation used to structure and graphically represent a safety argument Even though we have a solid standard for representing safety cases it doesn t reduce the risk of building incomplete and bad structured assurance cases because of bad assessment of tha safety case i e the number of claims could be very high and therefore will be hard to follow by the safety engineer A solution to this problem is to develop a tool that facilitates the construction and assessment of safety cases The main feature of the tool is to translate the GSN graphical notation into description logic in order check the GSN model for consistency Hence the GSN model for a safety critical application can be specified both in graphical notation and in description logic The advantage is that the specific reasoning services of descripti
49. ng Workshops ISSREW 2012 IEEE 23rd International Symposium on IEEE 2012 pp 349 354 Appendix A Published papers 1 Nicoleta Marc Adrian Groza A formal model of Goal Structuring Notation Computer Science Student Conference Cluj Napoca 2014 Won first prize at the Confer ence 2 Adrian Groza Nicoleta Marc Consistency Checking of Safety Arguments in the Goal Structuring Notation Standard 2014 Paper submitted at ICCP2014 71
50. nnections with RacerPro engine and NaturalOwl engine e third layer contains the GSN and ARM metamodels plus tool plug ins through which all tool functionality is provided e last layer represents the user interface layer and consists of the GSN editor and the model management tools GSN editing wizards From figure 5 2 can be seen that we kept the main component of the ACedit consisting of the GSN plug ins regarding the graphical editor eliminated the validation plug in and we added a new set of plug ins which provides the semantic reasoning facility validation and the others features GSN Ontology plug ins Figure 5 2 Component Diagram 5 1 1 GSN editor The GSN editor has two views e the diagram view deals with creation of GSN diagram accordingly to the mapping between metamodels and their graphical notation e the model view deals with creation of GSN metamodels 5 2 IMPLEMENTATION DETAILS 45 For communication between this two views it has been used the Model View Controller pattern as follows the model part of the MVC is represented by the model view and is the GSN model instance created by the user the view part is represented by the diagram view i e the editor s GUI and the controller represents the logic implemented in the others plug ins This communication is alsoo represented in figure 5 3 Model view 1 maca notifies manipulstes I I I I m m User F
51. oal g Goal gs Goal g Goal gs Goal c Context ca Context cz Context ei Evidence Evidence ez Evidence Evidence s Context Context ca Context 91 81 supportedBy inContextO f inContextO f inContextO f g2 1 has evidence O AN O Ot A OU N has evidence has evidence has evidence N gi Autonomous Vehicle maintains safety when operating in the environment has Text 92 SAW model is correct sufficient and assures vehicle safety hasText 93 Vehicle maintains situationawareness hasText an 94 Vehicle performs optimal safe actions according to the vehicle policy hasText gs Environment profile assumptions are not violated hasText 81 Argument by application of dynamic risk assessment has Text ei Hazard analysis results analysis ofkinematic model and accident sequence has Text eo Evidence based on simulation hasText es Evidence based on the analysis of simulated and recorded real scenarios hasText Evidence based on operational system performance statistics has Text Environment profile definition hasText c Situation awareness SAW model has Text Situation awareness SAW model has Text G N gt O O
52. ode of the diagram is 5 2 IMPLEMENTATION DETAILS 47 z console CommandConsole outputStream IOConsoleOutputStream null m consoleVievv IConsoleView null inputStream IOConsoleInputStream null ENTER KEY String yy eadKeyBoardJob Job openConsole lt lt create gt gt CommandConsole name String q etConsole CommandConsole printMessage message String displayConsoleView readConsole writeToConsole console IOConsole msg String CommandFactory execute command String String lt lt create gt gt Activator start context BundleContext stop context BundleContext lt lt create gt gt QueryCommand execute comm String String Figure 5 4 Class diagram for console plug in represented through generated ids at not by the node identifier from diagram when we parse the diagram_model file create Shape objects and save only the nodes that are shape or shape attribute if we find connectors that depending on the ids representing the targets we search for those shapes and add the connection at the parent shape This class uses org w3c dom and javax xml parsers libraries for parsing the XML file The Ontology class is contains methods that build the syntax to be added in the Abox file depending on the node type In figure 5 6 are represented all the classes and the relations between them from this plug in The GSN ontology plug in is implementing the communication of our tool
53. on logic are enacted to verify the compliance of the case with the GSN standard and also to signal possible argumentation flaws 16 1 1 ORGANIZATION OF THE PAPER 17 1 1 Organization of the paper Chapted I presents an introduction in arguing software safety domain In Chapter II we introduce the theme and the objectives of our system In Chapted III are presented all the references for the project within the project domain and related work Chapter IV presents the elements of a safety argument introduces the techincal instrumentation used the Goal Structuring Notation plus description logic Chapter V details the architecture of the system and implementation In Chapter VI are presented the needed resources and steps for installing the appli cation and how to use it Chapter VII focuses on methods for testing and validating our tool Finally in Chapter VIII we present the conclusion and further work Chapter 2 Project Obectives and Specifications 2 1 Problem Statement and Solution For many systems that present a certain level of resk safety is a good practice to justify prior to deployment if and why the sofware behavior should be trusted Because structured and evidence based arguments are more and more used to describe the assurance of the system many international standard adopted this strategy As explained in table 2 1 the problem arises in assessing complex safety cases and proving that the system is sufficiently se
54. ool screenshot AdvoCATE 2 is an Assurance Case Automation ToolsEt to support the auto mated construction and assessment of safety cases The tool is more complex then ACedit 22 23 AdvoCATE is an assurance case automation toolset and has been build to support the automated construction and assessment of safety cases The main features of the tool are i create and edit of assurance cases ii import and export of a variety of safety case for mats currently those produced from the ASCE CertWare and D Case tools iii assemble automatically fragments of safety cases iv Computation of metrics direct measurement and evaluation of the safety case Figure 3 2 represents a scrrenshot of this tool cir e la afro EI O lt Ecore gt Project Explorer 6 s mx s Sad ii 42 Palette G Gjavatar tests ae Pal EJ avatar ul y Select gt US certware sc test J Marquee gt I D CaseTemplate TU nasa tr work v Ep src Y E diagrams 2 Manual SC v2 diagram T Manual SC diagram Z TR SUAS SC diagram E Manual SC egsn E TR SUAS SC egsn US safecomp work gt 3 safery case test N25126301 Definition of software fare Software tata alp ie 53 Connections nen the intended benawor cevates from ves when ihe specficaton isSolvediy InContextOf gt Objects Goal Assumption Context Evidence Justification Strategy during descent 84081307 safety top
55. other can t import other other diagram diagrams types diagrams types diagrams types types from D case Asce Metrics not Limited available using available computation of metric Racer lisp library Diagram not all diagram nodes Reasoning services used Assesment and available are saved on columns Better dynamic and evaluation in CSV based on more flexible solution their type than limitation of their type displaying on columns Diagram based only on based only on based only on Validation constraints constraints constraints plus digram consistency and missing elements Reporting not CSV with nodes Three pdf reports available structured on validation to do and documentation 7 1 Chapter 7 User s manual System Installation For using the tool the user needs to have installed on the PC the following Eclipse Distribution with Epsilon this can be downloaded from here http www eclipse org epsilon download RacerPro knowledge base reasoner on 32 bits NaturalOwl engine To install the tool through eclipse updates Open the wizard and select from Eclipse top menu Install Update gt Availbale Soft ware Sites Click the Add button If the sofware site is in your local file system click Local to specify tyhe directory location of the file If the software site is in your local file but packaged as a jar or zip click Archive to specify the name of the file Select Add Site Select
56. ound 6 2 The user starts manually the engine 6 1 Query is incorrect 6 1 System notifies in the console the user to re enter the query 6 2 User re enters query 4 5 2 Validating the Safety Case When analysing the diagram by querying the RacerPro engine the safety engineer can simply identify the goals from the diagram that are still undeveloped or not supported by evidence goal descriptions or retrieve explanation why a goal belongs to a specific concept check the consistency of the Abox In this way the safety engineer can repair the problems and validate The following formal verifications are provided by the SafeEd system 1 Every node can be traced back to the top level claim That is there are no dangling nodes or sets of nodes 4 5 FUNCTIONALITY 39 Table 4 2 Retrieving information about the safety case Query RacerPro query Top level goal concept instances TopLevelGoal Support goals concept instances SupportGoal Evidence supporting goal g retrieve individual fillers gg hasEvidence Undeveloped Goals concept instances UndevelopedGoals Generate OWL save kb PATH kb owl syntax owl Check if Abox is consistent aboz consistent Get all contexts of a specific individual fillers g inContextOf goal 2 Each leaf node should either evidence or a reference to some previously reviewed assurance case 3 Cir
57. pplication of dynamic risk assessment G2 G3 Vehicle maintains situation awareness SAW model is correct sufficient and assures vehicle savety E2 E3 Evidence based on the analysis of simulated and recorded real scenarios Evidence based on simulation ci Environment profile definition c2 Situation awareness SAW model G4 G5 Vehicle performs optimal Environment safe actions according profile to the vehicle policy assumption are not violated E4 Evidence based on operational system performance statistics Figure 6 1 Autonomous vehicle scenario Table 6 1 Retrieving some information about the safety case represented in figure 6 1 Query RacerPro query RacerPro answer Top level goal concept instances TopLevelGoal g Support goals concept instances SupportGoal 92 93 94 95 Evidence supporting goal g retrieve individual fillers gg has evidence 1 2 es Undeveloped Goals concept instances UndevelopedGoals 93 04 95 Check if Abox is consistent abox consistent Get all contexts of a specific individual fillers g inContextOf C2 goal The second safety case is taken from medical industry and refers to the Therac 25 a case study in safety failure In figure 6 4 is a diagram build wit our tool representing the case of Therac 25 presented in 12 6 1 TESTING THE TOOL 59 2 gt G
58. relations Having the diagram and diagram documentation facilitate the work of the safety engineer or certification auditors 4 5 FUNCTIONALITY 41 Select Commands Console Add the Console from Open RacerPro RacerPro Opened View Results Figure 4 8 Flow Chart Querying the diagram 42 CHAPTER 4 ANALYSIS AND THEORETICAL FOUNDATION No RacerFile found Select Diagram Translation Open RacerPro Figure 4 9 Flow Chart for validating the diagram Chapter 5 Detailed Design and Implementation Out tool is an improvement of Acedit 1 tool New features like the option of querying the diagram generation of reports and documentation usage of safety metrics for the assessment of the safety cases have been added and others tool features have been improved for example the validation of a diagram 5 1 System Architecture The tool consist of a set of Eclipse plug ins User Interface model management tools Tool Core GSN plug ins Ontology plug ins reporting plug in Core Framwork Eclipse Framework Figure 5 1 System Archtecture As presented in figure 5 1 the tool is structured on layers as follows e first layer is the one at the bottom and consists of the core framework of the tool 43 44 CHAPTER 5 DETAILED DESIGN AND IMPLEMENTATION e second layer consists of several eclipse plug ins used to implement the tool EMF GMF GEF plus the libraries used for establishing co
59. s known do not violate safety assumptions claims 39 instance G7 Goal 40 attribute filler G7 Out of area events known do not violate safety assumptions claims 41 related G7 E4 has evidence 42 instance E4 Evidence 43 attribute filler E4 Evidence that out of area events known do not violate safety assumptions claims 44 realize abox 45 set current abox safetyATM racer GSN 46 Figure 6 7 Airspace system safety case translated in Abox using our tool assesment evaluation and reports generation A minus would be the weak graphically representation of elements and importing exporting diagrams from our tool The difference between our tool and this one is the fact that using ours the user will be able to build simple or complex queries for interrogating the diagram at any time during the development and not being limited only to metrics this is a plus at the assessment of the diagram available columns 62 CHAPTER 6 TESTING AND VALIDATION Table 6 4 Tools Comparison Table Functionality Acedit AdvoCATE Our Tool Creating GSN models must be GSN elements GSN models must be diagram differentiated better 1 are better represented differentiated better in the interface color is a plus in the interface Edit can edit only can edit other can edit only diagram diagrams build diagrams diagrams build with the tool type with the tool Import Export can t import other can import
60. sByEvidence String findRacer String startRacer getName String Tho setName name String definePrimitiveRoles String getContent String impliedConcepts staticString uivalentCon Stri getFile concepts String setfile file File concretedDomainAttribute String addBasicRules String Figure 5 7 Class diagram for ontology plug in 5 3 User Interface The workspace of the system is presented in Fig 5 8 A safety project top left consists of several assurance cases developed either as a graphical diagram files with gsn extension or as an abox in description logic files with racer extension In case of need the system automatically translated between these two input formats For a selected diagram file the user can transform into abox validate the diagram and generate reports The main window top cencer depicts the active gsn diagram The elements of the GSN standard are represented as follows goals with rectangular strategies with paralel ograms evidence and solutions are represented by circle assumptions and justifications with ellipse context by a rectangular with rounded corners the supportedBy relation is an arrow with the head filled while the inContextOf is represented by an arrow with empty head The title and description of a node can be entered by clicking on the node in the head part for the title and in the field with the placeholder description The diagram is
61. se argument on basic ATM rules claims 8 related 51 62 supportedBy 9 related S1 G3 supportedBy 10 instance G2 Goal 11 attribute filler G2 Basic ATM rules are safe claims 12 related G2 El has evidence 13 instance El Evidence 14 attribute filler E1 Evidence that basic ATM rules are safe claims 15 instance G3 Goal 16 attribute filler G3 Basic ATM rules are implemented safely claims 17 related 63 52 supportedBy 18 instance S2 Strategy 19 attribute filler S2 Basic ATM rules implemented safety in each geographical area claims 20 related 52 64 supportedBy 21 related 52 65 supportedBy 22 instance G4 Goal 23 attribute filler G4 Basic ATM rules implemented safely in each area claims 24 related G4 E2 has evidence 25 instance E2 Evidence 26 attribute filler E2 Evidence that basic ATM rules implemented safely in each area claims 27 instance G5 Goal 28 attribute filler G5 Assumptions for Area safety cannot be violated claims 29 related G5 S3 supportedBy 30 instance S3 Strategy 31 attribute filler S3 Whole airspace and out of area events cannot violate safety assumptions claims 32 related S3 G6 supportedBy 33 related S3 G7 supportedBy 34 instance G6 Goal 35 attribute filler G6 Whole airspace events known do not violate safety assumptions claims 36 related G6 E3 has evidence 37 instance E3 Evidence 38 attribute filler E3 Evidence that whole airspace event
62. se given as the ABox scl is computed with length concept instances NotVerifiedGoal or the number of undeveloped goals length concept instances UndevelopedGoal The main use case of metrics is to assess the progress during different stages of validating the safety case Given large safety cases one can monitor the rate to which the number individuals of type Not VerifiedGoal decreases 4 5 4 Generating Natural Language Reports on the Safety Case Our tool supports the generation of documentation and reports for the safety case There will be generated three types validation report to do or assement report and diagram documentation The to do reports contains things that still needs to be done assessment and vali dation of the safety case The validation report includes e nodes that do not have a description e elements that are not linked directly or indirectly through other elements of the diagram to the top level goal e goals that do not have evidence or solution e incomplete goals that have undeveloped sub goals With this report the safety engineer knows at any moment what still needs to be added to the safety case to have a complete and well build safety case The assessment report provides also quantitative information of the diagram in terms of number of nodes and their types The documnation file will include the assessment report and description of every goal node of the diagram including attributes and
63. tigates the issues of autonomy for safety critical systems the ways of safety assurance and the structure of safety arguments He proposes two approches for autonomous vehicle safety The first one is the classical one uses hazard analysis approach and is based on safety barriers This solution aims to iden tify event sequences leading to accidents and ways to control risks the safety is perceived in a binary way The second solution is based on the dynamic risk assesment approach i e design a system which is able to perceive and interpret risk factors and evaluate if foward ing will lead to a safe state or ends with an accident Autonomous systems rise problems for safety analysis and safety assurance and therefore for certification ISO 26262 stan dard and safety cases of systems obeying this standard have been studied in papers 10 and 11 The standard for vehicles requires building a safety case for electrical electronic that presents a certain level of risks in order to prove that the system requirements are complete and satisfied by evidence In the paper 12 the user presents the case study of Therac 25 machine that had massively overdosed six people Therac 25 is a computer controlled therapy machine that can treat the patient with relatively low energy electron beams or with X ray From the safety analysis of the system it can be seen that the developers focus more on the tech nology from olders versions of this machine than on the c
64. xt in which the argument is made so that the graphical representation of the safety case will be well structured It s a good practice to develop the safety cases prior to development because in this way you find the risks and faults before starting the development so you ll have the solution to mitigate them This paper described our tool that can not only be used to build safety arguments according to the Goal Structuring Notation standard but it also provides a better manage ment and assesment of the safety case The novelty of our approach is that the assurance case is automatically translated in description logic The advantage is that the specific reasoning services of description logic are enacted to verify the compliance of the case with the GSN standard and also to signal possible argumentation flaws The tool was demonstrated when developing safety all the safety cases presented in Chapter Testing and Validation The main advantage of our the tool is that it can reduce the risks of not building well structured safety cases or not provide evidence for all the statements from 67 68 CHAPTER 8 CONCLUSIONS the safety case Another big advantage is that our tool is extensible and can integrate with other corporate applications developed based on the Eclipse platform In this line ongoing work regards enhancing the tool with other 8 2 Further Work There are some improvements that can be done in the future to improve the tool and a
65. y case must be clear because all the information provided must be understood by unexperienced people e system a safety case can be build for any system acceptably it is very hard to prove that a system is 100 safety the goal of an assurance cases goal is to convince the others that the system is safety enough to be used e context The context of using the system must be specified in the safety case because context free safety is impossible to argue 4 1 1 ISO26262 standard Many safety standards require now the construction of safety cases for systems that may present a certain level of risk THe ISO 26262 standard states that any electrical electronic product must ensure an acceptable level of safety and requires building a safety case but it does not tell you the steps of building it 13 Fig 4 3 shows how such an analysis is performed in order to comply to the 15026262 requirements according to 14 The figure presents only the hazard analysis and risk assessment component The top level goal Goal1 is to show if the product ensures a sufficient and acceptable level of safety The user should structure the safety case into product assurance cases and process related assurance cases In figures 4 3 4 4 4 5 is developed only the hazard analysis and risk assessment claim of the product and is shown the corresponding process based Goal 2 and product based Goal 6 arguments The process based goal Goal2 in refined in

justifying software systems safety using arguments

Contents

Download Pdf Manuals

Related Search

Related Contents