Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande : application aux architectures SCADA

Résumé : 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.
Type de document :
Thèse
Automatique / Robotique. Université de Bretagne Sud, 2017. Français. 〈NNT : 2017LORIS442〉
Liste complète des métadonnées

Littérature citée [287 références]  Voir  Masquer  Télécharger

https://tel.archives-ouvertes.fr/tel-01680721
Contributeur : Abes Star <>
Soumis le : vendredi 12 janvier 2018 - 13:56:37
Dernière modification le : dimanche 14 janvier 2018 - 01:14:15

Fichier

2017theseMesliS.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01680721, version 2

Citation

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 / Robotique. Université de Bretagne Sud, 2017. Français. 〈NNT : 2017LORIS442〉. 〈tel-01680721v2〉

Partager

Métriques

Consultations de la notice

86

Téléchargements de fichiers

10