Validation formelle de données

Dans le monde du ferroviaire, les logiciels critiques pour la sécurité sont développés et validés indépendamment des données qui les paramètrent.

CLEARSY Data Solver

Par exemple, la topologie de la voie, les positions des signaux et des aiguilles, les points kilométriques, sont des données constantes utilisées par un pilote automatique pour calculer les courbes de freinage et déterminer à quel moment déclencher le frein d’urgence.

• Télécharger la plaquette CLEARSY Data Solver

Ainsi, chaque partie doit être sûre au même niveau selon l’EN 50128 : SIL4.

Le processus de validation des données consiste à s’assurer que l’ensemble de données respecte ses propriétés et toutes les règles de génération. Auparavant, le processus de validation manuelle des données était entièrement humain, menant à des activités à longues et douloureuses, sujettes aux erreurs.

Validation formelle des données

La validation formelle des données est l’évolution naturelle de ce processus humain en un processus plus sécurisé. CLEARSY a inventé cette approche grâce à ses connaissances et compétences approfondies sur la technologie des méthodes formelles et les outils associés.

https://youtu.be/sDbnODvnyDI

Outil de validation de données

CLEARSY fournit un outil de validation de données et ses services associés. Les bénéfices de cette approche formelle sont variés :

• Rapidité : jusqu’à 10 fois plus vite qu’une vérification purement humaine, seules quelques heures suffisent pour valider un projet ferroviaire complet
• Automatique, exhaustif, presse bouton et répétable à l’envie (évite les activités de non régression fastidieuse)
• Supprime les erreurs humaines, en utilisant les méthodes formelles et des techniques certifiées.
• Permet une forte réutilisation des règles d’un projet à l’autre (capitalisation des connaissances).
• Vise principalement les projets ferroviaires types : CBTC, ERTMS, RBC, ATS.

Description du produit

Un outil sur mesure

• Adapté aux formats de données des clients (xml, xls, parameter file, railML, csv, txt …).
• Format des rapports de vérification adapté au processus client.
• Peut être utilisé par le client final.

Un service de développement des règles de vérification formelle

L’outil est un solver qui va vérifier règle par règle les propriétés pour les données concernées. Ces règles peuvent être développées par le client ou par CLEARSY. Le service proposé est le suivant :

• Modélisation du modèle formel contenant les propriétés que les données doivent respecter.
• Ces modèles sont facilement lisibles après une formation.
• Les règles appartiennent ensuite au client qui peut donc les réutiliser autant que souhaité sur les différentes itérations d’un projet ou sur d’autres projets.

Le client final peut également spécifier ses propres règles et utiliser l’outil.

Références commerciales

Les clients sont les grand industriels ou les donneurs d’ordre du marché ferroviaire.