31 0 211KB
Chapitre 5
Vérification basée sur les modèles (Model Checking)
I. Le langage PROMELA 1. Introduction S P I N est un vérificateur de modèle - un logiciel pour la vérification des modèles de systèmes physiques, en particulier de systèmes informatiques. Tout d'abord, un modèle est écrit pour décrire le comportement du système; ensuite, les propriétés d'exactitude qui expriment des exigences sur le comportement du système sont spécifiées; enfin, le vérificateur de modèle est exécuté pour vérifier si les propriétés correctes sont valides pour le modèle et, dans le cas contraire, un contre-exemple est fourni: un calcul qui ne satisfait pas une propriété d'exactitude. Le challenge de la vérification basée sur les modèles consiste à écrire un modèle qui décrit le système de manière suffisante pour le représenter fidèlement, et ce modèle doit être suffisamment simple pour que le modélisateur puisse effectuer la vérification avec les ressources disponibles (temps et mémoire). Le langage PROMELA est utilisé pour écrire des modèles dans SPIN. Promela signifie “Protocol Meta Language”. Promela est un langage de spécification de systèmes distribués et de systèmes parallèles asynchrones. Il permet de décrire des systèmes concurrents, en particulier des protocoles de communication. Ce langage autorise la création dynamique de processus. Les communications peuvent s’effectuer de différentes manières: partage de variables globales, envoi et réception de messages via des canaux de communication. Ces derniers peuvent être définis pour réaliser des communications tant synchrones (rendez-vous) qu’asynchrones (bufférisées). Les interactions entre processus concurrents peuvent créer de nombreux problèmes tels que des inter-blocages, des modifications inattendues de valeurs de variables ...etc. La vérification de la correction d’un système décrit en PROMELA peut être réalisée grâce à l’outil de simulation et d’analyse spin.
Spin simule l’exécution du système en faisant des choix aléatoires d’ordre d’exécution des différents processus. Il engendre un programme C qui effectue une validation exhaustive par construction du graphe d’états. Lors des simulations et des validations, spin vérifie l’absence de blocage, cherche les réceptions de messages non spécifiées ainsi que les parties de code qui ne peuvent être atteintes; ni par conséquent exécutées. L’outil de validation peut également être utilisé pour vérifier des invariants du système et trouver des cycles d’exécution ne conduisant à aucune progression. Des techniques de compression de la représentation en mémoire du graphe d’états peuvent être utilisées dans Spin , qui permettent de construire des graphes de taille très importante.
2. Le langage Promela Les programmes dans PROMELA sont écrits en utilisant la syntaxe des langages de type C. Un programme PROMELA est constitué d'un ensemble de processus, de canaux de communication servant à transmettre des messages, et de variables. Les canaux et variables peuvent être déclarés soit globalement, soit localement, à l’intérieur d’un processus. Les processus spécifient le comportement du système alors que les canaux et variables définissent l’environnement d’exécution. En PROMELA, il n’y a aucune différence entre les conditions et les instructions. L’exécution d’une instruction ne peut avoir lieu que si celle-ci est exécutable. Une instruction est soit exécutable soit bloquante. Certaines instructions sont toujours exécutables, d’autres sont toujours bloquantes, mais la plupart peuvent être l’un ou l’autre en fonction des conditions. En particulier, une instruction bloquante peut être rendue exécutable (et viceversa) par certains événements. Une condition ne peut être passée que si elle est satisfaite. Si ce n’est pas le cas, elle est bloquée jusqu’à ce qu’elle devienne vraie. Les instructions sont séparées par un ";" ou "->". Tous deux sont équivalents, mais la flèche, dans certains cas, peut contribuer à la lisibilité du programme en indiquant une causalité. La dernière instruction, ne devant être séparée d’aucune autre, n’est pas suivie d’un séparateur. Exemple: au lieu d'écrire une boucle d'attente occupée. while(a!=b);
/* attend que a soit egal a b */
a = a+1;
/* ensuite augemente a de 1 */
bloque l’exécution du programme si a est différent de b. Le programme ne peut reprendre son cours que lorsque a sera devenu égal à b. En Promela, cette séquence s’écrire simplement : (a==b); a=a+1; ce qui peut être interprété comme "dès que a sera égal à b, a sera incrémenté de 1. Les affectations, comme a=2; ou encore a=a+1; etc sont toujours exécutables. L’instruction skip est une instruction toujours exécutable, mais qui ne fait rien et ne rend aucune valeur. Par exemple la séquence précédente s’écrit aussi : (a==b) -> a=a+1;
Exemple: Inversion des chiffres d'un nombre entier de 3 chiffres 1 2 3 4 5 6 7
active proctype P() { int value = 123; / * int reversed; / * reversed = (value % 10) *100 + ((value / 10) % 10) * 10 + (value / 100); printf("value = %d, rever sed = %d\n", value, reversed) }
Remarque: Par convention, un programme PROMELA n'a pas d'entrée, puisqu'il est destiné à simuler un système fermé. C'est-à-dire que s'il y a une unité dans l'environnement qui pourrait influencer le système, elle devrait être modélisée comme un processus. Néanmoins, il existe un canal d'entrée STDIN connecté à une entrée standard qui peut être utile pour exécuter des simulations d'un modèle unique avec des paramètres différents. 3. Variables et types de données Les variables dans PROMELA sont utilisées pour stocker des informations globales sur le système dans son ensemble ou des informations locales pour un processus spécifique, en fonction de l'emplacement de la déclaration de la variable. Une variable peut être l'un des six types de données prédéfinis suivants: bit, bool, byte, short, int, unsigned, chan. Les cinq premiers types de cette liste sont appelés les types de données de base. Ils sont utilisés pour spécifier des objets pouvant contenir une seule valeur à la fois. Le sixième type spécifie les canaux de message. Un canal de message est un objet qui peut stocker un certain nombre de valeurs, groupées dans des structures définies par l'utilisateur.
Les déclarations bool flag; int state; byte msg;
définissent des variables pouvant stocker des valeurs entières dans trois plages différentes. La portée de la variable est globale si elle est déclarée en dehors de toutes les déclarations de processus et locale si elle est déclarée dans la partie déclaration d'un processus. 3.1. Les types de données de base Les types de données numériques de PROMELA sont basés sur ceux du compilateur C utilisé pour compiler SPIN lui-même; ils sont indiqués dans le tableau ci-dessous. Tous les efforts devraient être faits pour modéliser les données en utilisant des types qui nécessitent le moins de bits possible pour éviter une explosion combinatoire dans le nombre d'états au cours d'une vérification: short au lieu de int et byte au lieu de short. Type
Taille (bits)
Valeurs
bit
1
0, 1
bool
1
false, true
byte
8
0 . . 255
short
16
-32768 . . 32767
int
32
-231 . . 231 -1
n ≤ 32
0 . . 2n -1
unsigned
Remarques: 1. Toutes les variables sont initialisées par défaut à zéro, mais il est recommandé de toujours donner des valeurs initiales explicites dans les déclarations de variables non seulement par de bonnes pratiques de programmation; mais cela peut également affecter la taille des modèles dans SPIN. 2. Les types bit et bool sont des synonymes pour un seul bit d'information. 3. Le type unsigned peut être utilisé pour les variables destinées à stocker des valeurs signées d'un nombre de bits spécifié. 4. PROMELA n'a pas les types de données suivants: •
le type caractère (char): les valeurs littérales peut être affectées à des variables de type octet et imprimé en utilisant le spécificateur de format %c.
•
le type chaîne de caractères: les messages sont mieux modélisés en utilisant seulement quelques codes numériques et le texte intégral n'est pas nécessaire. Dans tout les cas, les instructions printf ne sont utilisées que pour faciliter la simulation et sont ignorées lorsque SPIN effectue une vérification.
•
le type virgule flottante: les nombres en virgule flottante ne sont généralement pas nécessaires dans les modèles parce que les valeurs exactes ne sont pas importantes; il est préférable de modéliser une variable numérique par une poignée de valeurs discrètes telles que minimum, bas, haut, maximum.
3.2. Les tableaux PROMELA inclut le type tableau, une séquence de valeurs de données du même type, dont les éléments peuvent être accédés en fournissant un index donnant la position de l'élément dans la séquence. La syntaxe et la sémantique des tableaux sont similaires à celles des langages de type C; la première position dans le tableau se trouve à l'index zéro et les crochets sont utilisés pour l'opération d'indexation. Un message d'erreur sera affiché si l'index n'est pas dans les bornes de l'intervalle d'un tableau. Les tableaux dans PROMELA sont unidimensionnels. Les variables de type tableaux peuvent être déclarées comme suit: Par exemple, byte state[N] déclare un tableau de n octets qui peut être consulté dans des instructions telles que : state[0] = state[3] + 5 * state[3*2/n] où n est une constante ou une variable déclarée ailleurs. L'index d'un tableau peut être n'importe quelle expression qui détermine une valeur entière unique. L'effet d'une valeur d'index en dehors de la plage "0 .. N-1" est indéfini.
Exemple: Calcul de la somme des éléments d'un tableau d'entiers. 1 2 3 4 5 6 7 8 9 10
#include "for.h" active proctype P() { int a[5]; a[0] = 0; a[1] = 1 0; a[2] = 20; a[3] = 30; a[4] = 40 ; int sum = 0; for (i, 0, 4) sum = sum + a[i] rof (i); printf("The sum of the nu mbers = %d\n", sum) }
Remarques: •
Les éléments d'un tableau peuvent être initialisés par un calcul par une boucle: for (j, 0, 4) a[j] = j* 10 rof (j)
•
Les éléments d'un tableau peuvent être initialisés par une expression non déterministe: for (j, 0, 4) if
:: a[j] = j* 10 :: a[j] = j + 5
fi rof (j)
•
Une valeur initiale dans une déclaration est affecté à tous les éléments d'un tableau: int a[5] = 10;
3.3. Les noms symboliques Les constantes peuvent être définies comme en C. Pour déclarer un symbole pour un nombre, une macro de préprocesseur peut être utilisée au début du programme: #define N 10
La substitution textuelle est utilisée lorsque le symbole est rencontré:
i = j% N;
Le type mtype peut être utilisé pour donner des noms mnémoniques aux valeurs. L'avantage d'utiliser mtype sur une séquence de #define est que les valeurs symboliques peuvent être imprimées en utilisant le spécificateur de format %e, et elles apparaîtront dans les traces des programmes. En interne, les valeurs du type mtype sont représentées comme des valeurs d'octets positifs, il peut donc y avoir au plus 255 valeurs du type. Une limitation sur mtype est qu'il n'y a qu'un seul ensemble de noms défini pour un programme entier; Si vous ajoutez des déclarations, les nouveaux symboles sont ajoutés à l'ensemble existant. Exemple: 1 2 3 4 5 6
mtype = { red, yellow, green }; mtype light = green; active proctype P() { do :: if
7 8 9 10 11 12 od 13 } 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
:: light == red - > light = green :: light == yellow -> light = red :: light == green -> light = yellow fi ; printf("The light is now %e\n", light)
mtype = { red, yellow, green }; mtype = { green_and_yell ow, yellow_and_red }; mtype light = green; active proctype P() { do :: if :: light == red - > light = yellow_and_red :: light == yellow_and_red -> light = green :: light == green -> light = green_and_yellow :: light == green _and_yellow -> light = red fi ; printf("The light is now %e\n", light) od }
3.4. Les structures L’utilisateur peut définir ses propres structures nommées, à partir des types de base. Le mot réservé typedef permet d’introduire un nouveau nom pour désigner une structure, dont chaque champ a un type déjà défini. Ce nouveau type peut alors, à son tour, être utilisé pour déclarer et instancier de nouveaux objets. Ces types composés sont principalement utilisés pour définir la structure des messages à envoyer sur les canaux de communication.
Exemple: typedef Field{ short f; byte g }; typedef Msg { byte a[3]; int fld1; Field fld2; bit b }; Msg monmessage; monmessage.fld2.f = 3
Une utilisation additionnelle des définitions de type consiste à déclarer un tableau à deux dimensions comme un tableau dont les éléments sont défini par une définition de type avec un seul champ de type tableau: typedef VECTOR { int vector[10] } VECTOR matrix[5]; matrix[3].vector[ 6] = matrix[4].vector[7];
Exemple: Le programme ci-dessous utilise des définitions de type pour initialiser et imprimer un tableau creux. Un tableau creux est une structure de données utilisée pour stocker un tableau dont la plupart des éléments sont nuls. Pour chaque élément non nul du tableau, sa ligne, sa colonne et sa valeur sont stockées. 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 24 25 26 27 28 29
#include "for.h" #define N 4 typedef ENTRY { byte row; byte col; int value } ENTRY a[N]; active proctype P() { int i = 0; a[0].row = 0; a[0] .col = 1; a[0].value = -5; a[1].row = 0; a[1] .col = 3; a[1].value = 8; a[2].row = 2; a[2] .col = 0; a[2].value = 20; a[3].row = 3; a[3] .col = 3; a[3].value = -3; for (r, 0, N-1) for (c, 0, N-1) if :: i == N -> printf("0 ") :: i < N && r == a[i].row && c == a[i].col -> printf("%d ", a[i].valu e); i++ :: else -> printf("0 ") fi rof (c); printf("\n") rof (r) }
3.5. Les canaux de communications
Les systèmes distribués sont des systèmes informatiques constitués d'un ensemble de nœuds reliés par des canaux de communication. Pour modéliser un système distribué, les nœuds sont modélisés en tant que processus concurrents et les réseaux de communication en tant que canaux sur lesquels les processus peuvent envoyer et recevoir des messages. Les canaux de communication permettent aux processus d’échanger des messages. Un canal dans PROMELA est un type de données avec deux opérations, envoyer et recevoir. Chaque canal a associé un type de message; Une fois qu'un canal a été initialisé, il peut seulement envoyer et recevoir des messages de son type de message. Un nombre de 255 canaux peuvent être créés au plus. Le canal est déclaré avec un initialiseur spécifiant la capacité du canal et le type de message: chan ch = [capacity] of { typename, ..., typename }
La capacité du canal doit être une constante entière non négative. Le type de message spécifie la structure de chaque message pouvant être envoyé sur le canal sous la forme d'une séquence de champs; le nombre de champs et le type de chaque champ sont spécifiés dans la déclaration. Le nom d’un canal peut apparaître dans des instructions d'affectations, peut être transmis par des canaux de communication, ou passé en paramètre à des processus. Exemple: chan canal_1 = [16] of {short}; chan canal= [16] of {byte, int, chan, byte}, chan q1 = [5] of {int}; chan q2 = [2] of {int, chan}; chan q3 = [0] of {int};
Il existe deux types de canaux avec des sémantiques différentes: les canaux de rendezvous de capacité zéro et les canaux tamponnés de capacité supérieure à zéro. L'instruction d'envoi de messages consiste en une variable de canal suivie d'un point d'exclamation, puis d'une séquence d'expressions dont le nombre et les types correspondent au type de message du canal.
chan_name ! liste expressions
L'instruction de réception de messages consiste en une variable de canal suivie d'un point d'interrogation et d'une séquence de variables.
chan_name ? liste variables
Concrètement, les expressions dans l'instruction d'envoi sont évaluées et leurs valeurs sont transférées à travers le canal; l'instruction réception affecte ces valeurs aux variables spécifiées dans l'instruction. L’opération d’émission n’est exécutable que lorsque le canal en
question n’est pas plein. De même, l’opération de réception n’est exécutable que lorsque le canal en question n’est pas vide (un message est disponible dans le canal). Exemples: proctype A(chan q1) { q1!123; } proctype B(chan q2) { int x; q2?x;
}
init { chan q1 = [1] of {int}; run A(q1); run B(q1); } 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
chan request = [0] of { byte }; active proctype Server() { byte client; end: do :: request ? client -> printf("Client %d\n", cl ient) od } active proctype Client0() { request ! 0 } active proctype Client1() { request ! 1 }
Remarque: •
Par convention, le premier champ d'un message est souvent utilisé pour spécifier le type du message (une constante). Une notation alternative et équivalente pour les opérations d'envoi et de réception de messages est donc de spécifier le type de message, suivi d'une liste de champs de message entre parenthèses: Chan_name! expr1 (expr2, expr3) chan_name? var1 (var2, var3)
Par exemple, compte tenu des déclarations: mtype {open, close, reset}; chan ch = [1] de {mtype , byte, byte}; byte id, n;
une instruction envoie de messages peut être écrite dans l'un des formats suivants: ch! open, id, n; ch! open (id, n);
Remarques: •
L’envoi d’un message dans un canal ne peut avoir lieu que si celui-ci n’est pas encore plein. De même, la réception d’un message ne peut être effectuée que si le canal n’est pas vide. Lorsque ces opérations ne peuvent être réalisées, elles sont bloquantes.
•
Plusieurs fonctions permettent de travailler sur la longueur de la file associée à un canal. Elles effectuent des tests, mais n’ajoutent ni ne retirent de message:
•
Une fonction prédéfinie len(Chan_name) renvoie le nombre de messages actuellement stockés dans le canal chan_name.
•
Les primitives full(nom_canal) et empty(nom_canal) sont des fonctions booléennes prédéfinies qui indiquent si la file associée à nom_canal est pleine ou vide.
•
Les opérations nfull(nom_canal) et nempty(nom_canal) sont des fonctions booléennes prédéfinies qui indiquent si la file associée à nom_canal est non pleine ou non vide.
•
Un canal de communication prédéfini STDIN permet de lire un caractère sur l’entrée standard.
Exemple: chan STDIN; short c; do :: STDIN?c -> if :: c == -1 -> break /* EOF */ :: else -> printf("%c",c) fi od
4. Opérateurs et expressions L'ensemble des opérateurs utilisé dans le langage PROMELA, est présenté dans le tableau ci-dessous; les opérateurs sont presque identiques à ceux des langages similaires à C-. Il est conseillé d'utiliser généreusement les parenthèses pour clarifier la précédence et l'associativité dans les expressions. Opérateur = && ! == != , >=, state = 3 } proctype B() {state = state - 1 } init { run A(); run B() }
L'opérateur d'exécution init peut transmettre des valeurs de paramètres au nouveau processus à créer; seuls les canaux de communication et les instances des cinq types de données de base peuvent être passés en tant que paramètres. Les tableaux et les types de processus ne peuvent pas être transmis. L'opérateur init peut aussi lancer autant de processus de type différent, ou de même type, éventuellement en leur donnant des arguments différents. Il peut être utilisé dans n’importe quel processus pour en créer de nouveaux processus, . Un processus qui s’exécute disparaît lorsqu’il termine, c’est-à-dire lorsqu’il atteint la fin du code à exécuter, mais jamais avant les processus qu’il a lui-même créés. Exemple: 1) proctype A(byte state; short set) { (state == 1) -> state = set } init { run A(1, 3) }
2 ) int b=3; proctype A(int a) { byte x; x = a+b; } proctype B(int m) { byte y=0; (m==3) -> y=(y + b)%8; }
init {run A(2); run B(3); run B(5); }
Remarque: •
Un processus peut être déclaré de manière à s’activer d'une manière implicite au début
de l’exécution. Pour cela le mot-clef active doit précéder proctype. Plusieurs instanciations d’un même processus peuvent également être activées dans l’état initial du système. Ces processus ne sont pas activés avec des arguments. Toutefois, on peut préciser des paramètres formels pour des instanciations ultérieures à partir d’autres processus. Les arguments des processus instanciés par active sont alors initialisés à 0. Exemples: active proctype A() active [4] proctype B() 1 2 3 4 5 6 7 8 9 10 11 12 13
•
{ {
... ...
} }
chan request = [0] of { byte }; active proctype Server() { byte client; end: do :: request ? client -> printf("Client %d\n", cl ient) od } active proctype Client0() { request ! 0} active proctype Client1() { request ! 1}
Par convention, les instructions d'exécution sont incluses dans une séquence atomique pour s'assurer que tous les processus sont instanciés avant que l'un d'entre eux ne commence l'exécution.
•
Il existe une seule variable anonyme globale prédéfinie écrite en utilisant le caractère de soulignement _. La variable remplace les variables "fictives" utilisées dans d'autres langages, et a l'avantage que sa valeur ne fait pas partie des états d'un calcul, donc aucune mémoire n'est requise pour la stocker lors d'une vérification. L'utilisation la plus courante est dans les instructions de réception, où les valeurs de certains ou de tous les champs de messages ne sont pas nécessaires.
Exemple:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
•
chan request = [0] of { byte }; chan reply = [0] of { bool }; active proctype Server() { byte client; end: do :: request ? client -> printf("Client %d\n", client); reply ! true od } active proctype Client0() { request ! 0; reply ? _ } active proctype Client1() { request ! 1; reply ? _ }
La variable prédéfinie _pid est en lecture seule et locale à chaque processus; elle donne un nombre unique à chaque processus à son instanciation. La variable est de type pid et prend des valeurs de 0 à 254 (pas 255).
Exemple: active [3] proctype A() { printf("Je suis le processus numero %d\n",_pid) } 1 byte n = 0; 2 3 active [4] proctype P() { 4 byte temp; 5 temp = n + 1; 6 n = temp; 7 printf("Processus P%d, n = %d\n", _pid , n) 8 }
•
La variable prédéfinie _nr_pr est en lecture seule et globale; sa valeur représente le nombre de processus actifs. Dans la section 3.5 nous avons utilisé l'expression (_nr_pr == 1) dans le processus init pour attendre la fin de tous les autres processus.
Exemple:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
#include "for.h" byte n = 0; proctype P() { byte temp; for (i, 1, 10) temp = n + 1; n = temp rof (i) } init { atomic { run P(); run P() } (_nr_pr == 1) -> printf("The value is %d\ n", n) }
4. Instructions Il y a douze types d'instructions assertion
assignment
atomic
break
expression
goto
printf
receive
selection
repetition
send
timeout
Toute instruction peut être précédée d'une ou plusieurs déclarations. Une instruction ne peut être passée que si elle est exécutable. Pour déterminer son exécutabilité, l'instruction peut être évaluée: si l'évaluation renvoie une valeur nulle, l'instruction est bloquée. Dans tous les autres cas, l'instruction est exécutable et peut être passée. Le fait de passer une instruction après une évaluation réussie s'appelle «l'exécution» de l'instruction. L'évaluation d'une expression composée est toujours indivisible. Exemple: L'instruction suivante est toujours inexécutable (a == b && a != b) mais
(a == b) ; (a != b) peut
être exécutable dans cet ordre.
a) Il y a une pseudo instruction, skip, qui est syntaxiquement équivalente à la condition (1). Skip, est une instruction nulle; elle est toujours exécutable et n'a aucun effet lorsqu'elle est exécuté. Elle peut être nécessaire de satisfaire aux exigences de syntaxe. b) Les instructions Goto peuvent être utilisées pour transférer le contrôle à toute instruction étiquetée dans le même processus. Elles sont toujours exécutables. Chaque instruction peut être précédée d'une étiquette: un nom suivi de deux-points. Chaque étiquette peut être utilisée comme destination d'un goto. c) Les affectations et les déclarations sont également toujours exécutables. e) Les expressions ne sont exécutables que si elles renvoient une valeur non nulle. C'est-à-dire que l'expression 0 (zéro) n'est jamais exécutable et, de même, 1 est toujours exécutable.
4.1. Instructions de contrôle Ce sont des primitives permettant d’effectuer des séquences, des sélections, des répétitions, des branchements. 4.1.1. Séquence: Le point-virgule est le séparateur entre les instructions qui sont exécutées en séquence. Lorsqu'un le programme est exécuté, un registre appelé compteur d'emplacement location counter maintient l'adresse de l'instruction suivante qui peut être exécutée. Une adresse d'instruction est appelée un point de contrôle. Exemple: dans la séquence d'instructions suivante a trois points de contrôle, un avant chaque instruction, et le compteur d'emplacement d'un processus peut être à n'importe lequel d'entre eux. x = y + 2; z = x* y; printf("x = %d, z = %d\ n", x, z)
4.1.2. Instruction de Sélection: Une instruction de sélection commence par le mot réservé if et se termine par le mot réservé fi. Entre les deux, il y a une ou plusieurs alternatives, chacune consistant en un double deux points (::), une instruction appelée garde, une flèche et une séquence d'instructions. (Notez qu'aucun point-virgule n'est requis avant un double deux point ou le fi double) if :: guard1 -> séquence instructions1; :: guard2 -> séquence instructions2; : : :: guardN -> séquence instructionsN; fi;
L'exécution d'une instruction if commence avec l'évaluation des gardes; si au moins une est évalué à vrai, la séquence d'instructions suivant la flèche correspondant à l'une des vrais gardes est exécutée. Lorsque ces instructions ont été exécutées, l'instruction if se termine. Si plus d'une garde est exécutable, l'une des séquences correspondantes est sélectionnée de manière non déterministe. Si toutes les gardes ne sont pas exécutables, le processus se bloquera jusqu'à ce qu'au moins l'une d'entre elles puisse être sélectionnée. Il n'y a aucune restriction sur le type d'instructions qui peuvent être utilisées comme garde.
Exemples: 1 2 3 4 5 6 7 8 9 10 13
active proctype Racine() { int a = 1, b = -4, c = 4; int delta; delta = b * b - 4 * a * c; if :: delta < 0 -> printf("delta = %d: Pas de racines réelles\n", delta) :: delta == 0 -> printf("delta = %d: racines réelles double\n", delta) :: delta > 0 -> printf("delta = %d: Deux racines réelles\n", delta) fi }
6 if 7 8 9 10 fi
:: delta < 0 ; printf("delta = %d: Pas de racines réelles\n", delta) :: delta == 0; printf("delta = %d: racines réelles double\n", delta) :: delta > 0 ; printf("delta = %d: Deux racines réelles\n", delta)
1 active proctype Maximum() { 2 int a = 5, b = 5; 3 int max; 4 int branch; 5 if 6 :: a >= b -> max = a; branch = 1 7 :: b >= a -> max = b; branch = 2 8 fi ; 9 printf("The maximum of %d and %d = %d by branch %d\n", 10 a, b, max, bran ch) 11 }
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
active proctype Date() { byte days; byte month = 2; int year = 2000; if :: month == 1 || m onth == 3 || month == 5 ||month == 7 || mon th == 8 || month == 10 ||month == 12 -> days = 31 :: month == 4 || m onth == 6 || month == 9 || month == 11 -> days = 30 :: month == 2 && year % 4 == 0 && (year % 100 != 0 || year % 400 == 0) -> days = 29 :: else -> days = 28 fi ;
17 printf("month = %d, year = %d, days = %d\n", month, year, days) 18 }
Remarques: •
La garde else signifie que: si et seulement si toutes les autres gardes sont évalués à faux, les instructions suivant le else seront exécutées.
•
La séquence d'instructions suivant une garde peut être vide, auquel cas le contrôle quitte l'instruction if après avoir évalué la garde.
4.1.3. Expression conditionnelle: Une expression conditionnelle permet d'obtenir une valeur qui dépend du résultat de l'évaluation d'une expression booléenne. Elle doit être comprises entre parenthèses. Leur syntaxe est: (expr1 -> expr2 : expr3). Exemple: max = (a > b -> a : b) :: month == 2 && year % 4 == 0 -> days = (year % 100 != 0 || year % 400 == 0 ->29 : 28)
La sémantique des expressions conditionnelles est différente de celle des instructions if. Une instruction d'affectation comme max = (a > b -> a : b) est une instruction atomique, tandis que if ne l'est pas, et l'entrelacement est possible entre la garde et l'instruction d'affectation suivante. if :: a > b -> max = a :: else -> max = b fi
4.1.2. Instruction de Répétition: Une répétition ou une instruction do est similaire à une instruction de sélection, mais elle est exécutée de manière répétée jusqu'à ce qu'une instruction break soit exécutée ou qu'un saut goto transfère le contrôle en dehors de la boucle. La syntaxe de l'instruction de répétition est la même que celle de l'instruction de sélection if, sauf que les mots-clés sont do et od. La sémantique est similaire, consistant en l'évaluation des gardes, suivie de l'exécution de la séquence d'instructions suivant l'un des gardes vraies. Une seule option peut être sélectionnée pour l'exécution à la fois. Pour une instruction do, l'achèvement de la séquence d'instructions provoque le retour de l'exécution au début de l'instruction do et l'évaluation des gardes est recommencée de nouveau. La manière normale de terminer la structure de répétition est accomplie par break, ce qui n'est pas une instruction mais plutôt une indication
que le contrôle passe de l'emplacement actuel à l'instruction suivant od. L'utilisation d'une instruction break en dehors d'une instruction de répétition est illégale. Exemple: 1 2 3 4 5 6 7 8 9 10
active proctype PGCD() { int x = 15, y = 20; int a = x, b = y; do :: a > b -> a = a - b :: b > a -> b = b - a :: a == b -> break od ; printf("The PGCD of %d and %d = %d\n", x, y, a) }
1 #define N 10 2 3 active proctype Somme() { 4 int sum = 0; 5 byte i = 1; 6 do 7 :: i > N -> break 8 :: else -> sum = sum + i; i++ 10 od ; 11 printf("La somme des %d premiers nombres = %d\n", N, sum) 12 } 1 #include "for.h" 2 #define N 10 3 4 active proctype Somme() { 5 int sum = 0; 6 for (i, 1, N) 7 sum = sum + i 8 rof (i); 9 printf("La somme des %d nombres = %d\n", N, sum) 10 }
Remarques: • L'instruction goto peut être utilisé à la place de break pour sortir d'une boucle. bien que normalement break soit préférée car elle est plus structurée et ne nécessite pas d'étiquette. •
Une étiquette ne peut apparaître qu’avant une instruction. Si aucune instruction ne doit être exécutée à partir de cet endroit, on peut utiliser skip qui est une instruction toujours exécutable et sans effet.
•
Il n'y a pas de point de contrôle au début d'une alternative dans une instruction if ou do, c'est donc une erreur de syntaxe de placer une étiquette devant une garde. Au lieu de cela, il existe un point de contrôle "commun" pour toutes les alternatives au début de l'instruction.
1) do :: i > N -> goto exitloop :: else -> ... od ; exitloop: printf(...); 2) start: do :: wantP -> if :: wantQ -> goto start :: else -> skip fi :: else -> ... od 3) proctype PGCD(int x, y) { printf("le PGCD de%d et%d est", x, y) do :: (x > y) -> x = x – y :: (x < y) -> y = y – x :: (x == y) -> goto fin od; fin: printf("%d\n ", x) } init { run PGCD(24,36)}
5. Concurrence des processus Tous les processus lancés par des instanciations run s’exécutent non pas de manière séquentielle mais de manière concurrente. Exemple: Soient trois processus A, B et C contenant chacun trois instructions définis comme suit: proctype A() {
instrA1; instrA2; instrA3; } proctype B() { instrB1; instrB2; instrB3; } proctype C() { instrC1; instrC2; instrC3; } init { run A(); run B(); run (C)}
- Lorsque les processus s’exécutent de manière séquentielle, alors l’ordre d’exécution des instructions est celui ci: processus A instrA1; instrA2; instrA3;
processus B instrB1; instrB2; instrB3;
processus C instrC1; instrC2; instrC3;
- Par contre, lorsque les processus s’exécutent de façon concurrente, on ne connaît pas a priori l’ordre dans lequel les instructions seront exécutées dans les différents processus. L’ordre peut très bien être l’ordre séquentiel, mais les instructions pourront aussi être entrelacés plus ou moins régulièrement. comme l'exemple ci-dessous: processus A instrA1;
processus B
processus C instrC1;
instrA2; instrB1; instrB2; instrA3; instrB3; instrC2; instrC3;
Il en résulte que, de la même manière que pour les systèmes distribués, si on n’étudie pas explicitement la synchronisation des processus, on pourra observer des résultats aléatoires. byte state = 1;
proctype A() { (state==1) -> state = state+1; } proctype B() { (state==1) -> state = state-1; } init { run A(); run B();}
L'exécution de ce programme peut s'effectuer de plusieurs manières et ainsi donner différents résultats comme par exemple: processus A (state==1); state = state+1;
processus B
(state==1); (state==1); state = state-1; (state==1);
Variable globale State 2 Processus B est bloqué 0 Processus A est bloqué
(state==1); (state==1); state = state+1; state = state-1;
2 1
5.1. Séquence atomique Les instructions dans PROMELA sont atomiques. À chaque étape, l'instruction pointée par le compteur d'emplacement d'un certain processus (arbitraire) est exécutée dans son intégralité (Les expressions en Promela sont des instructions). Le défi d'écrire des programmes concurrents ne vient pas seulement de l'entrelacement en tant que tel, mais plutôt de l'interférence entre les processus qui peuvent causer des erreurs vraiment bizarres. Exemple: if :: a != 0 -> c = b / a /* Une possible division par 0. :: else -> c = b fi
1 byte n = 0; 2 3 active proctype P() { 4 byte temp; 5 temp = n + 1; 6 n = temp;
7 8 9 10 11 12 13 14 15
1 2 3 4 5 6 7 8 9 10 11 12 13
printf("Process P, n = %d \n", n) } active proctype Q() { byte temp; temp = n + 1; n = temp; printf("Process Q, n = %d \n", n) }
byte n; active proctype P() { byte temp; temp = n + 1; n = temp; printf("Process P, n = %d \n", n) } init { n = 0; run P(); run P() }
Dans PROMELA, il existe un des moyens d'éviter le problème de tester-affecter est d'utiliser les séquences atomiques. Une séquence atomique est séquence d'instructions entre parenthèses, préfixée par le mot-clé atomic, indique que la séquence doit être exécutée comme une unité indivisible, non entrelacée avec d'autres processus. En effet dans une séquence atomique, toutes les instructions doivent être exécutables, sauf éventuellement la première. Dans le cas, contraire, si une instruction dans la séquence n’est pas exécutable, alors il s’agira d’un deadlock, car aucun autre processus ne pourra rendre cette instruction exécutable et débloquer la situation. Exemple: byte state = 1; proctype A() { atomic {(state==1) -> state = state+1 } } proctype B() { atomic { (state==1) -> state = state-1 } } init { run A(); run B();}
Dans ce cas, la valeur finale de state est 0 ou 2, selon le processus exécuté. L'autre processus sera bloqué pour toujours. Les séquences atomiques peuvent être un outil important pour réduire la complexité d'un modèle de validation. Une séquence atomique limite la quantité d'entrelacement qui est autorisée, ce qui peut effectivement rendre des modèles de validation complexes traitables, sans perte de généralité.
5.2. Modélisation du Timeout Une instruction prédéfinie timeout (délai d'expiration) est une instruction qui modélise une condition spéciale qui permet à un processus d'interrompre l'attente d'une condition qui ne peut plus être vraie, par exemple une entrée provenant d'un canal vide. Le mot-clé timeout est une fonction de modélisation qui permet d'échapper à un état de blocage Il est commode de considérer le timeout comme similaire à un global else: alors que else est exécutable lorsqu'il n'y a pas de gardes exécutables dans les instructions
if
ou do, timeout devient vraie
uniquement lorsqu'aucune autre instruction dans le système distribué n'est exécutable. Notez que cette instruction ne véhicule aucune valeur: elle ne spécifie pas d'intervalle de temps (de délai), mais une possibilité de dépassement de délai. Exemple: Le processus suivant envoie un message de réinitialisation à un canal nommé guard chaque fois que le système s'arrête(s'immobilise). proctype watchdog() { do :: timeout -> printf("Reject.....\n") od}
Exemple: Dans la séquence ci-dessus, si rien ne peut être lu dans le canal qchan et si tous les autres processus sont bloqués, alors timeout devient exécutable et permet de sortir de la boucle. do :: qchan?var; :: timeout -> break; od
5.3. Synchronisation par Rendez-vous La communication asynchrone entre les processus se fait via les canaux de communication, déclarés par exemple par: chan qname = [N] of { byte } où N est constante positive qui définit la taille du buffer. Un canal déclaré avec une capacité de zéro : chan qname = [0] of { byte }
permet de définir un canal de rendez-vous qui ne peut que transmettre et non
stocker des messages. Cela signifie que le transfert du message de l'expéditeur (un processus avec une instruction d'envoi) au destinataire (un processus avec une instruction de réception) est synchrone et exécuté comme une seule opération atomique. Les interactions de messages via de tels ports de rendez-vous sont par définition synchrones. Exemple: chan name = [0] of { byte, byte }; byte name; proctype A() { name!msgtype(124); name!msgtype(121) } proctype B() { byte state; name?msgtype(state) } init { atomic { run A(); run B() } }
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
mtype { red, yellow, gre en }; chan ch = [0] of { mtype, byte , bool }; active proctype Sender() { ch ! red, 20, false; printf("Sent message\n ") } active proctype Receiver() { mtype color; byte time; bool flash; ch ? color, time, f lash; printf("Received mess age %e, %d, %d\n",color, time, flash) }
1 chan request = [0] of { byte }; 2 3 active proctype Server() {
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
byte client; end: do :: request ? client -> printf("Client %d\n", cl ient) od } active proctype Client0() { request ! 0 } active proctype Client1() { request ! 1 }
La communication par rendez-vous est binaire: seulement deux processus, un émetteur et un récepteur, peuvent être synchronisés de cette manière.
5.4. Procedures et fonctions Bien que PROMELA ne dispose pas de fonctions ou de procédures pour structurer le code des programmes, il peut être pratique de regrouper les instructions afin qu'elles puissent apparaître à plusieurs endroits dans un programme. Ceci est fait en utilisant la construction inline en dehors des déclarations de processus, qui donne un nom à une séquence d'instructions. inline Procedure_name(liste de paramètres formels){ ... code Promela ... } ... Procedure_name(liste de paramètres effectifs); ...
Lorsque le nom de la séquence inline est utilisé dans un processus proctype, les instructions entre les accolades sont copiées dans la position correspondante avant la compilation. Pendant la copie, les paramètres formels apparaissant après le nom de la séquence inline sont remplacés par les paramètres effectifs (réels de l'appel). Il n'y a pas de déclaration de type associée au paramètre formel car la substitution textuelle est effectuée sans aucun contrôle syntaxique ou sémantique. Tout problème provoqué par la substitution ne
sera trouvé que lors de la compilation ultérieure du code source PROMELA résultant. inline est très utile pour initialiser les structures de données. Exemple: 1 2 3 4 5 6 8 9 10 11 12 13 14 15 16 17 18 19 20 21
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
#define N 5 inline write(ar) { byte k=0; do :: k >= N -> break :: else -> printf("%d ", ar[k]); k++ od ; printf("\n") } active proctype P() { int a[N]; byte i=0; write(a); do :: i >= N -> break :: else -> a[i] = i; i++ od ; write(a) }
#define N 4 typedef ENTRY { byte row; byte col; int value } ENTRY a[N]; inline initEntry(I, R, C, V) { a[I].row = R; a[I].col = C; a[I].value = V; } active proctype P() { int i = 0; int r,c; initEntry(0, 0, 1, -5); initEntry(1, 0, 3, 8); initEntry(2, 2, 0, 20); initEntry(3, 3, 3, -3); r=0; do :: r >= N -> break :: else -> c=0; do :: c >= N -> break :: else ->
24 25 26 27 28 29 30 31 32 33 34
if :: i == N -> printf("0 ") :: i < N && r == a[i].row && c == a[i].col -> printf("%d ", a[i].valu e); i++ :: else -> printf("0 ") fi; c++; od; r++ od; }
6. Vérification des systèmes Le langage Promela est un langage de haut niveau d'abstraction qui permet de se concentrer sur la conception plutôt que sur les problèmes de mise en œuvre. Les programmes qui peuvent être écrits dans ce langage sont donc appelés modèles de vérification. En réalité, un système, d’un point de vue intrinsèque, n’est ni correct, ni incorrect. Il a un certain comportement et c’est à l’utilisateur de spécifier ce qu’il entend par un comportement correct. Un système qui s’arrête et n’évolue plus est soit terminé, soit bloqué (deadlock). Mais c’est à l’utilisateur de spécifier au vérificateur que cet état n’est pas l’état dans lequel le protocole devrait s’arrêter. Il en va de même pour le bouclage et autres phénomènes. Pour vérifier un système, nous devons être en mesure de spécifier avec précision ce que cela signifie pour un système pour être correct. Une conception peut être prouvée qu'elle est correcte uniquement si elle respecte des critères d'exactitude spécifiques tels que l'absence de blocages, de bouclages infinis et de terminaisons impropres. Nous avons besoin d'un formalisme pour spécifier ces propriétés d'exactitude. L'ensemble des propriétés d'exactitude qui peuvent être exprimés dans PROMELA est donc choisi avec soin. Cet ensemble n'est délibérément pas limité à un seul mécanisme toutpuissant. Plusieurs niveaux de complexité indépendants sont pris en charge. Les exigences les plus simples et les plus fréquemment utilisées, telles que l'absence de blocage, sont exprimées directement et vérifiées indépendamment des autres propriétés. Des types d'exigences légèrement plus compliqués, tels que l'absence de bouclages infinis, sont exprimés indépendamment, et portent une étiquette indépendante. Les exigences les plus sophistiquées sont inévitablement aussi les plus chères à vérifier. Dans les sections suivantes, un aperçu des types de critères de correction pouvant être exprimés pour les modèles PROMELA est donné. Ces sections montrent les structures du langage PROMELA nécessaires pour exprimer chaque propriété et donne quelques exemples de son utilisation.
6.1. Raisonnement sur le comportement Les critères de correction (les propriétés de correction) sont formalisés sous forme d'allégations sur le comportement d'un modèle PROMELA. Deux types généraux d'allégations sont formulés; un comportement donné est soit inévitable ou impossible. Étant donné que le nombre de comportements possibles d'un modèle PROMELA donné est limité,
toutefois, une revendication de l'un ou l'autre type définit implicitement une revendication complémentaire et équivalente de l'autre type. Il suffit donc de n'en supporter qu'une seule. "Toutes les propriétés de correction pouvant être exprimées dans PROMELA définissent des comportements qui sont revendiqués comme impossible." Pour affirmer qu'un comportement donné est inévitable, il suffit d'affirmer que tous les comportements déviants sont impossibles. De même, si une assertion de correction indique qu'une condition est invariablement vrai, les déclarations de correction indiquent qu'il est impossible de violer l'assertion, indépendamment du comportement du système. Le comportement d'un modèle de validation est complètement défini par l'ensemble de toutes les séquences d'exécution qu'il peut exécuter, une séquence d'exécution étant simplement un ensemble fini et ordonné d'états. Un état, à son tour, est complètement défini par la spécification de toutes les valeurs des variables locales et globales, de tous les points de contrôle de flux des processus en cours d'exécution et du contenu de tous les canaux de message. Un modèle de validation peut atteindre un état donné en exécutant des instructions PROMELA, en utilisant la sémantique de l'exécutabilité. Un modèle de validation peut également être placé dans un état donné suite à une affectation des valeurs appropriées aux variables, points de flux de contrôle et canaux. Bien entendu, toute séquence d'états arbitraire n'est pas nécessairement une séquence d'exécution valide. Un ensemble fini et ordonné d'états est une séquence d'exécution valide pour un modèle PROMELA donné M s'il répond aux deux critères suivants: o Le premier état de la séquence, c’est-à-dire l’état avec le nombre ordinal 1, est l’état initial du système de M, toutes les variables étant initialisées à zéro, tous les canaux de messages vides, seul le processus init étant actif et défini dans son état initial. o Si M est placé dans l'état avec le nombre ordinal i, il existe au moins une instruction exécutable qui peut l'amener à l'état avec le nombre ordinal i+1. Deux types spéciaux de séquences sont distingués, appelées séquences terminales et cycliques. •
Une séquence d'exécution est dite terminale si aucun état ne survient plus d'une fois dans la séquence, et le modèle M ne contient aucune instruction exécutable lorsqu'il est placé dans le dernier état de la séquence.
•
Une séquence d'exécution est dite cyclique si tous les états sauf le dernier sont distincts et si le dernier état de la séquence est égal à l'un des états antérieurs.
Les séquences cycliques définissent des exécutions potentiellement infinies. Toutes les séquences d'exécution terminales et cycliques pouvant être générées par l'exécution d'un modèle PROMELA définissent ensemble le comportement système de ce modèle. L'union de tous les états inclus dans le comportement du système s'appelle l'ensemble d'états accessibles du modèle.
6.1.1. Propriétés des états Les propriétés de correction des modèles PROMELA peuvent être construites à partir de propositions simples, une proposition étant une condition booléenne de l'état du système. Les propositions peuvent faire référence à tous les éléments d'un état système: variables locales et globales, points de contrôle de flux des processus en cours d'exécution arbitraires et contenu des canaux de message. Les propositions définissent implicitement un étiquetage des états. Dans un état donné, une proposition est vraie ou fausse. Les critères de correction peuvent ensuite être exprimés en termes d'états, par exemple, en définissant explicitement les états dans lesquels une proposition donnée doit être conservée. Certaines de ces exigences peuvent être spécifiées dans PROMELA avec, par exemple, des instructions d'assertion incorporées dans le modèle. Ce mécanisme en lui-même n'est toutefois pas suffisant. Si plusieurs propositions sont utilisées, une propriété de correction peut exprimer en tant qu’ordre temporel des propositions, c’est-à-dire en spécifiant l’ordre dans lequel les propositions doivent être vérifiées (avec la vérité d’une proposition soit immédiatement ou éventuellement à la suite de la vérité d'une autre). L'ordonnancement temporel peut également définir l'ordre dans lequel les propositions ne doivent jamais être respectées. Comme indiqué ci-dessus, ces deux alternatives pour définir des ordres temporels sont complémentaires. Seule la deuxième alternative est prise en charge dans PROMELA. Le formalisme pour supporter ceci est une nouvelle fonctionnalité du langage appelée revendication temporelle. Dans la formalisation des propriétés temporelles, un ordre des propositions est spécifié. Il est important de noter que la sémantique de cet ordre des propositions est différente de celle de l'ordre des instructions dans un modèle PROMELA. Dans la définition d'un processus PROMELA, un ordre séquentiel de deux instructions implique que la deuxième instruction sera exécutée après la fin de la première. Etant donné qu'aucune
hypothèse sur les vitesses relatives aux processus en exécution simultanée et concurrente n'est émise, la seule interprétation valable du mot après est éventuellement après. Les propriétés de correction doivent être plus spécifiques. Dans une propriété temporelle, un ordre séquentiel de deux propositions définit une conséquence immédiate. Les types de propriétés de correction peuvent être différents pour les séquences terminales et cycliques, de même que les algorithmes nécessaires pour vérifier ces propriétés. Une spécification importante appliquée aux séquences de terminaison est, par exemple, l’absence d’impasse (interblocage). Cependant, toutes les séquences de terminaison ne correspondent pas à des blocages. Il faut être en mesure d’exprimer quelles propriétés l’état final d’une séquence doit avoir pour que cette séquence soit acceptable en tant que séquence de terminaison sans interblocage. Enfin, pour les séquences cycliques, il faut être en mesure d'exprimer des conditions générales telles que l’absence de boucles infinies (livelock). Les instructions décrites dans les sections suivantes facilitent la validation d’un système. Il s’agit d’assertions et de caractéristiques particulières d’états, qui doivent être satisfaites pour que le comportement du système soit correct.
6.2 Assertions Les critères de correction peuvent souvent être exprimés sous forme de conditions booléennes qui doivent être satisfaites chaque fois qu'un processus atteint un état donné. Les assertions sont des instructions composées du mot clé assert suivi d'une expression booléenne. L’instruction de PROMELA assert (expression booléenne)est toujours exécutable et peut être placé n’importe où dans un modèle PROMELA. La condition peut être une expression booléenne arbitraire. Lorsqu'une instruction assert est exécutée pendant une simulation, l'expression est évaluée. Si la condition est vraie, l'instruction n'a aucun effet et l'exécution passe normalement à l'instruction suivante. La validité de la l'instruction est violée, s'il y a au moins un séquence d'exécution dans laquelle la condition est fausse dans ce cas le programme se termine avec un message d'erreur. L'espace d'états d'un programme est l'ensemble des états pouvant éventuellement se produire lors d'un calcul. Dans la vérification de modèle, l'espace d'états d'un programme est généré afin de rechercher un contre-exemple - s'il en existe un - correspondant aux spécifications d'exactitude.
Les assertions peuvent être placées entre deux instructions quelconques d'un programme et le vérificateur de modèle les évaluera dans le cadre de la recherche de l'espace d'états. Si, au cours de la recherche, il trouve un calcul menant à une fausse assertion, le programme est incorrect ou l'assertion n'exprime pas correctement une propriété de correction qui est valable pour le programme. Exemple: byte state = 1; proctype A() { (state==1) -> state = state+1; } proctype B() { (state==1) -> state = state-1; } init { run A(); run B();}
On peut essayer de prétendre que lorsqu'un processus de type A () se termine, la valeur de variable state doit être 2 et lorsqu'un processus de type B () se termine, elle doit être 0. Cela peut être exprimé comme suit: byte state = 1; proctype A() { (state==1) -> state = state+1; assert(state==2) } proctype B() { (state==1) -> state = state-1; assert(state==0) } init { run A(); run B();}
Bien entendu, les allégations faites sont totalement fausses et le vérificateur SPIN le démontrera rapidement.
6.3 Invariants système Une application plus générale de l'instruction assert consiste à formaliser les invariants système, c'est-à-dire des conditions booléennes qui, si elles sont vraies dans l'état initial du
système, restent vraies dans tous les états accessibles du système, indépendamment de la séquence d'exécution menant à chaque état spécifique. L'expression de ces invariants dans PROMELA consiste à placer l'invariant du système lui-même dans un processus de surveillance distinct.
proctype monitor() { assert(invariant) }
Une fois qu'une instance du processus de type moniteur a été démarrée (le nom n'a pas d'importance), avec une instruction d'exécution run, il s'exécute indépendamment du reste du système. Il peut décider d'évaluer l'assertion à tout moment; son instruction assert est exécutable précisément une fois pour chaque état du système. Exemple: considérons le modèle de validation des sémaphores de dijkstra #define p 0 #define v 1 chan sema[0] of {bit}; proctype dijkstra() { do : : sema!p -> sema?v od} proctype user() { sema?p; sema!v
/* section critique */ /* section non critique */}
init { atomic { run dijkstra(); run user(); run user(); run user()} }
Le sémaphore garantit un accès mutuellement exclusif des processus utilisateur à leurs sections critiques. Les processus utilisateurs user() peuvent être modifiés comme suit, une variable globale count est utilisée pour compter le nombre de processus dans la section critique. byte count; proctype user() { sema?p; count = count+1; skip; count = count-1; sema!v; skip }
/* section critique */ /* section non critique */
L'invariant système suivant peut être utilisé pour vérifier le bon fonctionnement du sémaphore:
proctype monitor() { assert(count == 0 || count == 1) }.
Une instanciation du
processus monitor doit être incluse dans le processus init pour lui permettre de vérifier la propriété de correction.
init { atomic {
run dijkstra(); run monitor(); run user(); run user(); run user()}
}
6.4 Interblocage (DeadLock) Lorsque PROMELA est utilisé comme langage de validation, l'utilisateur doit être en mesure de formuler des assertions très spécifiques sur le comportement modélisé. En particulier pour vérifier la présence d'interblocage dans un modèle PROMELA. Dans un système à états finis, toutes les séquences d'exécution se terminent après un nombre fini de transitions d'états ou reviennent à un état précédemment visité. Cependant, toutes les séquences terminales ne sont pas nécessairement des blocages. Afin de définir ce que c'est un interblocage dans un modèle PROMELA, le vvérificateur doit être en mesure de distinguer entre les états finaux attendus (normaux) et les états inattendus (anormaux). Un état de terminaison normale (final normal) dans une séquence d'exécution finale est un état dans lequel chaque processus instancié a correctement atteint la fin du code le définissant et où tous les canaux de message sont vides. Cependant, tous les processus ne sont bien sûr pas censés atteindre la fin de leur code. Certains peuvent très bien rester au repos à attendre une réception éventuelle, ou patienter en boucle, prêts à passer à l'action dès l'arrivée de nouvelles informations. Pour indiquer clairement au validateur que ces autres états finaux sont légaux et ne constituent pas un interblocage, un modèle PROMELA peut utiliser des étiquettes d’états finaux ou terminaux.
Exemple: Les processus serveur ne se terminent pas nécessairement après la fin des processus utilisateur. Mais Ils sont parfaitement correct. Par conséquent, il est nécessaires d'identifier ces états dans le corps du processus comme étant des états finaux valides. Dans PROMELA, cela peut être effectué avec des étiquettes d'états finaux. Exemple: L'exemple du sémaphore peut être décrit comme suit: proctype dijkstra() {end: do : : sema!p -> sema?v od}
S'il existe plusieurs états finaux possibles dans la définition d'un même processus. Toutes les noms d'étiquette doivent être uniques au sein d'un processus. Par conséquent, une étiquette d'état final est définie comme étant tout nom d'étiquette commençant par end par exemple: end_a, end0, end1, end_pr. Donc un état final normal est défini par: Chaque processus instancié a terminé son exécution ou a atteint un état marqué comme état final valide. Tout état final dans une séquence d'exécution terminale qui ne satisfait pas les deux critères pour les états finaux corrects est automatiquement classé comme un état final incorrect. Une propriété de correction implicite qui est faite à propos de tous les modèles de validation sera que les comportements qu’ils définissent ne comprennent pas d’états finaux invalides.
6.5 Mauvais cycles (Bad cycles) Deux propriétés des séquences cycliques peuvent être exprimées dans PROMELA, correspondant à deux types standard d’exigences de correction. Les deux propriétés sont basées sur le marquage explicite des états dans un modèle de validation. La première propriété spécifie qu'il n'y a pas de comportement infini des états non marqués; c'est-à-dire que le système ne peut pas infiniment faire passer par les états non marqués. Les états marqués sont appelés des états de progression et les séquences d'exécution qui enfreignent la propriété de correction ci-dessus sont appelées des cycles sans progression. La deuxième propriété est l'opposé de la première. Elle est utilisée pour spécifier qu'il n'y a pas de comportements infinis qui incluent des états marqués. Les séquences d'exécution qui violent cette propriété sont appelées livelocks.
6.5.1 Cycles sans progression Pour vérifier l'absence de cycles sans progression, if faut définir les états du système dans le modèle PROMELA indiquant la progression. Ces états de progression sont définis comme les étiquettes d’états finaux. Les étiquettes d’états de progression indiquent des états qui doivent être exécutés pour que le processus progresse. Un exemple peut être l’incrémentation d’un numéro de séquence ou la délivrance de données à un destinataire. Tout cycle infini dans l'exécution du processus
qui ne passe pas par au moins un de ces états de progression constitue une boucle de famine potentielle. Les noms des étiquettes d’états de progression doivent commencer par progress dans le cas de l'existence de plusieurs états de progression au sein du même processus. Dans l'exemple de sémaphore de dijkstra, le passage réussi du test de sémaphore peut être qualifié par une progression et il est étiqueté par un état de progression "progress". La propriété de correction peut exprimer que le passage de la condition du sémaphore ne peut être différé infiniment, par exemple, par un cycle d'exécution infini qui ne passe pas l'état de progression. proctype dijkstra() {end: do : : sema!p -> progress: sema?v od}
6.5.2 Les boucles et étiquettes accept Un bouclage peut parfaitement être un comportement correct. Pour exprimer le contraire d’une condition de progression, par exemple, formaliser le fait que quelque chose ne peut pas se produire à l’infini c'est-à-dire spécifier qu’un bouclage n’est pas un comportement correct. Nous pouvons exprimer de telles propriétés avec la troisième et dernière classe d'étiquettes spéciales en PROMELA. Ces étiquettes sont nommés les étiquettes d'état d'acceptation. Une étiquette d’état d’acceptation est une étiquette commençant par "accept". Elle indique un état qui ne peut pas faire partie d’une séquence d’états pouvant être répétée d'une manière à l’infini. Ainsi, pour le vérificateur, toute boucle infinie contenant cette instruction sera considérée comme une erreur de description du processus. Le vérificateur montrera un scénario menant à cette situation de bouclage. Par exemple, si on remplace l'étiquette d'état de progression dans le processus dijkstra() par une étiquette d'état d'acceptation. Cette propriété affirme qu'il est impossible de parcourir une série d'opérations p et I. Cette affirmation est fausse.: proctype dijkstra() {end: do : : sema!p -> accept: sema?v od}
En principe, on peut utiliser au mieux un état d'acceptation pour exprimer des comportements devant être impossibles, plutôt que simplement l'absence d'un état désigné dans tous les cycles.