Approches de vérification formelle : propositions méthodologiques

Télécharger le fichier original (Mémoire de fin d’études)

Modélisation de l’IHM de supervision

Les interfaces de supervision développées avec les logiciels SCADA disposent d’une archi-tecture logicielle à deux niveaux (figure 3.3). Le niveau d’exploitation gère l’interaction avec l’utilisateur, aussi bien concernant l’aspect graphique de l’application que concernant les dis-positifs de commande. Le niveau fonctionnel constitue quant à lui le cœur de l’application. Il Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017

Vérification formelle d’une chaîne de contrôle-commande élémentaire

comporte l’ensemble des traitements de supervision et gère également les échanges de données avec le programme de commande.
Si nous nous replaçons dans le contexte plus large des systèmes interactifs (section 1.3.3.1 du chapitre 1), les modules de présentation et dialogue correspondent au niveau d’exploitation des logiciels SCADA ; le module d’application correspond, quant à lui, au niveau fonctionnel des logiciels SCADA, au programme de commande et au comportement du composant matériel (figure 3.3). Nous présentons ci-après, notre modélisation du module de dialogue et du module d’appli-cation. Le module de présentation n’est pas modélisé dans ce chapitre.

Modélisation du niveau d’exploitation (Module de dialogue)

Le comportement d’une IHM résulte du comportement de ses objets graphiques. Ces der-niers sont classés par Moussa et al. [2002] en objet de commande et objet informationnel. L’ob-jet de commande est un objet interactif qui permet à l’utilisateur de lancer des commandes, comme par exemple un bouton. Par contre, l’objet informationnel ne sert qu’à afficher des informations à l’utilisateur, comme par exemple un texte, une animation, etc.
Inspirés par les travaux de Moussa et al. [2002] et par analogie avec leur classification des objets interactifs en objet de commande et en objet informationnel, nous avons construit des automates temporisés génériques afin de modéliser le module de dialogue. La communication, entre ces objets et l’utilisateur, est modélisée par l’envoi et la réception de messages.
L’objet de commande. Par exemple un bouton. Cet objet est constitué de trois états : Masqué, Affiché Activé, Affiché Désactivé, voir figure 3.6. À l’état initial, l’objet de commande est dans l’état Masqué, qui modélise le fait que l’objet est masqué pour l’utilisateur, soit parce que la vue qui le contient (VueMèreMasquée ?) n’est pas affichée, ou bien parce que sa condi-tion d’activation est fausse. Dès que la vue mère est affiché, il reçoit le message (VueMéreAf-fichée ?) et évolue à l’état Affiché Activé ou bien à l’état Affiché Désactivé, si la condition de son activation (respectivement de sa désactivation) est vraie. Puis il envoie à l’utilisateur le message (ObjetActivé !) ou bien (ObjetDésactivé !), ce qui signifie que le bouton est affiché activé (l’utilisateur peut cliquer sur le bouton), respectivement désactivé (le bouton est grisé).
À l’état Affiché Activé, l’utilisateur peut cliquer sur l’objet, ce qui est modélisé par la réception du message (Interaction ?). L’objet appelle la fonction associée, comme définit dans le code de l’interface. Ces fonctions sont prédéfinies dans le logiciel SCADA. Cet appel de fonction est modélisé par un ensemble de localités instantanées. Cela signifie que l’objet retourne dans un de ses états (Masqué, Affiché Activé, Affiché Désactivé) instantanément. À la fin de cette action, l’objet teste sa condition d’activation ou de désactivation afin d’atteindre l’un des états Masqué, Affiché Activé ou Affiché Désactivé.
L’objet informationnel. Il est caractérisé par deux états : Affiché et Masqué (figure 3.7).
À l’état initial, l’objet est Masqué. L’objet est masqué soit parce que sa condition de visibilité (Cond_Visibilié sur la figure 3.7) est fausse ; soit parce que la vue qui le contient est masquée (réception du message VueMèreMasquée). Dans cet état, il envoie le message ObjetMasqué !. Ce dernier est capturé par l’automate décrivant le comportement de l’utilisateur et signifie que l’objet est masqué pour l’utilisateur. Si la condition de visibilité devient vraie et que la vue mère est affichée, l’objet passe à l’état Affiché. Dans cet état, il envoie à l’utilisateur le message
ObjetAffiché ! qui signifie que l’objet est affiché à l’utilisateur. L’objet retourne à l’état Masqué si sa condition de visibilité est fausse, ou bien si sa vue mère n’est plus affichée (VueMèreMas-quée ?). Notons que l’objet informationnel ne reçoit pas d’interactions des utilisateurs car il ne sert qu’à afficher des informations.
Modélisation du niveau fonctionnel du logiciel SCADA Les actions associées aux objets de commande sont des fonctions basiques prédéfinies dans le logiciel SCADA. Nous modélisons ces fonctions par un automate temporisé et du code C dans UPPAAL. La figure 3.8 présente la modélisation de deux fonctions prédéfinies par l’automate temporisé de la figure 3.8-a et le code C correspondant à chaque fonction (figure 3.8-b). La fonction Fonction1, par exemple, permet d’inverser une valeur booléenne de 1 à 0 et de 0 à 1. La fonction Fonction2 permet l’affectation d’une valeur à une variable booléenne.
Le programme LD Le langage LD ou langage à contact est un langage graphique très répandu dans la pro-grammation des API. Le formalisme du langage LD a été inspiré des schémas électriques.
Un diagramme LD se compose de variables et d’échelons (ou rung en anglais, annotés R1, R2, etc. sur la figure 3.9). Les variables peuvent être des entrées qui proviennent de l’envi-ronnement ou des sorties vers cet environnement. Les rungs sont liés à une alimentation (ligne verticale tout à gauche) et se lisent de haut en bas. Chaque rung (ligne) est constitué de plusieurs éléments :
– Les contacts (entrées), comme FdcC et CtrlO sur la figure 3.9, permettent de lire une variable booléenne. Le contact peut être normalement ouvert ou normalement fermé. Un contact normalement ouvert est représenté par deux barres verticales (FdcC sur la ligne R1), et signifie qu’il est fermé si la variable booléenne associée est vraie, sinon, il est ouvert. Un contact normalement fermé est représenté par deux barres verticales et un slach (« / ») entre les deux barres (CtrlO sur la ligne R2), signifie que le contact est ouvert si la variable booléenne associée est vraie, sinon, il est fermé.
– Les bobines (sorties), comme StC et StFCmd sur la figure 3.9, servent à écrire la valeur d’une variable booléenne.
– Les blocs fonctionnels, par exemple TON2 sur la figure 3.9, permettent l’exécution de fonctions plus avancées (temporisateurs, compteurs, opérations arithmétiques, etc.)
Les éléments en séries (ET logique) sont sur la même ligne, a contrario, les éléments en parallèles (OU logique) sont sur plusieurs branches. Par exemple les lignes R2 et R3 de la figure 3.9 sont deux branches en parallèles, où chaque branche regroupe des éléments en sé-ries (CtrlO et FdcC sur la deuxième branche). Chaque rung peut s’écrire sous la forme d’une équation logique. Par exemple, la ligne R1 peut s’écrire StC:= FdcC.

Génération automatique des AT à partir du programme LD

L’approche est inspirée des travaux de Mokadem et al. [2010], Sarmento et al. [2008] et de Bender et al. [2008]. Initialement, nous modélisons manuellement en automates temporisés un sous-ensemble de blocs fonctionnels proposés par la norme IEC 61131-3. Nous avons modélisé essentiellement des temporisateurs (TP, TON et TOF), des bascules (RS, SR) et des détecteurs de front montant (RTRIG) et descendant (FTRIG). La figure 3.10 présente les automates tem-porisés respectifs des temporisateurs TON et TOF.
Modélisation des temporisateurs. Le temporisateur TON a pour rôle de gérer les retards à l’enclenchement, i.e. que la sortie Q de ce temporisateur passe à 1 après une durée définie (temporisation) durant laquelle l’entrée (in) est à 1. La sortie Q passe immédiatement à 0 si l’entrée in est égale à 0.
Nous avons modélisé ce temporisateur par trois états (figure 3.10-a), deux variables boo-léennes (in et Q) et une horloge (c1). À l’état initial le temporisateur est au repos. Il reste dans cet état et maintient la sortie Q à 0 tant que in est fausse (in==0). Le temporisateur passe à Intégration des techniques de vérification formelle dans une approche de conception des systèmes de contrôle-commande Soraya Kesraoui 2017

Vérification formelle d’une chaîne de contrôle-commande élémentaire

l’état Traitements si l’entrée est vraie et s’il a reçu un message (TON ?) de la part de l’auto-mate principal. Il reste dans cet état tant que la durée de temporisation n’est pas encore écoulée (c1<=PT), PT est une constante qui définit la durée de la temporisation. Une fois la durée écoulée (c1==PT) et que l’entrée in est toujours vraie, le temporisateur atteint l’état Fin Tem-porisation et il reste dans cet état tant que l’entrée in est vraie. Il quitte cet état pour atteindre l’état initial si l’entrée in devient fausse.

Table des matières

Sommaire
Table des figures
Liste des tableaux
Glossaire
Contributions scientifiques
Introduction générale
I Contexte et état de l’art
1 Contexte et problématiques
1.1 Introduction
1.2 L’ingénierie système : contexte académique
1.2.1 La spécification des exigences
1.2.2 La vérification des exigences
1.3 Conception des systèmes de contrôle-commande : contexte industriel
1.3.1 Les systèmes de contrôle-commande
1.3.2 L’architecture SCADA
1.3.3 Approches traditionnelles pour la conception des systèmes de contrôlecommande
1.3.4 Génération automatique des programmes de contrôle-commande
1.4 Problématiques et verrous scientifiques
1.4.1 Problématiques
1.4.2 Verrous scientifiques
1.5 Conclusion
2 État de l’art : systematic mapping
2.1 Introduction
2.2 État de l’art au travers des revues de la littérature existante
2.2.1 Classification des langages formels
2.2.2 Comparaison des langages de spécification
2.2.3 Utilisation des méthodes formelles
2.2.4 Bilan sur les revues de la littérature existantes
2.3 Méthode
2.4 Étape 1 : Définition du protocole
2.4.1 Définition des questions de recherche
2.4.2 Stratégie de la recherche
2.4.3 Sélection des articles
2.4.4 Extraction des données et classification
2.4.5 Évaluation de la validité de l’étude
2.5 Étape 2 : Conduction
2.6 Étape 3 : Rapport de synthèse
2.6.1 Résultats démographiques
2.6.2 Proposition d’une classification des langages formels
2.7 Résultats obtenus
2.7.1 QR1 : Quels sont les langages de spécification utilisés pour la vérification
formelle ?
2.7.2 QR2 : Comment a été réalisée la vérification formelle ?
2.7.3 QR3 : Quels sont les objectifs de la vérification formelle ?
2.8 Conclusion et Discussions
2.8.1 Bilan
2.8.2 Propositions
II Approches de vérification formelle : propositions méthodologiques
3 Vérification formelle d’une chaîne de contrôle-commande élémentaire
3.1 Introduction
3.2 Exemple illustratif : V2VM
3.2.1 Comportement de l’utilisateur
3.2.2 L’interface de supervision
3.2.3 Le programme de commande
3.2.4 La partie opérative
3.2.5 Les exigences de conception
3.3 Contexte et travaux connexes
3.3.1 Vérification formelle des programmes de commande
3.3.2 Vérification formelle des interfaces de supervision
3.3.3 Manques dans les travaux existants et problématique associée
3.4 Vérification formelle d’une chaîne de contrôle-commande élémentaire
3.4.1 Concepts utilisés
3.4.2 Approche générale
3.4.3 Formalisation d’une chaîne de contrôle-commande élémentaire
3.4.4 Vérification formelle d’une chaîne de contrôle-commande élémentaire
3.5 Conclusion
4 Vérification formelle des modèles de conception (P&ID)
4.1 Introduction
4.2 Exemple illustratif : P&ID
4.3 Contexte et travaux connexes
4.3.1 Vérification des P&IDs
4.3.2 Les architectures logicielles
4.4 Approche proposée
4.4.1 Concepts utilisés
4.4.2 Vérification formelle des diagrammes P&ID
4.4.3 Un style architectural pour la norme ANSI/ISA-5.1
4.4.4 Génération des modèles Alloy à partir des P&ID
4.4.5 Formalisation des exigences et vérification formelles des P&ID
4.4.6 Aide à l’analyse des résultats
4.5 Conclusion
III Approches de vérification formelle : mise en oeuvre et applications
5 Implémentation
5.1 Introduction
5.2 Méthodologie mise en oeuvre
5.2.1 Concepts IDM utilisés
5.2.2 Outils et langages utilisés
5.3 Flot de vérification des composants standards
5.3.1 Opération de modélisation de la tâche utilisateur
5.3.2 Opération de transformation de HAMSTERS en AT intermédiaire (AT’)
5.3.3 Opération de transformation des IHM SCADA en AT’
5.3.4 Opération de transformation des programmes LD en AT’
5.3.5 Opération de transformation de AT’ en AT
5.3.6 Opération de modélisation du composant physique en AT
5.3.7 Opération de spécification des exigences en CTL
5.3.8 Opération de vérification formelle
5.3.9 Bilan
5.4 Flot de vérification formelle des diagrammes P&ID
5.4.1 Opération de formalisation de la norme ANSI/ISA-5.1
5.4.2 Opération de construction
5.4.3 Opération de spécification des exigences
5.4.4 Opération d’épuration
5.4.5 Opération de transformation de P&ID en Alloy
5.4.6 Opération de vérification
5.4.7 Opération de visualisation des erreurs
5.4.8 Opération de correction
5.4.9 Bilan
5.5 Conclusion
6 Application à des cas industriels
6.1 Introduction
6.2 Vérification formelle de V2VM : Étude de cas
6.2.1 Opération de modélisation de la tâche utilisateur
6.2.2 Opération de transformation de HAMSTERS en AT
6.2.3 Opération de transformation des IHM SCADA en AT
6.2.4 Opération de transformation des programmes LD en AT
6.2.5 Opération de modélisation du composant physique en AT
6.2.6 Opération de spécification des exigences en CTL
6.2.7 Vérification formelle de V2VM
6.2.8 Validité
6.2.9 Bilan de la vérification formelle de la V2VM
6.3 Vérification formelle du P&ID du système EdS : Etude de cas
6.3.1 Opération de construction
6.3.2 Opération de spécification des exigences
6.3.3 Opération d’épuration et de transformation du P&ID en Alloy
6.3.4 Opération de vérification
6.3.5 Opération de visualisation des erreurs
6.3.6 Validité
6.3.7 Bilan de la vérification formelle du P&ID du système EdS
6.4 Conclusion
7 Conclusion
7.1 Introduction
7.2 Rappel des contributions
7.2.1 Intégration de la vérification formelle dans une démarche de conception
7.2.2 Aide à l’obtention des modèles formels
7.2.3 Application à des cas d’étude concrets
7.3 Perspectives
7.3.1 Extensions des flots proposés
7.3.2 Aide à la spécification des exigences
7.3.3 Vérification formelle du système global
Bibliographie
Annexes
A Données de la Systematic Mapping
A.1 Requêtes de recherche dans les différentes bases
A.2 Listes des articles retenus pour la systematic mapping
B Guide d’entretien réalisé avec les experts métiers
B.1 Présentation
B.2 Analyse des exigences
B.3 Analyse de la conception système
B.4 Analyse de la vérification
B.5 Confrontation avec le P&ID, la commande, et l’interface de supervision
C Modèle complet de V2VM
C.1 Tâches utilisateurs
C.2 Interface de supervision
C.3 Programme de commande
C.3.1 Composant physique
C.4 Extrait d’un contre-exemple Alloy en XML
D Grammaire VB en xtext