Generating and verifying configuration data with OVADO²®

The OVADO²®¹ tool has been used for more than a decade to formally check whether system configuration data comply with their rules in the context of railway systems². OVADO²® is currently deployed in SIL4 processes compliant with the safety requirements of the CENELEC EN 50128 standard. In these processes, it is considered a T2-class tool since it only helps to verify the system. This article describes how the OVADO²® tool has been used, for the first time, by Systerel to formally generate equipment configuration data derived from the system configuration data.

This innovative use has been applied in a real industrial context, the deployment of the OCTYS VTPA system by Alstom on Line 6 of the Paris metro operated by RATP. The industrial process had to be adapted in order to remain compliant with a SIL4 safety level of the EN 50128 standard. The OVADO²® tool is considered a T3-class tool for this new purpose since it now produces system configuration data.

OVADO²® Basic Usage¶

The OVADO²® tool is an evaluation engine that takes as inputs configuration data and a formal model (in B language) of rules on the data and that verifies whether each rule holds. Figure 1 illustrates the tool’s basic workflow. The tool consists of two independent tool chains, allowing it to be used in a SIL4 process. The first chain is developed in Java/Eclipse as an engine evaluating B language predicates and expressions until getting to data values. The second chain first produces a B abstract machine gathering data values and rules modeled as B properties and then calls the B model-checker ProB to evaluate the rules.

Figure 1: Basic use of OVADO²® to check whether data comply with their rules.

OVADO²® can interface natively with data from XML or Excel files. To interface with other data formats, it is possible to develop specific extension modules. In this case two independent modules must be developed, one for each OVADO²® tool chain.

The formal model of the rules is composed of 3 parts: the interface with input data, intermediate definitions and the rules themselves. The intermediate definitions permit to develop intermediate abstractions, in order to avoid working directly with the raw configuration data, and they also allow reusable library functions to be defined.

Then, OVADO²® can evaluate for each rule if the data respect the rule or not. To do so, it evaluates the rule as well as each intermediate definition transitively used till it gets to configuration data values. When a rule is not obeyed, OVADO²® produces a list of counterexamples to the rule and helps the user to analyse the causes of the rule violation.

OVADO²® Used to Check Railway Systems¶

To configure railway systems, the data is usually split into two parts: high level configuration data of the system provided in a user-friendly format (e.g. XML or Excel) and low level configuration data loaded into the different devices of the system provided in a specific format (e.g. binary data). Low-level data is deduced deterministically from system high-level data. Until now, it was produced by software tools developed specifically for data generation with no safety requirement as the safety issues were entirely covered by the verification activity.

Data verification with OVADO²® consists in verifying the data rules issued by the various stakeholders in charge of the system configuration and verifying the consistency between the implementation data and the system data from which it is derived. To achieve this consistency check, the OVADO²® model includes the definition of the theoretical computation of the equipment configuration data from the system data, as well as the equality properties of the latter with the equipment configuration data produced by the data generation tools. Figure 2 illustrates this use of OVADO²®.

Figure 2: A more complete use of OVADO²® in which the rules on the system data and the correct construction of the equipment configuration data in relation to the system data are checked

A New Usage of OVADO²® to Generate Data¶

Originally, the OVADO²® tool was only used to evaluate rules on configuration data, which means computing a Boolean result (TRUE or FALSE) for each evaluated rule. However, the tool can evaluate any intermediate expression modeled from the input data and not only Boolean expressions. Over the years, several OVADO²® extension modules have been developed to exploit some of these intermediate expressions, such as the module for displaying counterexamples of rules and the module for displaying interactively any expression to perform analyses on data or to debug the model. A data export module has been developed for this project, so that OVADO²® can now generate configuration data, as shown in Figure 3.

Figure 3: New use of OVADO²® to generate equipment configuration data from system data.

In this solution, the formal model mainly contains the definition of the equipment configuration data computed from the system data. OVADO²® evaluation engine can evaluate those data and a new generic extension module has been developed to export them into an XML file. The equipment configuration data being defined as a specific binary format in hexadecimal files, a specific tool for formatting XML data in hexadecimal data has also been developed.

In order to be able to generate data, the system data must respect certain consistency constraints. Moreover, since the generated data must fill tables, the constraints of the format of these tables must also be obeyed. For instance, there should be no overflow of the number of elements and no overflow of the values of the elements. All these constraints constitute consistency rules that must be enforced. It was natural to verify these rules by integrating them into the formal OVADO²® data generation model. Before generating configuration data, it is necessary to check those rules in order to guarantee that this data generation is feasible and conforms to what is expected.

The safety strategy does not rely on producing safe configuration data. It relies on verifying safely that configuration data produced are correct. This strategy covers possible errors that may occur at any step of data production: evaluation of data inside OVADO²®, generic export into XML files, translation into specific binary format or even while copying and delivering data configuration files. That is why only the first chain of OVADO²® is used to generate configuration data. However, both OVADO²® toolchains are still used for the verification activity.

This new use of OVADO²® changes its tool class according to the EN 50128 standard. Indeed, it goes from being a T2-class tool (tool used for verification only) to a T3-class tool (tool contributing to the generation of code or data of the safety critical software).

This innovative approach has several advantages. It raises the quality level of the data generation solution, as it is now based on a formal model close to the data specification and on a generic evaluation engine (OVADO²®). It also reduces the costs by factoring out common activities between generation and verification.

Adaptation of the SIL4 Process¶

This approach requires managing the common mode between data generation and verification in the OVADO²® model. Indeed, 80% of the OVADO²® model is dedicated to the computation of intermediate data used to produce the theoretical equipment configuration data. The remaining 20% represent the pure modeling of the rules.

Mitigation of a common mode error within the model is performed thanks to a detailed verification activity of the OVADO²® formal model. In this activity, each model element is verified independently and traced in auditable records by filling about fifteen criteria established following the feedback of both Systerel and RATP OVADO²® modeling experts. This verification activity has to be done once for a given OVADO²® model. When the input documents describing the data and rules evolve, the OVADO²® model creation activity and its detailed verification activity must be reworked, addressing only the differences. For each element of the OVADO²® model (rule, intermediate definition or interface with a constant), examples of verification criteria are: the presence of a natural language specification of the element and its completeness and consistency with the formal model, compliance with naming rules, data type verification, Well-Definedness verification, the presence of comments for case-based modeling or for tricky modeling points, traceability and compliance with the documents specifying the rules and the data format. There are also several criteria dedicated to the railway domain, such as consistency between the different references on the track, the consistency of the position of switch points on several tracks or unit consistency for the physical quantities. The Well-Definedness verification is done by providing an informal proof. For instance for a given $f(x)$ expression this proof may rely on $f$ being a function and $x$ being part of the domain of $f$.

From an industrial point of view, the cost of this detailed verification activity of the OVADO²® formal model is estimated at 10 to 15% of the development cost of the model.

Conclusion¶

To conclude, this article presented how the OVADO²® tool, that was primarily used to the verification of configuration data of railway systems from a formal modeling of the rules on the data, was successfully used, in addition to its primary use for verification, to generate configuration data of railway equipment. This evolution brought the tool from the EN 50128 T2 tool class to the T3 tool class. It brings advantages in terms of translation quality and factorization of data generation and verification activities. Finally, this new use of OVADO²® still complies with a SIL4 process.