software & system
critical configuration data

OVADO is a RATP qualified and extensible tool dedicated to the formal validation of data.

Why using OVADO Purchase »

The OVADO tool

Formally prove model properties on data

Critical systems are complex and become more and more configurable. Assuring their behavior and their safety level requires to validate the consistency of several hundreds of thousands of values of configuration data. These validation tasks, particularly tedious and expensive, are often subject to very tight schedule as they are performed in the final phase of development.

OVADO offers an innovative approach to data validation based on the separation of the validation tool from the properties to validate.

The modeling team formalizes unambiguously the properties identified by domain experts.
Using this set of properties, OVADO checks automatically data conformity. The non-compliance of a data set is characterized by the extraction of counterexamples.

Costs reduction and shorter validation time

  • Expressiveness of the OVADO language
  • Simultaneous processing of properties
  • Carry-over of a common set of properties from one project to another
  • No need for a new qualification of the validation tool
  • Significant reduction of delay and cost of the safety case and its approval by an ISA
  • Quick and easy validation replay for each new data set

Increased validation quality

  • Shared language between domain experts and modelers
  • Exhaustive mathematical check of the properties on the configuration data
  • Readability and traceability of validation activities
  • Data validation through two independent and diversified toolchains
  • OVADO is certified T2 SIL4 according to the EN 50128 standard

Easy to operate and maintain

  • No need to write dedicated programs anymore
  • Easy allocation of independent tasks to users
  • Compatibility, via plug-in, with any configuration data format (XML and Microsoft Office Excel available by default)
  • Automatic generation of validation reports
  • Counterexample analysis
  • Standard environment based on the Eclipse platform

Standard compliance

Formal validation of configuration data is recommended by some safety standards and is an integral part of the system or software validation process.
OVADO is certified T2 SIL4. It fully complies with the requirements of the EN50128 standard.

Use case

RATP started the development of the tool in 2008, and is using it since.
OVADO® has been used by RATP in double-checking activities for Paris subway lines L1, L3, L5 and L9. The OVADO, T2 SIL4 certified version, has been successfully used by Systerel for validating L13 data. Originally designed for the railway sector, this tool suits industrial projects in various sectors such as aeronautics, space, defense, automotive, health or bank sectors.

How to get OVADO2?

OVADO is a RATP tool distributed and partly designed by Systerel.
To get more information on how to get OVADO, please contact us at or contact Systerel.


OVADO is based on open source software, most notably the Eclipse and Rodin platforms, without which its development would not have been possible. We would like to thank here all the contributors to OVADO.

©2012, 2016 Systerel. Last update on 2016-09-05.