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.
OVADO2® 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, OVADO2® checks automatically data conformity. The non-compliance of a data set is characterized by the extraction of counterexamples.
Formal validation of configuration data is recommended by some safety standards and is an integral part of the system or software validation process.
OVADO2® is certified T2 SIL4. It fully complies with the requirements of the EN50128 standard.
OVADO® has been used by RATP in
double-checking activities for Paris subway lines L1, L3, L4, L5, L6,
L9, L14, etc. The OVADO2® version, T2 SIL4
certified, has been used successfully by Systerel for validating Paris
Originally designed for the railway sector, this tool suits industrial projects in various sectors such as the aeronautics, space, defense, automotive, health or bank sectors.
They trust us: ALSTOM, CNES, THALES...
OVADO2® is based on open source software, most notably the Eclipse and Rodin platforms, without
which its development would not have been possible.
OVADO2® is also based on the ProB model checker.
We would like to thank here all the contributors to OVADO2®.