Navigation
Minimap of introduction diagram
Minimap of stage diagram

SACE outline

AS verification argument pattern

The argument pattern relating to this stage is shown in Figure 31 below and key elements from the pattern are described in the following sections.

Figure 31: [UU]: Argument pattern for AS verification

This argument is created for each tier, to demonstrate that the verification evidence that is provided for that tier is sufficient to show that the safety requirements defined at that tier are satisfied.

The claim is supported by making an argument over the chosen verification strategy that is defined in [RR]. A justification for why the defined strategy has been chosen must also be provided (J8.1). The strategy may involve testing, formal verification, or some combination of these approaches. Where testing is used, claim G8.2 must be instantiated. Where formal verification is used, claim G8.6 must be instantiated.

Where testing is being used, for each of the defined safety requirements it must be demonstrated that the testing undertaken demonstrates that the requirement is satisfied. To support this claim it is necessary to show that the relevant test cases are passed (G8.3), that those test cases are sufficient, given the operating context of the AS, to demonstrate that the requirement is satisfied (G8.4), and that any test platform that was used to perform the tests is sufficiently representative (G8.5). The verification log ([SS]) is used as evidence to support these claims.

Where formal verification is being used, for each of the defined safety requirements it must be demonstrated that the verification undertaken demonstrates that the requirement is satisfied. To support this claim it is necessary to show that the formally specified properties have been proven to be satisfied (G8.7), and that those specified properties are sufficiently representative of the safety requirement in the AS operating context (G8.8).

To demonstrate that the formally specified properties are satisfied, the results of the formal analysis ([TT]) are used as evidence (Sn8.4). It is also necessary however to demonstrate that the formal model that is used to undertake the analysis is an accurate reflection of the real AS in its operating environment. This claim is made at G8.10 and is supported by evidence from the verification log ([SS]).

Continue to: Stage 9. Afterword - authors and thanks

Our site depends on cookies to provide our service to you. If you continue to use this site we will assume that you are happy with that. View our privacy policy.