Vérification des propriétés temporisées des automates programmables industriels

Le model-checking

  La méthode du model-checking (vérification du modèle) est fondée sur trois étapes :
– La phase de modélisation du système a pour but de fournir une représentation formelle du système étudié. De nombreux modèles ont été proposés, dont la sémantique est définie sous la forme de systèmes de transitions où les noeuds représentent les états du système, tandis que les transitions décrivent les évolutions possibles d’un état à un autre. On peut citer les structures de Kripke, les automates finis, les automates temporisés, les réseaux de Petri,. . .
– La phase de spécification de la propriété consiste à traduire dans un langage formel de spécification la propriété à vérifier, écrite en langage naturel. Parmi les nombreux formalismes proposés, citons les logiques temporelles de temps linéaire ou de temps arborescent (LTL,CTL,TCTL,. . .) , le µ-calcul,. . .
– La phase de vérification applique à ces données un algorithme qui vérifie si le modèle du système satisfait ou non le modèle de sa spécification. Cet algorithme dépend de la nature des modèles choisis pour le système et la propriété.

Travaux existants

   Comme nous l’avons dit précédemment, les automates temporisés ont été définis par Alur et Dill. La première définition est apparue dans [AD90], ensuite ils ont publié une version longue de leur travail [AD94]. Depuis cette classe de modèle a été largement étudiée. Par exemple, il a été montré dans [HKWT95] que le nombre d’horloges augmente le pouvoir d’expression des automates temporisés. D’autre part, un algorithme a été proposé dans [DY96] pour minimiser le nombre d’horloges d’un automate donné. D’autres travaux ont étudié des sous-classes intéressantes des automates temporisés. Par exemple, le problème universel qui est indécidable pour le modèle général, a été montré décidable pour la classe des automates temporisés à deux sens, bornés (“two-way bounded timed automata”) dans [AH92], et pour la classe des automates événement-horloge (“event-clock automata”) dans [AFH94] (le problème universel consiste à décider si le langage reconnu par un automate donné est égal à (Σ × R+)∞). De nombreuses variantes du modèle original ont été proposées. Une extension des automates temporisés avec des actions silencieuses (ε-transitions) a été étudiée dans [BGP96, BDGP98], il a été prouvé que l’ajout des actions silencieuses augmente strictement le pouvoir d’expression. Une variante du modèle d’Alur et Dill avec l’ajout des contraintes d’horloges du type (x + y ∼ c) a été étudiée dans [Duf97, BD00], il a été prouvé que ces modèles sont indécidables pour tester le vide du langage accepté, avec au moins quatre horloges. Dans [AHV93], il a été montré que les modèles avec des paramètres dans les contraintes d’horloges sont aussi indécidables pour le test du vide. Une autre extension des automates temporisés avec des mises à jour des horloges a été étudiée dans [BDFP00a, BDFP00b].

Outils de vérification

   Les algorithmes de model-checking sont implémentés dans des logiciels. Une importante activité de recherche concerne ces outils et vise à augmenter leur efficacité et à repousser leurs limites. Il existe plusieurs model-checkers temporisés : HyTech [HHWT95], Uppaal [LPY97] , Kronos [DOTY96], etc. Kronos est un model-checker pour TCTL. Uppaal permet la vérification d’un fragment de CTL tandis que HyTech réalise une analyse d’accessibilité sur les systèmes hybrides, un modèle qui étend les automates temporisés avec des horloges de pentes variables, des contraintes linéaires sur les horloges et des mises à jour plus riches. Nous présentons brièvement l’outil Uppaal ci dessous. Uppaal permet d’analyser des systèmes formés d’une collection d’automates temporisés qui communiquent par des variables entières partagées et des synchronisations par messages. Les automates temporisés d’Uppaal (figure ??) sont une variante des automates temporisés d’Alur et Dill. Leurs états de contrôle peuvent être étiquetés par deux étiquettes particulières :
– L’étiquette u pour Urgent : un tel état est équivalent au fait de remettre à zéro une horloge x avant d’arriver dans cet état et d’ajouter la garde x ≤ 0 sur les transitions d’action sortant de cet état. L’automate doit donc le quitter immédiatement. Les délais dans les états urgents sont toujours égalent à zéro.
– L’étiquette c pour Committed : cette notion est plus restrictive que la notion d’état urgent. L’automate doit quitter un état marqué par “c” immédiatement après son arrivée en empruntant forcément une des transitions sortant (s’il y en a plusieurs) d’un état étiqueté par c. En plus des horloges, les automates d’Uppaal manipulent des variables entières bornées. Les transitions de ces automates sont étiquetées par des gardes, des remises à zéro, des mises à jour de certaines variables entières et des étiquettes de synchronisation m? et m! où m est un canal. Notons qu’il y a deux possibilités de synchronisation de composants par messages :
– Les canaux binaires : un émetteur envoie le signal m! et un unique récepteur se synchronise avec lui par le signal complémentaire m?. Les transitions de ces deux composants étiquetées par m! et m? sont franchies en même temps. Si, à partir d’une configuration, plusieurs couples de transitions peuvent être synchronisées, le choix est non déterministe. Ce mode de synchronisation peut conduire à des blocages si un automate envoie un signal m! mais aucun composant ne peut le recevoir (par exemple si la garde de la transition étiquetée par m? est fausse).
– Les canaux multiples (broadcast) : les transitions étiquetées par m? et m! sont synchronisées, mais cette fois avec un émetteur et un nombre arbitraire de récepteurs, qui peut être égal à zéro. Ainsi, une synchronisation de ce type entre plusieurs composants ne conduit jamais à un blocage.

Les blocs fonctionnels

   L’utilisation des blocs fonctionnels dans la programmation des APIs est un mécanisme très utile, formalisé par la norme IEC 61131-3. Un bloc fonctionnel est représenté par un rectangle, a un nombre prédéfini de points de connexion en entrée (à gauche) et en sortie (à droite). C’est un programme qui réalise une fonction élémentaire entre ses entrées et ses sorties, caractérisée par un type. Il est utilisé d’une manière globale en faisant abstraction de son code interne. Un bloc fonctionnel possède en plus de ses entrées et de ses sorties, des variables internes. Son programme est écrit dans un des langages de la norme. Celle-ci n’exige pas de connecter toutes les entrées et les sorties des blocs fonctionnels au programme global.

Conception de programmes sûrs

   Dans le cas des langages de la norme IEC 61131-3, des modèles ont été développés pour l’extraction automatique de programmes corrects. Par exemple, un modèle à base de réseaux de Petri a été proposé dans [Fre98]. Une extension temporisée de ce modèle a été définie dans [Fre00b] avec une traduction vers le langage SFC. Une traduction vers les langages LD et IL a été introduite dans [Fre00a]. Dans [EFP94] un langage de programmation a été défini (c’est un sous ensemble de ST) pour la génération de programmes sûrs (pour les APIs) à partir d’une spécification. D’autre travaux ont proposé des modèles temporisés. Par exemple, dans [Hen97], les auteurs proposent un formalisme implémentable pour l’extraction automatique de programmes sûrs, à base de machines à états temporisées, appelées PLC-automates. Ils donnent aussi une traduction de ce formalisme vers du code ST. L’approche de conception de programmes sûrs nécessite de la part des constructeurs, un changement majeur de leurs techniques de programmation.

Description de la plate-forme MSS

   Présentation. La plate-forme MSS (figure 3.11) permet de trier des pignons (des petites pièces cylindriques) selon le matériau dont ils sont formés et de leur ajouter ou de leur retirer un palier (une petite pièce ronde). Cette plate-forme est composée de quatre postes consécutifs :
– poste 1 : Les pignons sont placés manuellement sur des palettes, et sont ensuite transportés et expédiés individuellement par un cylindre pneumatique au poste 2.
– poste 2 : Les pignons sont transportés par un chariot, piloté par une ceinture linéaire bidirectionnelle (figure 3.12). Le chariot s’arrête d’abord sur une position de test, où la présence/absence d’un palier est détectée. Ce test est effectué par un vérin et un capteur de fin de course. Le vérin commence à descendre aussitôt que le chariot est en position de test : si le vérin est détecté par le capteur de fin de course alors le palier est absent sinon le palier est présent. Ensuite, le chariot transporte le pignon pour être examiné par 3 capteurs (respectivement inductif, capacitif et optique) pour déterminer son matériau (respectivement acier, cuivre ou plastique noir). L’information récoltée est ensuite transmise au poste 3. Finalement, le chariot transporte le pignon à ce troisième poste.
– poste 3 : L’information obtenue précédemment est traitée à cette étape : les pignons sont emportés par le chariot pour une phase d’extraction ou d’insertion de palier.
– poste 4 : Les pignons sont déchargés.
L’étude de cas décrite dans cette section concerne le poste 2 de la plate forme MSS.

Table des matières

1 Introduction
1.1 Le model-checking
1.2 Modèle et logique temporisés
Automates temporisés
Logique temporisée
1.3 Contexte : Plan Pluri-Formations VSMT
Un automate programmable industriel (API)
1.4 Contributions de cette thèse
1.5 Plan de la thèse
2 Modélisation et spécification de systèmes temporisés 2.1 Systèmes de transitions temporisés
2.2 Logiques temporelles
2.2.1 La logique CTL
2.2.1.1 Syntaxe de CTL
2.2.2 La logique TCTL
2.2.2.1 Syntaxe de TCTL
2.2.2.2 Sémantique de TCTL
2.2.3 Expressivité
2.3 Les automates temporisés
Horloges
Contraintes d’horloges
2.3.1 Sémantique d’un automate temporisé
2.4 Problème d’accessibilité et graphe des régions
Le problème d’accessibilité
Le graphe des régions
Complexité
2.5 Model-checking de TCTL
2.5.1 Algorithme d’étiquetage
Complexité
2.5.2 Travaux existants
2.6 Outils de vérification
3 I Modélisation des automates programmables industriels
3 Les automates programmables industriels
3.1 Description des Automates Programmables Industriels
3.2 Comportement des Automates Programmables Industriels
3.3 Programmation des APIs
3.3.1 La norme IEC 61131-3
3.3.2 Les blocs fonctionnels
Les temporisateurs
3.4 État de l’art : vérification des APIs
Conception de programmes sûrs
Vérification de programmes existants
3.5 Étude de cas : la plate-forme MSS (Mechatronic Standard System)
3.5.1 Description de la plate-forme MSS
Présentation
Dysfonctionnement du test de vérin
3.5.2 Modélisation de la station 2 de la plate-forme MSS
3.5.2.1 Structure globale du modèle
3.5.2.2 Programme de contrôle
Modèle de la tâche maître
Modèle des temporisateurs
Modèle de la tâche événementielle
3.5.2.3 Système contrôlé : environnement
Modèle du chariot
Modèle du vérin
Modèles des capteurs
Modèle de l’environnement extérieur
3.5.2.4 Vérification avec l’outil Uppaal
3.6 Conclusion
II Spécifications et algorithmes
4 Abstraction des états transitoires
4.1 Motivations
4.2 Définition de la logique pour abstraire des états transitoires : TCTL∆
4.3 Sémantique de la logique TCTL∆
4.3.1 Définition d’autres opérateurs
Notation
4.3.2 Discussion
4.4 Équivalences de formules
4.5 Expressivité des modalités U k
4.5.1 TCTLa ≺ TCTL0
4.5.2 TCTL ≺ TCTL0
Formule E_U∼c_
Formule A_U∼c_
4.5.3 U k ne peut pas s’exprimer avec U k+1
Formule E_U k+1 ∼c _
Formule A_U k+1 ∼c _
4.6 Résultat d’indécidabilité pour la sémantique globale
4.6.1 Contexte général
4.6.2 La machine à deux compteurs
4.6.3 L’indécidabilité de TCTL∆ Σ
4.6.3.1 Incrémentation du compteur c1
4.6.3.2 Décrémentation du compteur c1
4.6.3.3 Réduction globale
4.7 Conclusion
5 Model-checking
5.1 Équivalence des exécutions
5.2 Algorithme de model-checking
5.2.1 Algorithme d’étiquetage
5.2.1.1 Formule E_U k ∼c_
5.2.1.2 Formule A_U k_
5.2.1.3 Formule A_U k c_
5.2.1.7 Formule A_U k =c_
5.3 Correction de l’algorithme d’étiquetage
Complexité
5.4 Discussion et conclusion
Conclusion et perspectives
Bibliographie
Index

Télécharger le rapport complet