Cette thèse contribue à une approche formelle de conception d'un programme de contrôle/commande pour les systèmes automatisés de production (SAP) contrôlés par des automates programmables industriels (API). Dans ce contexte, deux constats principaux ont été soulevés : il existe manque de méthodologie efficace pour la conception d'un programme API dans le monde industriel et les méthodes formelles issues du monde académique ne sont ni connues ni utilisées par l'industrie car trop complexes. Par ailleurs, l'industrie du futur nécessitera des contrôleurs toujours plus flexibles et fiables. La flexibilité implique que les programmes seront encore plus difficiles à réaliser, et par conséquent, la difficulté pour garantir la fiabilité de ceux-ci sera accrue.Pour répondre à ces problématiques, une méthode de conception formelle s'intégrant dans un cycle de développement industriel classique (cycle en V) a été proposée. De plus, afin de faciliter le transfert vers l'industrie tant d'un point de vue technique (API) qu’humain (pratique des automaticiens), le formalisme utilisé est entièrement basé sur des variables et des équations logiques appelées contraintes logiques. Ces contraintes logiques permettent la spécification des exigences informelles recensées dans le cahier des charges. A partir de ces contraintes logiques, un algorithme de résolution des contraintes, implémentable dans un API, est synthétisé et implémenté automatiquement dans un langage de programmation normalisé pour API. Ce filtre logique peut être utilisé pour : commander un SAP contrôlé par un API, vérifier formellement un programme API, mettre en sécurité un programme API déjà existant présentant des erreurs.Les travaux de cette thèse ont eu pour objectif de lever certains verrous et de globalement améliorer et renforcer l'approche par filtre logique. Dans le but de généraliser l'approche par filtre, un effort important a été réalisé autour de la formalisation des contraintes logiques et des différentes fonctions et propriétés associées au filtre logique. Cet apport de formalisation a permis, en particulier, de proposer une approche de vérification formelle de la notion de cohérence d'un filtre logique ainsi qu'une condition nécessaire et suffisante à cette propriété. Enfin, après avoir mis à jour l'algorithme d'implémentation classique, deux algorithmes de recherche locale d'une solution basés sur des techniques de solveur SAT ont été proposés. / This thesis contributes to a formal approach to design control/command program for automated production systems controlled by Programmable Logical Controller (PLC). In this context, two main observations have been highlighted: there is a lack of efficient methodology for the design of PLC program in the industrial field and the academicals formal approaches are neither known nor used in manufacturing industry due to high complexity. Furthermore, the industry of future will require flexible and reliable PLC program. The flexibility implies that programs will be even more difficult to design and, consequently, the complexity to guarantee the reliability will be increased.To address these issues, a formal design approach, presented as a classical V-cycle, have been proposed. Moreover, to facilitate the industrial transfer from both technical (PLC) and human (engineer practice) point of view, the formalism is exclusively based on logical variables and equations called logical constraints. These constraints are used to specify the informal requirements described in the specification book. From these constraints, a logical filter is synthesized automatically and a solving algorithm, IEC 61131-3 compliant, is implemented in the PLC program. This logical filter may be used to: command an automated production system controlled by a PLC, verify formally a PLC program, and make safe an existing PLC program containing errors.The contributions of this thesis covered the whole development cycle: formal specification, formal analysis and synthesis, automatic implementation in a PLC program. To support these contributions, a significant effort was made on the formalism based on logical constraints. This new formalism has allowed, in particular, to propose a necessary and sufficient condition to the coherence property of a logical filter and to guarantee the convergence of the online solving algorithm. At least, the classical solving algorithm has been updated according to the new formalism, and two algorithms based on SAT solver techniques and local research have been proposed and tested on real PLC.

La SNCF cherche à mettre en place des solutions innovantes permettant d’améliorer la sécurité et les conditions de travail des chargés d’études lors des travaux d’automatisation. En partant de l’étude théorique du projet jusqu’à sa validation sur site, en passant par la mise en œuvre des programmes, du câblage des armoires, et de leur vérification sur plateforme et en usine, ces différentes tâches s’avèrent souvent être longues, complexes, et répétitives, ce qui a pour effet d’augmenter la charge de travail des chargés d’études. En vue d’améliorer les conditions de travail des chargés d’études, ce projet de recherche vise principalement à améliorer leurs méthodologies de vérification des programmes API (aspects fonctionnels et sécuritaires) et du câblage des armoires électriques. Ce projet intitulé « Vérification formelle et simulation pour la validation des programmes API des EALE » se décompose en deux axes :  la vérification hors ligne des programmes API : basée sur une approche formelle, la méthode s’appuie sur une modélisation de l’installation électrique, des programmes API et du cahier de recette dans le model-checker Uppaal. Le principe consiste à vérifier automatiquement si les programmes satisfont aux tests du cahier de recette.  la vérification en ligne du câblage des armoires de contrôle/commande/ protection grâce à un simulateur de partie opérative interfacé avec les armoires de contrôle/commande/protection (via une armoire de test). La vérification se fera de manière automatique et en ligne, toujours avec les tests du cahier de recette, et permettra de valider le câblage des armoires et les réglages des appareils de protection numérique. / In order to keep its leadership in French rail market and to improve working conditions of its systems engineers during automation projects, the SNCF (French acronym for National Society of French Railways) wants to develop solutions increasing the productivity. One of these improvements focuses on the current methodology used by the systems engineers to verify and validate the control command system of electrical installations. This task remains one of the most important during an automation project because it is supposed to ensure installations safety, but it should be optimized. Through an industrial thesis financed by SNCF, the aim of this research project is to improve this method and reduce time validation of control command system by providing tools which will help systems engineers to verify and validate quickly and automatically the control command system during any automation project. It is composed of two axes : - Offline verification of PLC programs with model checking - Online validation of electrical cabinets with virtual commissioning

Les travaux présentés dans ce mémoire de thèse s'intéressent à la génération et à la mise en œuvre de séquences de test pour le test de conformité de contrôleurs logiques. Dans le cadre de ces travaux, le Grafcet (IEC 60848 (2002)), langage de spécification graphique utilisé dans un contexte industriel, a été retenu comme modèle de spécification. Les contrôleurs logiques principalement considérés dans ces travaux sont les automates programmables industriels (API). Afin de valider la mise en œuvre du test de conformité pour des systèmes de contrôle/commande critiques, les travaux présentés proposent: - Une formalisation du langage de spécification Grafcet. En effet, l'application des méthodes usuelles de vérification et de validation nécessitent la connaissance du comportement à partir de modèles formels. Cependant, dans un contexte industriel, les modèles utilisés pour la description des spécifications fonctionnelles sont choisis en fonction de leur pouvoir d'expression et de leur facilité d'utilisation, mais ne disposent que rarement d'une sémantique formelle. - Une étude de la mise en œuvre de séquences de test et l'analyse des verdicts obtenus lors du changement simultané de plusieurs entrées logiques. Une campagne d'expérimentation a permis de quantifier, pour différentes configurations de l'implantation, le taux de verdicts erronés dus à ces changements simultanés. - Une définition du critère de SIC-testabilité d'une implantation. Ce critère, déterminé à partir de la spécification Grafcet, définit l'aptitude d'une implantation à être testée sans erreur de verdict. La génération automatique de séquences de test minimisant le risque de verdict erroné est ensuite étudiée.

Les travaux présentés dans ce mémoire de thèse s'intéressent à la validation fonctionnelle de contrôleurs logiques par des techniques de test de conformité et de validation en boucle fermée. Le modèle de spécification est décrit dans le langage industriel Grafcet et le contrôleur logique est supposé être un automate programmable industriel (API) mono-tâche. Afin de contribuer à ces techniques de validation fonctionnelle, ces travaux présentent : - Une extension d'une méthode de formalisation du Grafcet par traduction sous la forme d'une machine de Mealy. Cette extension permet de produire un modèle formel de la spécification lorsque le Grafcet est implanté selon un mode d'interprétation sans recherche de stabilité, qui n'est pas préconisé dans la norme IEC 60848 mais largement utilisé dans les applications industrielles. - Une contribution au test de conformité par la définition d'un ensemble de relations de conformité basées sur l'observation de plusieurs cycles d'exécution pour chaque pas de test. - Une contribution à la validation en boucle fermée par la définition d'un critère de fin d'observation et par une technique d'identification en boite grise pour la construction et l'analyse du système en boucle fermée. / The results presented in this PhD thesis deal with functional validation of logic controllers using conformance test and closed-loop validation techniques. The specification model is written in the Grafcet language and the logic controller is assumed to be a Programmable Logic Controller (PLC). In order to contribute to these validation techniques, this thesis presents: - An axtension to a fomalization methods for Grafcet languages by translation to a Mealy machine. This extension generates a formal model of a Grafcet specification that is interpreted without search of stability. This mode of interpretation is not recommended by the standard IEC 60848 but is widely used in industrial applications. - A contribution to conformance test by a definition of a set of conformance relation based on the observation of several execution cycles for each test step. - A contribution to closed-loop validation by the definition of a termination criterion and by a new gray-box identification technique that is used for construction and analysis of the closed-loop system.

Les travaux présentés dans ce mémoire de thèse s'intéressent à la génération et à la mise en œuvre de séquences de test pour le test de conformité de contrôleurs logiques. Dans le cadre de ces travaux, le Grafcet (IEC 60848 (2002)), langage de spécification graphique utilisé dans un contexte industriel, a été retenu comme modèle de spécification. Les contrôleurs logiques principalement considérés dans ces travaux sont les automates programmables industriels (API). Afin de valider la mise en œuvre du test de conformité pour des systèmes de contrôle/commande critiques, les travaux présentés proposent: - Une formalisation du langage de spécification Grafcet. En effet, l'application des méthodes usuelles de vérification et de validation nécessitent la connaissance du comportement à partir de modèles formels. Cependant, dans un contexte industriel, les modèles utilisés pour la description des spécifications fonctionnelles sont choisis en fonction de leur pouvoir d'expression et de leur facilité d'utilisation, mais ne disposent que rarement d'une sémantique formelle. - Une étude de la mise en œuvre de séquences de test et l'analyse des verdicts obtenus lors du changement simultané de plusieurs entrées logiques. Une campagne d'expérimentation a permis de quantifier, pour différentes configurations de l'implantation, le taux de verdicts erronés dus à ces changements simultanés. - Une définition du critère de SIC-testabilité d'une implantation. Ce critère, déterminé à partir de la spécification Grafcet, définit l'aptitude d'une implantation à être testée sans erreur de verdict. La génération automatique de séquences de test minimisant le risque de verdict erroné est ensuite étudiée. / The works presented in this PhD thesis deal with the generation and implementation of test sequences for conformance test of logic controllers. Within these works, Grafcet (IEC 60848 (2002)), graphical specification language used in industry, has been selected as the specification model. Logic controllers mainly considered in these works are Programmable Logic Controllers (PLC). In order to validate the carrying out of conformance test of critical control systems, this thesis presents: - A formalization of the Grafcet specification language. Indeed, to apply usual verification and validation methods, the behavior is required to be expressed through formal models. However, in industry, the models used to describe functional specifications are chosen for their expression power and usability, but these models rarely have a formal semantics. - A study of test sequences execution and analysis of obtained verdicts when several logical inputs are changed simultaneously. Series of experimentation have permitted to quantify, for different configurations of the implantation under test, the rate of erroneous verdicts due to these simultaneous changes. - A definition of the SIC-testability criterion for an implantation. This criterion, determined on the Grafect specification defines the ability of an implementation to be tested without any erroneous verdict. Automatic generation of test sequences that minimize the risk of erroneous verdict is then studied.