Our blogs typically concentrate on technical details which will help with the detailed verification of your software. This blog sets the scene to future blogs describing some of the ways in which our verification tools can be used to help meet safety certification requirements. Verification data provides evidence about the performance and functionality of your code, however, you'll also need to justify why that verification data is relevant, how it fulfills certification requirements, whether it is sufficiently complete, consistent, correct etc.. When certifying a safety critical system there is a need to present a safety case, which consists of two parts:
- Evidence data about your software such as test results, failure analysis, requirements specifications, hazard logs...
- Argument justifying the relevance of your evidence in demonstrating that the software is sufficiently safe. For example, showing that all requirements have been traced to the implementation, that each hazard has been mitigated, that the test data covers all necessary test cases and so on.
There are a number of equally valid ways of presenting your safety argument, such as simply presenting via a text document, or using a graphical notation. Here at Rapita we tend to use the Goal Structuring Notation (GSN), originally adapted for safety case use by the University of York [1]. We've found this very useful internally when developing qualification kits, and when talking to customers to demonstrate a) how our products can help meet certification standards and b) how to ensure the most compelling and useful output from our verification tools. The main symbols of GSN are in the image below. Rectangles represent Goals (also known as claims) which need to be met. Claims start at a high level, which broad claims about your system or software which can be systematically decomposed to smaller goals. Eventually these can be individually supported by evidence (also called solutions), represented by circles. Other symbols include parallelograms as strategies (describing how you intend to decompose your argument), and lozenges as context. Assumptions and Justifications can be represented using ovals. A simple (incomplete!) example is shown below for illustration.