OVADO²® est un outil RATP qualifié et extensible, dédié à la validation formelle des données de configuration des logiciels et systèmes. L’article Generating and verifying configuration data with OVADO²® décrit une utilisation d’OVADO²® dans le cadre d’un projet SIL4 de génération formelle de données de configuration.

Cependant, cet outil est également utilisé dans des projets moins contraints tels que des activités de second regard. C’est dans ce cadre notamment que la RATP utilise OVADO²® pour de nombreuses lignes (L1, L3, L4, L5, L6, L9, L10, L11, L14) du métro parisien. Dans ce cadre, les données de configurations sont généralement appelées « invariants ».

Le second regard sur les invariants avec OVADO²®¶

Pour commencer les activités de second regard, le modélisateur reçoit les invariants à vérifier ainsi que leurs spécifications et les données ayant permis de les obtenir. À partir de ces données et des spécifications, l’ingénieur modélise les invariants et écrit les propriétés permettant de vérifier l’égalité entre les invariants fournis et modélisés.

OVADO²® vérifie ensuite automatiquement ces propriétés. Si ces dernières ne sont pas respectées, l’outil permet l’extraction semi-automatique de contre-exemples.

La modélisation dans OVADO²®¶

Un modèle OVADO²® est composé de plusieurs éléments, chacun associé à une notion qui lui est propre :

Les constantes qui servent d’interface avec les données (nom, type, accès à la donnée) ;
Les définitions qui regroupent les données calculées et les fonctions réutilisables (nom, expression B) ;
Les propriétés qui sont évaluées par OVADO²® (nom, prédicat B).

Les données¶

Il faut séparer deux types de données OVADO²® : les données permettant de calculer les invariants modélisés et les invariants à vérifier.

Les invariants à vérifier sont dans un document texte et ne doivent pas être modifiés par le modèle. Cette donnée d’entrée sera donc lue à travers une constante pour être directement utilisée dans la propriété correspondante (dans ce cas, une propriété d’égalité).

Exemple d’invariant à vérifier

Les données permettant le calcul peuvent être fournies sous la forme d’un fichier Excel qui contient les différents objets et leurs attributs.

Exemple de données permettant le calcul

Les constantes¶

Les constantes ont pour fonction de récupérer les données depuis un fichier (xml ou Excel). C’est également à cette étape que les données vont être typées.

Exemple de constantes récupérant les données d’un fichier Excel

Toute mise en forme des données telle qu’un changement d’unité se fera dans des définitions.

Les définitions¶

Les définitions regroupent les différentes étapes de modélisation et permettent de calculer l’invariant respectant les spécifications.

La première étape est de mettre en forme les données contenues dans les constantes pour les rendre plus facilement utilisables en associant les objets entre eux (une voie avec son point de début par exemple). Cette étape est surtout utile quand le modèle est assez complexe.

Exemple de fonctions mettant en forme les données

Ensuite, il est possible de définir l’invariant tout en suivant les spécifications. Dans notre exemple, la spécification demande que l’invariant associe la voie, représentée par son numéro sur la ligne, avec le PK du début de la voie (en cm) :

Plusieurs opérateurs B sont disponibles nativement dans OVADO²®. Il est par exemple possible de retrouver “;” pour la composition de fonctions, ou encore “~” pour la fonction inverse.

Les propriétés¶

Les propriétés sont des assertions logiques qu’OVADO²® va vérifier pour toutes les valeurs. Dans le cadre de ce type d’activités de second regard, il s’agit de vérifier l’égalité entre les deux invariants.

Vérification de l’égalité de deux invariants

Après vérification par OVADO²®, soit l’égalité est vérifiée (résultat en vert) et l’on passe à l’invariant suivant, soit il y a une différence et il faut analyser les contre-exemples (les valeurs qui diffèrent).

Après analyse, si la différence est une erreur de modélisation, il faut modifier le modèle pour pouvoir rejouer la propriété. Sinon, il faut discuter du problème avec le fournisseur de l’invariant.

Conclusion¶

Les activités de second regard sont nécessaires pour s’assurer de la sécurité et du bon fonctionnement du matériel roulant. Cependant, il s’agit d’une activité très couteuse en temps et en ressource. L’outil OVADO²® permet d’avoir un cadre formel qui facilite l’écriture de modèle de bonne qualité et l’analyse des erreurs dans les invariants fournis (grâce notamment à la génération semi-automatique des contre-exemples). Pour affiner les analyses, OVADO²® offre également une fenêtre d’évaluation qui permet de tester et d’observer n’importe quel invariant, définition intermédiaire et/ou constante.