La validation et la génération de données constantes sont devenus des thèmes importants dans le monde ferroviaire, pour démontrer la sécurité d’un système ferré.
Plusieurs travaux ont été menés dans ce domaine. On citera:
- le développement par RATP d’un outil de vérification de données ferroviaires, initialement développé autour du moteur de calcul de prédicats B, PredicateB, de l’animateur de modèles B évènementiel Brama, et complété par la suite par le model-checker ProB;
- les travaux de validation des données par Siemens Transportation Systems, durant le projet européen DEPLOY, en s’appuyant sur le model-checker ProB;
- la validation et la génération de données par Alstom Transportation Systems, en s’appuyant sur le model-checker ProB, conduisant à la création d’un nouveau type de projet Atelier B: validation/génération de données.
La validation de données constantes consiste à s’assurer que les données d’exploitation d’une ligne de métro telles que la topologie des voies, la position des équipements, etc. respectent un certain corpus de règles de signalisation. Ces données constantes, téléchargées in fine à bord d’équipements de sécurité tels que des pilotes automatiques, participent à la sécurité de l’ensemble et doivent donc être validées en conséquence. Cette validation a longtemps été manuelle, compte tenu de la grande quantité d’informations à manipuler (jusqu’à 100 000 informations élémentaires et plusieurs centaines de règles).
Les progrès réalisés par les model-checkers, et par ProB en particulier, ont permis la constitution de modèles de données, s’appuyant sur le langage mathématique de B, et leur vérification de larges ensembles de données vis à vis de ce modèle, ramenant le temps de vérification de plusieurs mois à quelques heures (hors temps de modélisation) avec un niveau de confiance dans les résultats obtenus bien supérieur.
D’un point de vue technique, le modèle de données et les valeurs à qualifier sont transformés en un modèle B qui est ensuite fourni à ProB, dans le but de:
- vérifier que les données sont compatible avec le modèle de données. En cas d’incompatibilité, ProB est à même de fournir tous les contre-exemples;
- générer certaines données, en cas d’instanciation partielle du modèle. Si certaines valeurs ne sont pas fournies, ProB est capable de déterminer leur valeur, si une solution existe.
La validation de données s’insère dans tout cycle de développement, y compris le cycle de développement formel B.