Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

HAL Id: tel-01738049 https://tel.archives-ouvertes.fr/tel-01738049 Submitted on

HAL Id: tel-01738049 https://tel.archives-ouvertes.fr/tel-01738049 Submitted on 20 Mar 2018 HAL is a multi-disciplinary open access archive for the deposit and dissemination of sci- entific research documents, whether they are pub- lished or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers. L’archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d’enseignement et de recherche français ou étrangers, des laboratoires publics ou privés. Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande : application aux architectures SCADA Soraya Kesraoui To cite this version: Soraya Kesraoui. Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande : application aux architectures SCADA. Automatique / Robo- tique. Université de Bretagne Sud, 2017. Français. NNT : 2017LORIS442. tel-01738049 THESE / UNIVERSITE BRETAGNE SUD UFR Sciences et Sciences de l’Ingénieur sous le sceau de l’Université Bretagne Loire Pour obtenir le titre de : DOCTEUR DE L’UNIVERSITE BRETAGNE-SUD Mention : STIC Ecole Doctorale SICMA présentée par Soraya Mesli Kesraoui Préparée à l’unité mixte de recherche : Lab-STICC (UMR 6285), IRISA (UMR 6074), CRIStAL (UMR 9189) Établissement de rattachement : Université Bretagne Loire Intégration des techniques de vériﬁcation formelle dans une approche de conception des systèmes de contrôle-commande : Application aux architectures SCADA Thèse soutenue le 11 mai 2017 devant la commission d’examen composée de : M. Yamine Ait Ameur Professeur, IRIT (UMR 5505), École Nationale Supérieure d’électronique, d’électrotechnique, d’Informatique, d’Hydraulique et de Télécommunications / Président M. Christophe Kolski Professeur, LAMIH (UMR 8201), Université de Valenciennes et du Hainaut-Cambrésis / Rapporteur M. Olivier H. Roux Professeur, IRCCyN (UMR 6597), École Centrale de Nantes / Rapporteur Mme. Pascale Marangé Maître de Conférences, CRAN (UMR 7039), Université de Lorraine / Examinateur M. Pascal Berruet Professeur, Lab-STICC (UMR 6285), Université Bretagne Sud, Lorient / Directeur de thèse M. Armand Toguyeni Professeur, CRIStAL (UMR 9189), École centrale de Lille / Co-directeur M. Flavio Oquendo Professeur, IRISA (UMR 6074), Université Bretagne Sud, Vannes / Co-directeur M. Alain Bignon Docteur, Responsable R&I, Segula Technologies, Lanester / Responsable industriel CIFRE Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 "Je dédie cette thèse à mes chers parents." Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 Remerciements Ho que c’est difﬁcile d’écrire et de trouver les mots justes pour exprimer mes remercie- ments et ma gratitude envers celles et ceux qui m’ont soutenu durant ces trois années de thèse. Je remercie tout d’abord Alain BIGNON qui a cru en moi et qui m’a proposé ce sujet de thèse. Je te remercie aussi pour tes conseils, pour ton encadrement et surtout pour ton soutien jusqu’à la dernière minute. Tu resteras toujours "Mon meilleur chef!". Je remercie également messieurs Pascal BERRUET, Armand TOGUYENI et Flavio OQUENDO d’avoir accepté d’encadrer cette thèse. Travailler sous la direction de trois professeurs avec des contraintes de distance n’est pas toujours évident, mais vous avez su rendre ce travail agréable. Je vous remercie surtout pour l’intérêt que vous avez porté à mes travaux, pour le suivi, les conseils, votre disponibilité et aussi pour la bonne ambiance qui a rythmé nos réunions. Je souhaite remercier messieurs Christophe KOLSKI et Olivier H. ROUX d’avoir accepté de relire ces travaux. Je remercie également monsieur Yamine AIT AMEUR d’avoir accepté d’examiner et de présider le jury de cette thèse. Je remercie aussi madame Pascale MARANGE d’avoir bien voulu accepter la charge d’examinateur. Je tiens aussi à remercier le personnel des laboratoires lab-STICC et L’IRISA pour leur pro- fessionnalisme. Je n’oublie pas de remercier les doctorants du Lab-STICC (Amandine POR- CHER, Fanny GUENNOC, Rani KHAN, Thomas TOUBLANC) et de l’IRISA pour les dis- cussions très enrichissantes qu’on a pu avoir au cours de ces années de thèse. Je remercie également et chaleureusement mes collègues de Segula Technologies, surtout l’équipe du midi : Perine Le SENECHAL, Éric LE BRIS, Sophie PRAT, Laurianne BOULHIC, Olga GOUBALI, Nicolas AUFFRET, Davy RODIER et Fabien SILONE. Merci à Perine, Olga et Laurianne d’avoir relu et corrigé les chapitres de cette thèse. Merci à Eric d’avoir accepté de participer à mes multiples entretiens. Merci à vous tous pour les bons moments qu’on a pu partager. Je remercie aussi Raoul DJOUSSE, Landry RAHAMEFY et Franck NGANKAM d’avoir participé et contribué à mes travaux. Je tiens spécialement à remercier mes amies depuis toujours : Sonia, Farisa, Dihia, Nas- sima, Loulou et Kahina. Merci pour votre soutien et votre amitié. Cette thèse m’a aussi permis de rencontrer des personnes formidables comme Olga GOUBALI et Asma BENMESSAOUD GABIS. Je te remercie Olga pour ton soutien et d’avoir toujours cru en moi. Tu as toujours su me communiquer ta joie de vivre et ta bonne humeur dans les moments difﬁciles. Je te remer- cie Asma pour les bons moments passés ensemble et pour toutes les discussions imaginables et inimaginables qu’on a pu avoir. Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 1 Je remercie spécialement mes parents qui ont toujours étaient là pour moi et qui ont tou- jours cru en moi. Je remercie aussi mes frères et sœurs : Ouissem, Sabrina, Touﬁk et Cherif. Je tiens aussi à remercie mes beaux-parents de m’avoir considéré comme leur ﬁlle et de m’avoir toujours soutenue. Je remercie aussi Salim, Djamila et Zazi. Je n’oublie pas de remercier la personne qui m’a supporté durant ces trois années de thèse. Je te remercie Djamal d’être toujours à mes côtés et d’avoir supporté mes nombreuse crises de stresse et d’angoisse. Je suis convaincu que sans toi, cette thèse n’aura pas eu lieu. Merci ! Je remercie tous ceux qui ont contribué de prés ou de loin à cette thèse. Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 Cette thèse est le fruit d’une collaboration entre l’entreprise SEGULA Technologies, ac- teur majeur des métiers de l’ingénierie, et trois laboratoires de recherches : Le Lab-STICC, l’IRISA et CRIStAl. Le Lab-STICC est un pôle de référence en recherche sur les systèmes communicants. L’IRISA de Vannes est un pôle de référence en recherche sur les architectures logicielles, l’analyse et le traitement d’images, la fouille de données, l’interaction gestuelle, l’informatique mobile et décisionnelle. CriStAL est un pôle de référence en recherche sur l’in- génierie des données et de modèles, les systèmes embarqués temps réels, le traitement d’image, le génie logiciel et la conception système. Segula Engineering France 165 rue de la Montagne du Salut BP 50256 - 56602 Lanester Cedex Tel : +33 (0)2 97 87 73 07 www.segulatechnologies.com Laboratoire des Sciences et Techniques de l’Information, de la Communication et de la Connaissance (Lab-STICC) de Lorient, UMR 6285 Centre de Recherche Christiaan Huygens Rue de Saint Maudé 56321 Lorient Cedex Tel : +33 (0)2 97 87 45 60 www.lab-sticc.fr Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) de Vannes, UMR 6074 Campus de Tohannic Bâtiment ENSIBS, rue Yves Mainguy BP 57356017 Vannes cedex Tel : +33 (0)2 97 01 72 35 www-irisa.univ-ubs.fr Centre de Recherche en Informatique, Signal et Automatique (CRIStAL) de Lille, UMR 9189 Université Lille 1 Bâtiment M3 extension, Avenue Carl Gauss 59655 Villeneuve d’Ascq Cedex www.cristal.univ-lille.fr Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 2 Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017 Sommaire Sommaire v Table des ﬁgures ix Liste des tableaux xi Glossaire xiii Contributions scientiﬁques 1 Introduction générale 1 I Contexte et état de l’art 7 1 Contexte et problématiques 9 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.2 L’ingénierie système : contexte académique . . . . . . . . . . . . . . . . . . . 10 1.2.1 La spéciﬁcation des exigences . . . . . . . . . . . . . . . . . . . . . . 11 1.2.2 La vériﬁcation des exigences . . . . . . . . . . . . . . . . . . . . . . . 15 1.3 Conception des systèmes de contrôle-commande : contexte industriel . . . . . . 18 1.3.1 Les systèmes de contrôle-commande . . . . . . . . . . . . . . . . . . . 18 1.3.2 L’architecture SCADA . . uploads/Ingenierie_Lourd/ benefict-book 1 .pdf