COMPRENDRE ET ANALYSER LE SAE

Connaissances liées au model checking

Dans cette section nous définissons les connaissances liées au model checking, que nous abrégerons en connaissances techniques, comme l’ensemble des informations requises et produites par le processus de vérification par model checking, telles que les propriétés, le modèle formel, le LTS ou encore les traces. Ces connaissances sont toujours présentes lors de l’activité de diagnostic. 4.1.1 Concepts SAE Le système à l’étude (SAE) est décrit par une spécification comprenant un lot de propriétés formelles, et un modèle formel de son comportement. Composant et processus Le comportement du système est décrit par un composant. Il contient des variables globales (fifos par exemple) et des instances de processus reliés entre eux par des canaux. Un processus est une machine à état qui évolue de manière concurrente aux autres processus. Il est décrit par un ensemble de variables et d’un automate, lui-même composé d’états et de transitions. Durant l’exécution d’une transition, différentes actions sont réalisées comme l’affectation de variable, la lecture ou l’écriture dans un canal. Un des états est initial. Message et canal Un processus communique avec d’autres processus, soit de façon synchrone, soit de façon asynchrone. Dans la thèse, nous faisons le choix que les échanges sont uniquement asynchrones. Dans ce cas précis, des messages sont échangés via des canaux de type FIFO où l’ordre d’envoi des messages est préservé lors de la réception. 63 COMPRENDRE ET ANALYSER LE SAE Partie , Chapitre 4 – Comprendre et analyser le SAE Environnement L’environnement communique également par envoi de messages asynchrones avec le système. Il guide ainsi l’exécution du système suivant un scénario, réduisant de ce fait son espace d’état. Au moment de l’exécution, il est instancié automatiquement sous la forme d’un processus unique. Graphe d’exploration Un graphe d’exploration produit par un model checker (OBP dans notre cas) représente l’ensemble des états atteignables du modèle nommés configurations, composé du système (modélisé en langage FIACRE) et de l’environnement (décrit avec CDL pour OBP). Un graphe d’exploration est produit par le model checker, celui-ci possède toujours une configuration initiale et un ensemble de configurations finales. Configuration Une configuration est une structure de données regroupant des informations relatives à un état du système et son environnement. Une configuration regroupe les informations sur des instances de processus et de leurs informations (variables, états), des canaux de communications, des prédicats ou des observateurs. Transition Une transition est un arc entre deux configurations. Chaque transition est associée à un label. Dans le cas d’OBP il représente soit une émission de message, soit une réception de messages, soit un rendez-vous, soit un « internal » (changement interne à un processus). Trace Une trace est la description d’un chemin dans le graphe d’exploration. Une trace possède une configuration initiale, et une configuration finale, correspondant généralement au rejet d’un observateur. Il peut exister plusieurs traces ayant la même configuration initiale et finale. Prédicats Un prédicat permet d’évaluer des expressions basées sur les données d’exécution du modèle (variables, états…). Par exemple, déterminer si le processus NET est dans l’état idle, se traduit en CDL par predicate P1 is Net1@Idle. Déterminer si la variable length de la fifo F1 du composant Run1 est inférieure à une constante donnée SIZE, se traduit en CDL 64 4.1. Connaissances liées au model checking par predicate P2 is Run1 : F1.length <= SIZE. Autre cas de figure, un événement associé à un changement de valeur d’un prédicat. Exemple, l’événement E1 survient lorsque le prédicat P1 devient vrai, se traduit en CDL par l’expression E1 is P1 becomes true. Observation des propriétés Un observateur, au sens OBP, est un automate. Selon la séquence des transitions, consécutive à l’observation des activités du système et de l’environnement, l’observateur atteint soit un état que l’on souhaite obtenir (état succès), soit un état qui ne doit pas apparaître (état rejet). L’observateur peut observer des occurrences d’événements (émission ou réception de message), ou des changements de valeur booléenne d’un prédicat. Les transitions, déclenchées par l’observation des événements (event), peuvent être gardées par des prédicats (predicate). Une version simplifiée d’une transition (non-temporisée) entre un état source (sourceState) et un état cible (targetState) est définie grâce à la syntaxe sourceState – / predicate / event / -> targetState. Un observateur permet d’exprimer une propriété de type sûreté (il contient un état reject). Logique temporelle La logique temporelle, comme la LTL, permet d’exprimer des propriétés et des prédicats logiques à l’aide d’opérateurs logiques (nous utiliserons ici not (¬), and (∧), or (∨) et implies (→)) et temporels (nous utiliserons ici globally (), eventually (♦) et weakly until (W)). Pour exprimer de telles propriétés, il est possible d’utiliser Plug, une extension à OBP. Si les observateurs permettent d’exprimer pleinement les propriétés de sûreté, ils ne permettent pas d’exprimer la vivacité. Il faut donc utiliser la LTL pour exprimer des propriétés de vivacité.

Modèle Reprenons le premier scénario

Le modèle à vérifier est exprimé dans le langage formel Fiacre. L’architecture est composée de 4 entités, un contrôleur global appelé GC, deux contrôleurs locaux Plc1 et Plc2 et un réseau de communication Network reliant le GC aux Plc1 et Plc2. Les contrôleurs locaux permettent d’accéder à une ressource partagée Res, chacun par un accès, respectivement Res1 et Res2. L’architecture fonctionne de la manière décrite par les automates 4.1, 4.2 et 4.3. Une entité de l’environnement souhaite accéder à une ressource de l’architecture. Elle envoie un message au GC indiquant dans le message la demande d’accès à la ressource (Res1 ou Res2) et l’opération à réaliser sur cette ressource (Read ou Write). GC reçoit cette requête (état Idle), l’ignore si elle lui est directement adressée (état ReceivedForward, puis transition GcIgnoring), ou dans le cas contraire, la retransmet à un PLC via le 65 Partie , Chapitre 4 – Comprendre et analyser le SAE Figure 4.1 – Automate de GC Figure 4.2 – Automate de NET 66 4.1. Connaissances liées au model checking Network (état Sending). Le Network traite ensuite la requête (état ReceivedForward). Comme GC, si la requête lui est destinée, il l’ignore (retour dans l’état Idle), sinon il la retransmet au PLC concerné. Le PLC reçoit la requête (état Received), accède à la ressource (état Access) et envoie un message contenant une réponse (état Sending). La réponse est transmise à l’environnement en passant d’abord par le Network, puis par le GC, via leurs états respectifs (ReceivedBack). Les entités considérées jouent des rôles différents. Le rôle P LC1_OW NER a les droits en lecture et écriture sur RES via Res1 mais pas via Res2. Le rôle P LC2_OW NER a les droits en lecture et écriture via Res2 mais pas via Res1. Nous considérons deux clients, le Client1 joue le rôle de P LC1_OW NER, et le Client2 joue le rôle de P LC2_OW NER. Figure 4.3 – Automate de PLC Les processus sont reliés par des FIFOs de taille finie. Ici la taille initiale est 4, c’est à dire que la fifo peut contenir jusqu’à 4 messages, pas au delà. Les FIFOs supportent des messages de deux types, SEND (requête) ou RECV (réponse). Un message contient différents paramètres, l’entité source à l’origine du message (source), l’entité destinataire (target), et une donnée (data). Une donnée (data) est composée de trois informations, le type d’opération, soit lecture (RED) ou écriture (WRT), l’accès à la ressource, soit Res1 ou Res2, et un type d’acquittement, soit ACK ou NACK. Le listing 4.1 présente un exemple de message exprimé en Fiacre. 67 Partie , Chapitre 4 – Comprendre et analyser le SAE 1 // Exemple , un message de l e c t u r e par l e Cli e n t 1 de l a Res1 g e r e e par l e PLC1 2 CLT1_READ_PLC1 i s { s o u r c e = ID_CLT_1, t a r g e t = ID_PLC_1, data = RED_RES1} Listing 4.1 – Message Pour simplifier, les messages sont associés à une constante qui respecte des conventions de nommage dans l’ordre suivant type de message [envoi (SEND) | réception (RECV)], entité source, entité cible, type d’accès [lecture (RED) | écriture (WRT)], ressource. Par exemple, une demande de lecture de la Res1 détenue par le Plc1 par le Client1 est exprimée par la constante SEND_CLT1_P LC1_RED_RES1.