Intégration des techniques de vérification ...
Document type :
Thèse
Title :
Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande : application aux architectures SCADA
English title :
Integration of formal verification techniques into a control-command system design approach : application to SCADA architectures
Author(s) :
Kesraoui, Soraya [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance [Lab-STICC]
Institut de Recherche en Informatique et Systèmes Aléatoires [IRISA]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance [Lab-STICC]
Institut de Recherche en Informatique et Systèmes Aléatoires [IRISA]
Thesis director(s) :
Pascal Berruet
Flavio Oquendo
Armand Abdoul Karim Toguyeni
Flavio Oquendo
Armand Abdoul Karim Toguyeni
Defence date :
2017-05-11
Jury president :
Yamine Aït-Ameur [Président]
Christophe Kolski [Rapporteur]
Olivier-Henri Roux [Rapporteur]
Pascale Marangé
Christophe Kolski [Rapporteur]
Olivier-Henri Roux [Rapporteur]
Pascale Marangé
Jury member(s) :
Yamine Aït-Ameur [Président]
Christophe Kolski [Rapporteur]
Olivier-Henri Roux [Rapporteur]
Pascale Marangé
Christophe Kolski [Rapporteur]
Olivier-Henri Roux [Rapporteur]
Pascale Marangé
Accredited body :
Université de Bretagne Sud
Doctoral school :
École doctorale Santé, information-communication et mathématiques, matière (Brest, Finistère)
NNT :
2017LORIS442
Keyword(s) :
Contrôle commande
Spécification
Modélisation
Vérification formelle
Style architectural
Idm
Alloy
Automates temporisés
Ctl
Revue systématique
Spécification
Modélisation
Vérification formelle
Style architectural
Idm
Alloy
Automates temporisés
Ctl
Revue systématique
English keyword(s) :
Control-Command
Specification
Modeling
Formal verification
Architectural style
Mde
Alloy
Timed automata
Ctl
Systematic mapping
Specification
Modeling
Formal verification
Architectural style
Mde
Alloy
Timed automata
Ctl
Systematic mapping
HAL domain(s) :
Sciences de l'ingénieur [physics]/Automatique / Robotique
French abstract :
La conception des systèmes de contrôle-commande souffre souvent des problèmes de communication et d’interprétation des spécifications entre les différents intervenants provenant souvent de domaines techniques très variés. ...
Show more >La conception des systèmes de contrôle-commande souffre souvent des problèmes de communication et d’interprétation des spécifications entre les différents intervenants provenant souvent de domaines techniques très variés. Afin de cadrer la conception de ces systèmes, plusieurs démarches ont été proposées dans la littérature. Parmi elles, la démarche dite mixte (ascendante/descendante), qui voit la conception réalisée en deux phases. Dans la première phase (ascendante), un modèle du système est défini à partir d’un ensemble de composants standardisés. Ce modèle subit, dans la deuxième phase (descendante), plusieurs raffinages et transformations pour obtenir des modèles plus concrets (codes,applicatifs, etc.). Afin de garantir la qualité des systèmes conçus par cette démarche, nous proposons dans cette thèse, deux approches de vérification formelle basées sur le Model-Checking. La première approche porte sur la vérification des composants standardisés et permet la vérification d’une chaîne de contrôle-commande élémentaire complète. La deuxième approche consiste en la vérification des modèles d’architecture (P&ID) utilisés pour la génération des programmes de contrôle-commande. Cette dernière est basée sur la définition d’un style architectural en Alloy pour la norme ANSI/ISA-5.1. Pour supporter les deux approches, deux flots de vérification formelle semi-automatisés basés sur les concepts de l’IDM ont été proposés. L’intégration des méthodes formelles dans un contexte industriel est facilitée, ainsi, par la génération automatique des modèles formels à partir des modèles de conception maîtrisés par les concepteurs métiers. Nos deux approches ont été validées sur un cas industriel concret concernant un système de gestion de fluide embarqué dans un navire.Show less >
Show more >La conception des systèmes de contrôle-commande souffre souvent des problèmes de communication et d’interprétation des spécifications entre les différents intervenants provenant souvent de domaines techniques très variés. Afin de cadrer la conception de ces systèmes, plusieurs démarches ont été proposées dans la littérature. Parmi elles, la démarche dite mixte (ascendante/descendante), qui voit la conception réalisée en deux phases. Dans la première phase (ascendante), un modèle du système est défini à partir d’un ensemble de composants standardisés. Ce modèle subit, dans la deuxième phase (descendante), plusieurs raffinages et transformations pour obtenir des modèles plus concrets (codes,applicatifs, etc.). Afin de garantir la qualité des systèmes conçus par cette démarche, nous proposons dans cette thèse, deux approches de vérification formelle basées sur le Model-Checking. La première approche porte sur la vérification des composants standardisés et permet la vérification d’une chaîne de contrôle-commande élémentaire complète. La deuxième approche consiste en la vérification des modèles d’architecture (P&ID) utilisés pour la génération des programmes de contrôle-commande. Cette dernière est basée sur la définition d’un style architectural en Alloy pour la norme ANSI/ISA-5.1. Pour supporter les deux approches, deux flots de vérification formelle semi-automatisés basés sur les concepts de l’IDM ont été proposés. L’intégration des méthodes formelles dans un contexte industriel est facilitée, ainsi, par la génération automatique des modèles formels à partir des modèles de conception maîtrisés par les concepteurs métiers. Nos deux approches ont été validées sur un cas industriel concret concernant un système de gestion de fluide embarqué dans un navire.Show less >
English abstract : [en]
The design of control-command systems often suffers from problems of communication and interpretation of specifications between the various designers, frequently coming from a wide range of technical fields. In order to ...
Show more >The design of control-command systems often suffers from problems of communication and interpretation of specifications between the various designers, frequently coming from a wide range of technical fields. In order to address the design of these systems, several methods have been proposed in the literature. Among them, the so-called mixed method (bottom-up/top-down), which sees the design realized in two steps. In the first step (bottom-up), a model of the system is defined from a set of standardized components. This model undergoes, in the second (top-down) step, several refinements and transformations to obtain more concrete models (codes, applications, etc.). To guarantee the quality of the systems designed according to this method, we propose two formal verification approaches,based on Model-Checking, in this thesis. The first approach concerns the verification of standardized components and allows the verification of a complete elementary control-command chain. The second one consists in verifying the model of architecture (P&ID) used for the generation of control programs.The latter is based on the definition of an architectural style in Alloy for the ANSI/ISA-5.1 standard. To support both approaches, two formal semi-automated verification flows based on Model-Driven Engineering have been proposed. This integration of formal methods in an industrial context is facilitated by the automatic generation of formal models from design models carried out by business designers. Our two approaches have been validated on a concrete industrial case of a fluid management system embedded in a ship.Show less >
Show more >The design of control-command systems often suffers from problems of communication and interpretation of specifications between the various designers, frequently coming from a wide range of technical fields. In order to address the design of these systems, several methods have been proposed in the literature. Among them, the so-called mixed method (bottom-up/top-down), which sees the design realized in two steps. In the first step (bottom-up), a model of the system is defined from a set of standardized components. This model undergoes, in the second (top-down) step, several refinements and transformations to obtain more concrete models (codes, applications, etc.). To guarantee the quality of the systems designed according to this method, we propose two formal verification approaches,based on Model-Checking, in this thesis. The first approach concerns the verification of standardized components and allows the verification of a complete elementary control-command chain. The second one consists in verifying the model of architecture (P&ID) used for the generation of control programs.The latter is based on the definition of an architectural style in Alloy for the ANSI/ISA-5.1 standard. To support both approaches, two formal semi-automated verification flows based on Model-Driven Engineering have been proposed. This integration of formal methods in an industrial context is facilitated by the automatic generation of formal models from design models carried out by business designers. Our two approaches have been validated on a concrete industrial case of a fluid management system embedded in a ship.Show less >
Language :
Français
Collections :
Source :
Files
- https://tel.archives-ouvertes.fr/tel-01738049/document
- Open access
- Access the document
- https://tel.archives-ouvertes.fr/tel-01738049/document
- Open access
- Access the document
- https://tel.archives-ouvertes.fr/tel-01738049/document
- Open access
- Access the document
- document
- Open access
- Access the document
- 2017theseMesliS2.pdf
- Open access
- Access the document