Méthode de validation formelle d’un poste d’aiguillage informatique

Dans cet article, nous verrons comment répondre à la problématique suivante : les vérifications et essais avant la mise en service d’équipements critiques sont essentiels, leur durée et efficacité ne sont pas prévisibles. Les contraintes économiques et la complexité croissante liée au développement d’outils informatisés tendent à limiter l’efficacité des méthodes actuelles d’approbation. Dans la pratique, il apparaît une réduction du taux de couverture des essais et la survenue de nombreux incidents contraires à la sécurité constatés au cours des essais finaux ou après la mise en exploitation. La méthode présentée permet de valider formellement les nouveaux postes d’aiguillage informatisés français. Ceux-ci interprètent en temps réel des réseaux de Petri particuliers décrivant les fonctionnalités de signalisation. Le but de notre projet interne était de définir une méthode opérationnelle de validation formelle des postes d’aiguillage informatiques. C’est une méthode formelle de preuve par induction qui couvre les spécifications fonctionnelles et leur implémentation. Avec la méthode proposée et ses outils associés, nous vérifions exhaustivement que le système vérifie en permanence les propriétés de sûreté identifiées à sa conception et ne révèle pas dans sa réalisation de conditions superflues : il remplace ainsi tous les essais antérieurs et est inclus dans les procédures actuelles. Les avantages sont une réduction significative du temps d’essai et des coûts associés, une augmentation du taux de couverture (maintien de la sécurité déterministe vs une sécurité probabiliste), une réponse aux demandes d’évolutions fonctionnelles des postes à réaliser et valider par les équipes de maintenance. La maîtrise de ces méthodes par les ingénieurs en signalisation du gestionnaire d’infrastructure est sûrement une clé pour montrer, d’une part, qu’accroître le niveau de sécurité ne se traduit pas nécessairement par une augmentation de l’effort financier. D’autre part, il est possible de clarifier les responsabilités entre Industriel (Comment faire ?) et Gestionnnaire de l’Infrastructure (Pourquoi et Quoi faire ?).