Validez formellement les données de configuration de logiciels et systèmes

OVADO est un outil RATP qualifié et extensible, dédié à la validation formelle des données de configuration des logiciels et systèmes.

Pourquoi utiliser OVADO ? Acheter
OVADO - Outil de VAlidation des DOnnées

Validation automatique des données critiques de configuration

Les systèmes critiques sont des systèmes complexes devenus aujourd’hui de plus en plus paramétrables. Garantir leur comportement et leur niveau de sécurité impose alors de valider la cohérence et la consistance de plusieurs centaines de milliers de données de configuration. Ces activités de validation, particulièrement fastidieuses et onéreuses, sont réalisées le plus souvent sous fortes contraintes de planning, car menées en phase finale de développement.

OVADO offre une réponse innovante à la problématique de vérification de données de configuration d’un système ou logiciel reposant sur la séparation de l'outil de validation des propriétés à valider.

L'équipe de modélisation formalise de façon non ambiguë les propriétés identifiées par les experts métier.

OVADO vérifie alors automatiquement que les données en entrée satisfont ces propriétés. La non-conformité d’un jeu de données est caractérisée par l’extraction d’un contre-exemple.

Génération formelle de données de configuration

Afin de gagner en qualité et en temps de développement, OVADO permet maintenant de générer les données à l'aide d'un modèle formel. Avec le processus adapté, il est possible d'utiliser OVADO à un niveau T3 pour du SIL4 et ainsi de gagner en qualité, en délai et en coût de production des données. En effet, une factorisation importante de travaux de modélisation entre les activités de validation et les activités de génération permet de converger rapidement vers des données valides moyennant un renforcement de la vérification de cette factorisation.


OVADO, un outil offrant de hautes performances

Fonctionnalités

  • Possibilité de génération des données à partir d'un modèle formel
  • Vérification formelle des données vis-à-vis des exigences
  • Production exhaustive des contre-exemples pour chaque cause élémentaire de non-respect d'une exigence
  • Évaluation interactive d'expressions pour la mise au point de la modélisation des exigences et l'analyse des contre-exemples


Réduction des coûts et du temps de génération et validation

  • Expressivité du langage d'OVADO
  • Capitalisation des propriétés d'un projet à un autre
  • Absence de requalification de l'outil de validation
  • Réduction notable du délai et du coût de constitution d'un dossier de sécurité et de son approbation par un EOQA
  • Rejeu de validation facile et rapide pour chaque nouvelle version de données

Amélioration de la qualité de la validation

  • Langage commun, non ambigu, entre experts métier et modélisateurs
  • Démonstration mathématique exhaustive du respect des propriétés par les données de configuration
  • Lisibilité et traçabilité des activités de validation
  • Validation double chaîne des données
  • OVADO est qualifié T2 SIL4 selon la norme EN 50128:2011


Facilité d'utilisation et de maintenance

  • Concept de propriétés dispensant d’écrire un programme
  • Distribution facilitée des tâches entre les utilisateurs
  • Compatibilité, par plug-in, avec tous formats de données de configuration (par défaut : XML et Microsoft Office Excel)
  • Production automatique des rapports de validation
  • Analyse de contre-exemples
  • Environnement standard basé sur la plate-forme Eclipse


Conformité aux normes

La validation formelle des données de configuration est recommandée par certaines normes de sécurité et fait partie intégrante du processus de validation du système ou logiciel considéré.

OVADO est qualifié pour une utilisation T2 SIL4. Il est ainsi entièrement conforme aux exigences de la norme EN 50128:2011 applicables à cette catégorie d’outils dans le domaine ferroviaire.

OVADO est utilisable comme outil de classe T3 pour du SIL4 avec le processus approprié.




Applications industrielles

L’outil OVADO a été utilisé par la RATP pour des activités de second regard sur les lignes L1, L3, L4, L5, L6, L9, L10, L14 du métro parisien. Sa version OVADO, qualifiée T2 SIL4, a été utilisée avec succès par Systerel sur la validation des données de la ligne 13.

Il a été utilisé pour générer pour ALSTOM les données des lignes L6 et L10 du métro parisien.

Conçu initialement pour le domaine ferroviaire, cet outil est adapté à différents types de projets industriels faisant intervenir des données de paramétrage ou de configuration. Il peut être utilisé dans des secteurs d’activité variés tels que l’aéronautique, le spatial, l’automobile, le médical ou le bancaire.

Ils nous font confiance

Parmi les sociétés qui nous font confiance, on compte : ALSTOM, Le CNES, THALES, etc.




Comment obtenir OVADO?

OVADO est un outil RATP partiellement développé et commercialisé par Systerel.

Pour plus d'information sur l'obtention d'une licence d'utilisation d'OVADO, merci de contacter Systerel par mail : ovado@systerel.fr ou via le formulaire de contact.




Remerciements

OVADO est basé sur des composants logiciels open-source, plus particulièrement sur la plate-forme Eclipse et le langage supporté par l'outil Rodin, sans lesquels son développement n’aurait pas été possible.

OVADO est également basé sur le model checker ProB.

Nous souhaitons remercier tous ceux qui ont participé à l’élaboration de ces composants d’OVADO.