Determine verification strategy

An appropriate verification strategy shall be adopted. At the highest level this will require a decision on whether verification shall be undertaken using testing, formal verification or a combination of both approaches. The advantages and disadvantages of using either approach for the verification of AS are discussed below.

Testing Testing involves exposing the system to a defined set of inputs and checking that the outputs or behaviour of the system is as specified and safe. The main advantage of using testing is that evidence may be generated against the real system operating in the target environment. This means that demonstrating the relevance of the verification evidence to the AS operation is comparatively straightforward.

Some testing of AS may however be performed in a controlled environment, such as a test site or a laboratory setting, requiring that the similarity to the actual operating environment is demonstrated. The main disadvantage is that testing cannot be carried out exhaustively, so achieving an acceptable level of coverage of the operating domain can be very challenging, particularly for AS in complex operating environments that represent a very large state space. Providing justification for the acceptability of the level of coverage that is achieved is also a major challenge.

Simulation Testing does not always need to be performed using the target AS in its intended operating environment. Particularly for AS, simulation may also be used for the purposes of testing. Simulation may be used for a number of reasons:

• it can allow verification activities to begin earlier in the development lifecycle, since a fully developed system is not required
• it can also enable tests to be carried out that would otherwise be difficult to create (due to their rarity in the real world) or dangerous to perform (since they would require exposing people to unnecessary risk)
• it can also be used as a way of increasing the coverage that can be achieved through testing, by enabling test cases to be created quickly and cheaply.

The disadvantage of using simulation is that all simulations are models of the real world and justifying the representativeness of the simulation models can be challenging. This is discussed further in Activity 29.

“In‐the‐loop” simulation is an approach that can be used as part of the verification of an AS in which real system components are used to provide inputs to the simulation. Using an in‐the‐loop approach can help to ensure that the data used by the simulation during verification is representative of the data to which the AS will be exposed during operation.

Formal verification Formal verification involves using mathematical techniques to prove that a formally specified model of (some aspect of) the AS will always satisfy a set of formally specified properties. The main advantage of using formal verification techniques is that the properties are proved to be true for the entire scope of the model of the AS, meaning that the challenge of demonstrating sufficient coverage that existed for testing is avoided. The disadvantage of using formal analysis is being able to demonstrate that the analysis results are a true reflection of the real system in operation. Firstly, in order to support verification, the formally specified properties that are defined must sufficiently capture the intent of the safety requirements being verified. Secondly, the formal model, upon which the properties are proven to hold, must be sufficiently representative of the system itself, and any elements of the operating environment included in the model. All models require abstractions and assumptions to be made. For complicated AS operating in complex environments demonstrating the acceptability of the abstractions and assumptions made is challenging. Due to these challenges, formal methods should be used with caution for AS, and should be done so in combination with testing. An overview providing further details of different applications of formal methods to AS is available at [30].

The chosen verification strategy shall be documented ([RR]).