Contexte global : Dans le domaine industriel, les systèmes de contrôle commande (SCC) sont aujourd’hui présents dans toutes les lignes de production automatisée.  Toutefois, leur sûreté de fonctionnement  doit être garantie afin d’éviter des disfonctionnements pouvant compromettre la sécurité des personnes et des biens. Vérifier la sûreté de ces SCC consiste à vérifier (1) les programmes automates et (2) le câblage des armoires électriques. Comme dans la plupart des industriels, la vérification de (1) et (2) à la SNCF se fait simultanément en usine, au travers des procédures de tests avec cahier de recettes.

 Problématique industrielle : Les méthodes de tests (comme les cahiers de recette) et de simulation permettent d’explorer qu’une partie des comportements possibles du système de contrôle commande. Elles ne sont donc pas exhaustives en plus d’être exposées aux erreurs humaines lors des essais pour des raisons de fatigue, de stress, et de surcharge mentale. Ces méthodes diffèrent en cela des techniques de vérification formelle qui permettent de vérifier de manière exhaustive la sûreté de fonctionnement d’un système en explorant la totalité de ses états atteignables.

 Objectif : Dans ce projet de recherche, nous proposons d’abord une approche méthodologique permettant de vérifier de manière exhaustive les systèmes de contrôle commande (appliquée aux installations électriques de la SNCF). Cette approche permet de vérifier dans un premier temps les programmes automates de manière exhaustive en utilisant les méthodes formelles (model-checking). De ce fait l’ingénieur pourra vérifier et valider ses programmes API dès leur conception. De plus lorsqu’un programme automate vérifié ne respecte pas les spécifications fonctionnelles et sécuritaires, il nous est possible de le rendre formellement sûr de fonctionnement grâce à l’implémentation d’un filtre logique de commande par contraintes, dont le rôle est d’interdire et de corriger toutes erreurs de commandes envoyées par l’opérateur. Après vérification formelle des programmes automates, la deuxième étape est basée sur l’utilisation du Virtual Commissioning et consiste à valider automatiquement les programmes (par simulation Software-In-the-Loop -SIL) et le câblage des armoires de contrôle commande (par simulation Hardware-In-the-Loop - HIL).

 Etat de l’art : Du fait de la non-exhaustivité des méthodes de tests et simulations, plusieurs travaux de recherche ont été effectués sur la vérification formelle des programmes automates. Ces méthodes nécessitent une modélisation de la partie opérative, des programmes automates (quel que soit le  langage de programmation : SFC, ST, LD, IL, FBD) et des propriétés à vérifier. Dans la littérature, des approches de modélisation (généralement en réseau de Petri, automates à états temporisés…) ont été proposées dans des travaux, et les méthodes formelles (telles que l’analyse statique, le model-checking…)  permettent d’en vérifier certaines propriétés. Toutefois la complexité de la modélisation atténue les performances des outils de vérification  et provoque souvent l’explosion combinatoire pendant la simulation. Nous proposons dans ce projet de recherche une approche de modélisation simplifiée des programmes automates (en SFC, LD, et ST) et de la partie opérative, pour avoir de meilleurs résultats de simulation comparés aux travaux existants. De plus ces méthodes de vérification formelles restent toujours très peu utilisées en industrie : d’où l’intérêt de les faire connaitre en montrant leur supériorité par rapport aux méthodes actuelles, et en particulier le cahier de recettes.

 Apport du travail : Comparé aux méthodes existantes dans l’industrie, notre approche de vérification est méthodologique et garantit formellement la sûreté de fonctionnement du système de contrôle commande. La vérification formelle et la validation des programmes automates dès leur conception permettent de faciliter la validation du câblage des armoires en usine. En effet, toute anomalie rencontrée lors des essais automatiques en usine (avec un simulateur HIL) provient nécessairement d’un mauvais câblage car les programmes ont déjà été formellement vérifiés et validés en amont. Ce qui n’est pas le cas des techniques actuellement utilisées à la SNCF, qui consistent à valider en même temps les programmes et le câblage, et dont le diagnostic des anomalies est moins évident. Parmi les autres avantages de cette approche, figurent également (a) un gain de temps lors de la vérification étant donné que celle-ci est automatisée, (b) une vérification plus exhaustive et fiable, (c) une augmentation de la robustesse du système face aux erreurs de commandes (grâce à un filtre logique de sécurité), (d) une augmentation du rendement et une réduction des pannes qui minimisera les pertes économiques.