Back-to-back Testing

Problem Addressed¶

In critical systems, the standards provide some activities to control defects between the specification of a system and its implementation.

These activities include verification, testing, simulation, proof, validation and qualification of the tools used. One of the industrial problems concerns the difficulty of taking some value for the validation policy from all the work carried out on models or codes that are not yet the software executed on its execution platform.

The B2BT approach proposed by Systerel is in line with the techniques of automatic generation of test by Model Checking 1 2 3 but proposes to bring new elements of conviction to use more massively the work carried out on models or source code by an automatic generation of tests qualifying the conformity of executable software with the semantics of the model / source code.

Specificities of the B2BT Tool¶

The B2BT solution developed by Systerel is based on our existing technologies. We have therefore chosen to build our models in High Level Language (HLL) 4, the language used by our Systerel Smart Solver (S3) solutions 5. A model can be the result of different activities: either specific to B2BT activities, or reuse of validation and verification data, or automatic translation from another language, etc.

Finally, this model is used by the B2BT tool to generate test sequences.

B2BT falls into the category of testing by comparison of observable behaviour and as such, the sequences generated describe for each step of the system the expected outputs according to its inputs and the state of its memories. The choice of the strategy used for the generation of the sequences, as well as the level of confidence given to these sequences, are described in the second part.

Although not the focus of this post, it is important to note that the same HLL model, can be used by our S3-core analysis engine to perform formal proof activities.

Application to a Simple Model¶

In order to illustrate the process of sequence generation, a deliberately simple, but understandable and representative software application is detailed in this section.

Consider that this application has 2 inputs, represented by two Boolean variables \(I1\) and \(I2\), and 2 outputs, represented by two Boolean variables \(O1\) and \(O2\).

The observable behaviour of the outputs as a function of the inputs is described by the following boolean equations.

Let us further consider that we have a testable device, i.e. one whose inputs can be controlled in order to control its outputs, which embeds a software implementation based on the behaviour described in (1) and (2).

Sequence Generation¶

The HLL model corresponding to this system can be constructed. This model is explained in Fig. 1.

Figure 1: HLL model of the application

The HLL model is then used to generate the test sequences. At the end of the generation, a test case of length 4 cycles is obtained, as shown in Fig. 2 where each line represents the successive states (f for False, t for True) of each input variable (\(I1\) and \(I2\)) and each output (\(O1\) and \(O2\)).

Figure 2: Generated test sequence B2BT

Tests on Host Machine / Simulator¶

The host/simulator test allows a test facility to be set up with the finest checking facilities:

• The synchronisation of the execution of the system under test,

• Maximum observation (internal variables become accessible).

This maximum flexibility ensures the correct timing of the inputs as well as the fine synchronisation of the outputs.

“White Box” Testing¶

A “white box” test is when the test tool and the machine to be tested meet the following conditions:

• The test device interfaces with the target machine,

• The test facility has read and write access to the internal variables of the system under test,

• The test facility can control the start of a cycle on the target machine.

It is then possible to control the various operating cycles of the system under test or to force its variables.

“Grey Box” Tests¶

A “grey box” test is when the test tool can only read some or all of the variables in the system under test. In this configuration, it is always possible to synchronise the test equipment with the internal variables of the system under test. The system must of course have such variables (execution cycle counter, acquisition/transmission status, etc.).

“Black Box” Testing¶

“Black box” testing is when the test tool has no access to the internal variables of the system under test. Tests are particularly complex to implement in this type of configuration. It is possible to try to synchronise the test fixture and the system by setting their cycle times to close (ideally equal) values and starting them synchronously.

However, this type of configuration is much more sensitive to runtime discrepancies.

Controlling the execution of tests on a “black box” configuration may require a particular test generation strategy to make the scenario compatible with the possible shift of one cycle of the sample. Such a strategy is usually more expensive.

An alternative is to build an overlay to the system under test that embeds the test vectors and expected outputs in the system under test if its resources offer the capacity. This is a “white box” configuration, but it requires modifications to the software to make it compatible with the encapsulation.

Compiler Optimisation¶

Let us first consider that the model is a semantically equivalent image of the source code. The differences that are observable at test execution may arise from the platform on which this code is executed (set of hardware resources, base software, operating systems) or from the compiler used to transform it into executable software. The defects encountered can then be reproduced and analysed to identify the root cause. In the area of critical software development, (e.g. IEC 61508-3, IEC 62138), the standards require that the tools that contribute to the production of the executable software be evaluated with respect to the level of confidence about the absence of failure in the software. Compilers belong to this class of tools. This application of the B2BT can be seen as a solution for checking the output of the compiler at runtime on the target, capturing failures that impact on the output of the executable software. This analogy also applies to the runtime platform, but also to translation tools between higher-level semantics and a compilable language.

Based on this safeguard, it is now possible to consider B2BT as a means of mastering off the shelf tools. One application could be to allow oneself to exploit more widely the power of compilers, in particular the optimisation options when they are accompanied by restrictions such as “the activation of optimisation lifts the guarantee on the order of evaluation of the parameters of a function” when the B2BT tests are successfully carried out.

Continuity of Formal Verification Activities¶

Let us then consider the case where the model used to generate the B2BT tests is not derived from the code but is developed through formal property checking activities. The interest of formal property checking is to demonstrate mathematically that RAMS requirements hold on model, whatever the sequence of inputs considered and at whatever temporal depth in the life of the system. In this case, the contribution of B2BT is to be able to demonstrate that the machine under test has no observable mutations with respect to the execution semantics of the model that supported the proof activities. When the proof obligations of the formal model are shown as proven, this proof holds on the execution semantics of the model and by transitivity on the machine under test since it does not contain any observable deviation.

In this case, B2BT complements traditional validation strategies by allowing the demonstration of compliance with RAMS requirements by proof on a formal model associated with the demonstration of compliance with the semantics underlying the proof on the machine under test by the correct execution of B2BT sequences.

Such an approach makes it possible to consider hybrid validation approaches where the proof takes over the demonstration of compliance with the RAMS requirements. A proof approach provides complete coverage with respect to RAMS in the sense that the proof provides a demonstration that whatever the sequence of events on the inputs to a model, a proof obligation holds.

In comparison, an approach using functional tests is based on scenarii. Except for a few rare situations where completeness of combinations is possible, an approach by test only provides coverage by sampling.

The strategy is therefore to develop a validation policy consisting of a proof against RAMS requirements with automatically generated B2BT tests and some functional tests against non-safety critical requirements (usability, performance, liveliness, etc.). The proof provides full coverage of the RAMS requirements. The B2BT consolidates that the RAMS requirements are based on the execution of the semantics by fine sampling the respect of the execution semantics.

It is notable that the development of a proof is less costly in terms of workload than the development of a test in terms of engineering load. Indeed, writing a proof requirement consists in formalising the “WHAT” of a requirement.

This simple example shows that the proof offers full coverage (whatever the value sequences on the inputs, then the RAMS property is respected) where the test only samples (in the scenario approach, we test only one trace of the system against a huge, if not infinite, amount). It also demonstrates that the engineering effort associated with proof is more efficient and more robust to changes than the engineering effort associated with testing (proof does not search for scenarios, but establishes an invariant under all circumstances and the search is delegated to the machine).

Treatment of Obsolescence¶

Finally, consider the case where the model is derived from a software version of an obsolete equipment.

It is common in the industry that an equipment qualified in the more or less recent past can no longer be maintained, due to a lack of available spare parts or even a lack of a test environment that is still operational (test servers running obsolete OSs that security policies ban or will rightly ban from the networks because of their vulnerabilities). As part of the obsolescence treatment of such equipment, it is possible to generate test sequences for compliance with the execution semantics of the obsolete code using the B2BT approach.

These tests offer a finer coverage than validation tests: the successful completion of these tests demonstrates that the new generation of equipment has no semantic alteration in relation to the execution semantics of the qualified but obsolete version.

In the event that the owner does not have or no longer has the validation test facilities used at the time, the B2BT tests provide an automatic solution for rebuilding a new generation qualification repository. This approach must be weighed against obsolescence management with a set of functional evolutions. In this case, it will be necessary to proceed in two steps: qualifying the obsolescence treatment with the help of B2BT and then adding a set of tests or proofs dedicated to the functional evolutions.

This obsolescence treatment approach can be generalised more globally to the control of software being ported to new execution platforms.

Validation of a Critical System¶

The most ambitious prospective usage will be to use the B2BT technology for a critical system, coupled with a model produced by a validation team. Indeed, in this configuration, the validation team imposes through its model, the execution semantics of the object in accordance with the client’s needs without descending into the complexity of the production of the executable software or the security execution platform. This last use case proposes a strategy for the integration of commercial off the shelf components within critical control systems.

In fact, by ensuring that the execution semantics proposed by a commercial safety computer and its programming environment remain unchanged from those of a model of the requirement, the B2BT provides elements for an answer to the suitability for use of a safety computer with its programming environment provided as a black box with safe operating conditions.

Implementation on EDF Models¶

In partnership with EDF, Systerel has used the B2BT tool on a Lustre model provided by EDF. This model has been developed to match typical applications used in certain command and control systems of a nuclear unit. The objective is thus to evaluate the applicability of the B2BT method to nuclear applications. Several successive steps have been implemented to allow the use of this model to perform the generation of the B2BT test sequences.

Systerel and EDF have worked on the definition of high-level coverage criteria. Three high-level coverage criteria were retained to verify that the tests generated by the B2BT solution cover the particularly sensitive and critical behaviours of the application. Although these criteria are not detailed for reasons of confidentiality, it should be noted that they were specifically defined for this project. The walk through of the test sequences, with respect to these high-level criteria, will then increase the level of confidence in the coverage of the tests by B2BT: not only are all mutations tested, but all critical paths have been walked through.

These steps are briefly described below:

1. Pre-processing of input files The input files, in Lustre V6 format for the purposes of the study, require translation into the HLL language,

2. Analysis of the correct definition of the model

   Before launching the generation of the test sequences, a verification pass of the good design of the model is carried out using the S3 analysis engine. This check mainly consists of ensuring that the initial model is sound by confirming the absence of, for example, access to variables outside the defined bounds or division by zero.

3. Generation of test sequences

   Once the model has been translated and checked, it can be passed to the test sequence generation tool B2BT which will apply the mutations and produce test sequences to detect any defects.

4. Measurement of the coverage rate according to the defined criteria

   The generated test sequence is applied to the application model in order to measure the value of the coverage rate achieved for each of the defined coverage criteria.

5. Execution of the test sequence

   This last step consists of playing the test sequence on the target equipment. It should be noted that if step 1 introduces faults in the semantics, then these will be detected during the execution of the test, except in the case of combined faults.

   Due to the existence of long timeouts (several hundred cycles) in the application studied and the explosion of the state space inherent in the use of a proof engine at large depths, the model has been equipped to allow the control of memories and timeouts.

In addition to these two types of B2B test generation, we added some test sequence generation that focuses on higher-level test objectives.

Results¶

Conclusion¶

These different experiments have shown that this automatic test sequence generation method can efficiently address industrial system validation problems and take into account material constraints (standard or tooling test bench) and complexity constraints (generation by operator mutation or by high-level criteria only) for the execution of test sequences.