Assurance Case Design: Proving Spousal Coffee Satisfaction

Practical Assurance Case Design IV&V Workshop S. R. Brown KeyLogic Inc With my thanks and appreciation Don Ohi Project Monitor Travis Dawson Chief Engineer Bill Stanton for tolerating a lot of questions 9/2/2013 1

Why Assurance Cases State your case: What are we trying to prove How are we trying to prove it What evidence supports the proof Assurance Cases make the point Design of Assurance Support of Assurance GSN Standard Kelly, T.: 'Arguing Safety: A Systematic Approach to Managing Safety Cases', D.Phil Thesis, University of York (1998). Available for download from http://www-users.cs.york.ac.uk/~tpk 9/2/2013 2

State Your Case Spousal Coffee Assurance Case ID EC_01 My coffee will provide spousal satisfaction Label JC_01 Spousal coffee satisfaction is critical to morning kharma. Label AC_1 Examine each element of coffee satisfaction ID EC_02 ID EC_03 ID EC_04 The coffee is adequately hot Two creamers have been added to the coffee No sugar has been added to 9/2/2013 3 the coffee Label JC_02 The two key parameters in coffee temperature are initial temperature and time to serving. Label E_C01 Label EC_02 AC_02 Label Argue through coffee temperature discriminators. Two creamer packets are on the the counter No sugar packets are on the counter ID C_1020 ID C_1020 The coffee pot heater is on and operating The coffee is serves with no more than three minutes delay. Label EC_03 Label EC_04 The coffee warmers are operating. The coffee isserved immediately

ID EC_01 My coffee will provide spousal satisfaction Label JC_01 Spousal coffee satisfaction is critical to morning kharma. Make the Argument Label AC_1 Examine each element of coffee satisfaction ID EC_02 ID EC_03 ID EC_04 The coffee is adequately hot Two creamers have been added to the coffee No sugar has been added to the coffee Label JC_02 The two key parameters in coffee temperature are initial temperature and time to serving. Label E_C01 Label EC_02 AC_02 Label Argue through coffee temperature discriminators. Two creamer packets are on the the counter No sugar packets are on the counter 9/2/2013 4 ID C_1020 ID C_1020 The coffee pot heater is on and operating The coffee is serves with no more than three minutes delay. Label EC_03 Label EC_04 The coffee warmers are operating. The coffee isserved immediately

ID EC_01 My coffee will provide spousal satisfaction Label JC_01 Spousal coffee satisfaction is critical to morning kharma. Label AC_1 Examine each element of coffee satisfaction ID EC_02 ID EC_03 ID EC_04 The coffee is adequately hot Two creamers have been added to the coffee No sugar has been added to the coffee Gather the Evidence Label JC_02 The two key parameters in coffee temperature are initial temperature and time to serving. Label E_C01 Label EC_02 AC_02 Label Argue through coffee temperature discriminators. Two creamer packets are on the the counter No sugar packets are on the counter ID C_1020 ID C_1020 The coffee pot heater is on and operating The coffee is serves with no more than three minutes delay. Label EC_03 Label EC_04 The coffee warmers are operating. The coffee isserved immediately 9/2/2013 5

Assurance Case Semantic Content What I get out of a cup of coffee: The assurance design is not a description of the system Assurance network needs only to go as far as necessary to provide stated assurance Strength of evidence is a constant consideration Without more information there is little basis for claim prioritization Can address risk (uncertainty) Does not support consequence ID EC_01 My coffee will provide spousal satisfaction Label JC_01 Spousal coffee satisfaction is critical to morning kharma. Label AC_1 Examine each element of coffee satisfaction ID EC_02 ID EC_03 ID EC_04 The coffee is adequately hot Two creamers have been added to the coffee No sugar has been added to the coffee Label JC_02 The two key parameters in coffee temperature are initial temperature and time to serving. Label E_C01 Label EC_02 AC_02 Label Argue through coffee temperature discriminators. Two creamer packets are on the the counter No sugar packets are on the counter ID C_1020 ID C_1020 The coffee pot heater is on and operating The coffee is serves with no more than three minutes delay. Label EC_03 Label EC_04 The coffee warmers are operating. The coffee isserved immediately 9/2/2013 6

Where to Start Is Clearly Stated Initially a major goal: In almost every case it is self-evident if the objective is defined. This is where perspective becomes important. Consider stakeholder needs. Testable (yes/no) Will decompose in a useful way ID G_1 Lessons Learned: The GENERIC Spacecraft will travel to Planet X and enter orbit, remaining in orbit doing nothing in particular until the requir Look for simple and comprehensive claims Claims must be objective (yes/no) Watch out for claims that must decompose through out-of-scope domains (e.g.: reset/sideswap hardware timing) Take advantage of self-similarity, patterns and common arguments. 9/2/2013 7

Perspectives and Planning The perspective of the assurance case is important Software lifecycle (NPR 7150) System/Human safety 09-1 System definition Project-specific 9/2/2013 8

Argument: the Art of Assurance Case Arguments are in the context of the system Appeal to Specificity Provide detail to support a more general claim Little uncertainty Arguments describe how the child claims satisfy the parent claim but do not carry the burden of proof Some Useful decomposition classes Appeal to Usage Use scenario to decompose to subsystems by required actions Some uncertainty Some approaches require a justification for each argument but this was often redundant. Assumptions are often necessary in order that the argument is clear to a reviewer Note: 3Q is a special case of appeal to usage Appeal to architecture Use software architecture to decompose to subsystems No uncertainty Use cases can be a good basis for an Appeal to Usage. Note semantic equivalence. 9/2/2013 9

ID G_56 When to Stop The spacecraft will calculate estimated attitude based on IMU, STAR, and SUN sensors Label J_701 Label S_700 AD performs sensor integration via a 12 state Kalman Filter. Steps include forward propagation, noise covariance update bias update, and check Iterate through AD functional Completeness Are all claims fully decomposed? Are all assumptions described? Depth Is there evidence that is directly relatable? Abstraction Are sub-claims at (more or less) the same level of abstraction? Is evidence ascribed at the appropriate level of abstraction? Generally the lowest level claim can be supported by one or more low level requirements. Software architecture level System-level tests and requirements are evidence too, but lower- level evidence is earlier in the project and often less ambiguous. behaviors Label J_702 for divergence. Kalman filter algorithms are not validated (scope). There is evidence to support this assumption but the decomp is out of scope. ID G_701 The AD system will calculate state propagation ID G_702 ID G_703 The AD system will calculate noise covariance and accelerometer bias The AD system will detect Kalman filter divergence Label E_703 FVT_AD.301 Label J_704 J_703 Label ID G_704 ID G_705 If the covariance exceeds a configurable threshold the Kalman filter will re-initialize If, after Kalman filter reset, another divergence is detected within a configurable period, the high level fault protection will force a side swap. Ibid J_702 Ibid J_702 Label E_701 Label E_702 E_705 E_706 Label Label L5_FSWGNCxxxx UT_xxxx L5_FSWGNCxxxx UT_xxxx 9/2/2013 10

Top Down or Bottom Up? GSN Standard describes both methods, then tosses in a third use both. Practical use dictates that both are necessary for IV&V Top level claims provide the entire motivation for the assurance case Evidence is determined by a combination of artifacts and IV&V analysis. 9/2/2013 11

GENERIC PBRA Summary GENERIC PBRA Summary 5 7 16 20 23 25 4 Capability 1 Launch 2 Commission 3 Cruise 4 POI 5 Do Nothing (science) 6 Health and Maintenance 7 Disposal 6 13 18 22 24 Probability 3 4 11 15 19 21 2 3 1 4 2 6 5 2 8 10 14 17 7 1 1 3 5 9 12 1 2 3 4 5 Impact 9/2/2013 12

Using the Assurance Cases with PBRA ID G_53 L_54 CFL = Critical failure list GENERIC 02-003 The GNC system will autonomously complete the POI maneuver in the presence of any single failure not on the CFL Label J_61 Label S_1 Behavior decomp could be done using either a step-by-step scenario decomp or the 3Q decomp. In this case the 3Q decomp prompts a look at the failure cases fairly early, driving out some of the bigger behaviors like reset/reboot Use 3Q decomposition J_61 This branch covers the non- failure nominal behavior G_61 ID ID G_62 G_64 The FSW will persist in POI in the presence of any failure not on the CFL The FSW will execute the maneuvers required for POI J_62 This branch addresses failure cases (Q3) We can map scenario steps to the assurance case because we used them for decomposition Semantically, it seems that scenarios map to arguments (decomp by behavior), and scenario steps map to claims. The FSW will not generate or permit commands which would prevent POI C_61 The GENERIC POI maneuver is defined in GMP Section 7 and is comprised of a series of sequences running in a VM S_S_67 Label There are two types of maneuvers required, the TCM and the POI burn. Treate as separate cases since they are distinct commands and have different fault responses. J_64 This branch addresses bad behavior (Q2) ID G_65 Label A_611 ID G_66 GENERIC FSW will perform the TCM sequences The GENERIC FSW will perform the pre-POI configuration sequence correctly The sequences are constructed properly commands Label J_600 Label S_1 Decompose by scenario steps (commands) Here we look at each command required for the TCM sequence C_62 ID G_610 All GNC error budgets are defined in the PPPC The Flight System will autonomously perform the POI maneuver. ID G_67 The FSW will turn to point at an arbitrary J-2000 reference using thruster and reaction wheel commands. E_600 GNCUTxxxx ID G_68 The FSW will perform translation dv maneuvers using RCS jets in an arbitrary J-2000 reference direction. ID G_69 Label J_67 Label S_65 The FSW will point the spacecraft toward the sun upon command using reaction wheels and thrusters if necessary. Iterate through POI scenario The scenario steps are based on Mission Plan (page). (Appeal to behavioral decomposition) steps Label E601 SVT_SunPoint Label J_610 ID G_613 ID G_611 ID G_614 ID G_612 The Flight System will set propulsion for main engine burn using prop/pyros to enable main engine flow The flight system will configure COMM for POI upon command The Flight System will start the main engine burn at the commanded SC_Time The Flight System will set POI_Timeout and POI_DVTarget per POI command parameters ID G_615 COMM is out of scope for now The Flight System will stop the main engine burn at POI_DVTarget or POIDVTimeout, whichever is achieved first. Label E603 Req L- Label E_609 5FSWGNCx Label E_608 Label E_604 xxx Label E_606 Label E_607 Label E_605 9/2/2013 13 Req L5- FSWGNCxxx Req L5- UT_INxxxx x UT_xxxx FSWGNCxxxx UT-xxxx FT_GNCxxxx

Odd topics Where does static code analysis fit into the picture? Certainly provides assurance in some sense Applies to the product in general but traceable to architectural components Claim: Module XYZ is free of implementation flaws How does uncertainty fit into the picture? IEEE15026 assumes there is a way to combine the independent (and ill- defined) components of uncertainty, or at least specify uncertainty. Even if we could calculate uncertainty, would it be a Good Thing? Would broad categories be sufficient? 9/2/2013 14

And now for something you will really like Hot spots for development Algorithmic blind spots Scoring or ranking system Real project testbed Structured GSN Is a practical S/C assurance case possible? Is a practical S/C assurance case useful? Is it difficult to write top-level claims? Is it difficult to develop arguments for decomposition? Can this be a uniform and systematic process for each project? 9/2/2013 15