​
OVADO
OVADO in english OVADO en français

Validate
software & system
critical configuration data

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

Why use OVADO2®? 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.

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 generation of configuration data

In order to gain in quality and development time, OVADO2® can now generate data using a formal model. With the appropriate process, it is possible to use OVADO2® at a T3 level for SIL4 and thus gain in quality, time and cost for data production. Indeed, a significant factorization of modelling work between the validation and generation activities allows to quickly converge towards valid data at the smaller expense of reinforced verification of this factorization.



Back to top

OVADO2®, a Tool Offering High Performances

Features

  • Ability to generate data from a formal model
  • Formal verification that data comply with their requirements
  • Exhaustive production of counterexamples for each elementary cause of non-compliance with a requirement
  • Interactive evaluation of expressions used during requirements modeling and counterexamples analysis


Costs Reduction and Shorter Generation and Validation Time

  • Expressiveness of the OVADO2® language
  • 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 unambiguous 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
  • OVADO2® is qualified for T2 SIL4 use according to the EN 50128:2011 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.
OVADO2® is qualified for T2 SIL4 use. It fully complies with the requirements of the EN 50128:2011 standard.

OVADO2® can be used as a T3 tool for SIL4 with the appropriate process.



Back to top

Use Case

OVADO® has been used by RATP in double-checking activities for Paris subway lines L1, L3, L4, L5, L6, L9, L10, L14, etc. The OVADO2® version, qualified for use as T2 SIL4, has been used successfully by Systerel for validating Paris L13 data.

It was used to generate and validate data for ALSTOM for Paris subway lines L6 and L10.

Originally designed for the railway sector, this tool suits industrial projects using configuration data. It may be used in various sectors such as the aeronautics, space, defense, automotive, health or bank sectors.

They Trust Us

Among all companies trusting us we can name: ALSTOM, CNES, THALES, etc.



Back to top

How to Get OVADO2®?

OVADO2® is a RATP tool distributed and partly designed by Systerel.
To get more information on how to get OVADO2®, please contact us by mail at ovado@systerel.fr or via the contact form.



Back to top

Acknowledgements

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®.