La méthode formelle pour valider des données de paramétrage : CLEARSY est choisie

Formal methods for validating parameterization
17 janvier 2020

Pour valider les données qui paramètrent son système d’enclenchement ferroviaire, CLEARSY est choisie pour l’infaillibilité de son approche basée sur les méthodes formelles.

Une grande société a confié à CLEARSY la validation des données du système de pilotage des aiguilles, le système d’enclenchement. L’objectif est la certification SIL4 (niveau maximum de sécurité de la norme CENELEC EN 50128). La solution d’enclenchement proposée par la société est générique et demande à être paramétrée. La validation rigoureuse des données du paramétrage est un des aspects exigés par la certification.

La validation basée sur les méthodes formelles propose une logique nouvelle, fondée sur les mathématiques, qui a pour avantage de lever toutes les ambiguïtés quant à l’interprétation des données et des propriétés qu’elles doivent respecter, précise Erwan Mottin qui dirige l’activité validation de données chez CLEARSY. En d’autres termes, la validation formelle garantit la conformité des paramétrages avec les niveaux de sûreté de fonctionnement exigé par la norme, dans ce dossier. Pour atteindre ces objectifs de sécurité, CLEARSY s’appuie d’une part sur un outil informatique certifié – le CLEARSY Data Solveur – et d’autre part, sur des règles de vérification développées en utilisant les méthodes formelles.

Editeur de l’Atelier B, depuis 2001, CLEARSY a développé le 1er outil de validation formelle de données en 2005 en réponse à une commande de la RATP. Depuis, ATOS, SNCF, Siemens, Alstom, et Thales font appel à ses services. Dans le cadre de ce contrat, CLEARSY préparera l’outillage nécessaire et les pièces du dossier nécessaire au processus de validation SIL 4. La livraison est prévue à l’automne.