1
Lanagae promela
PRÉSENTÉ PAR :
MEZOUAR ABDERRAHMANE MONSEF
BENACHI BOUCHRA
2
Ï page web : http://spinroot.com/spin/whatispin.html
cours en ligne avec plus d’informations :
http://lipn.univ-paris13.fr/~petrucci/poly_spin.ps.gz
3
introduction
Promela (PROcess MEta LAnguage) : langage de spécification utilisé par
le model checker SPIN
SPIN : Simple Promela INterpreter I
parmi les model checkers les plus utilisés I
développé par G. Holzmann (Bell Labs, NASA JPL) I
ACM Software Award 2001
Deux modalités d’utilisation I
simulateur
vérifieur
4
promela
Il ne s’agit pas d’un langage d’implémentation (tel que C, Java), mais de
spécification.
Modélisation de la synchronisation et de la coordination des tâches, pas
de la computation.
Promela : pas un langage de programmation, mais un langage pour construire
des modèles de vérification.
Un modèle de vérification n’est qu’une abstraction d’un désign
qui ne contient que les aspects qui sont importants pour les propriétés qu’on
veut vérifier.
Un modèle de vérification contient souvent des choses qui ne font pas
partie de l’implémentation
5
promela
Beaucoup de la notation de Promela dérive du langage C (mais pas
tous)
Un modèle de Promela ne contient que 3 type d’objets de base :
tâches (proctype) I
objets de données I
canaux `a messages
Chaque programme contient au moins un objet de type proctype et (au
moins) une instanciation de cet objet
6
Taches :création
proctype : déclaration d’une tâche
active [3] : instanciation de trois tâches
active [2] proctype you_run(){ /*2 taches de type you_run*/ printf("my pid is: %d\n", _pid); }
_pid : unique id de la tâche
de 0 `a ...
l’exécution des tâches est asynchrone
$ spin you_run.pml
my pid is: 1
my pid is: 0
2 processes created
et $
spin you_run.pml
my pid is: 0
my pid is: 1
2 processes created
7
Taches :création
run : n’importe quelle tâche peut créer une nouvelle tâche
proctype you_run2(byte x){ /*2 taches de type you_run2*/
printf("x = %d, pid = %d\n",x, _pid);
}
init{
run you_run2(0);
run you_run2(1);
}
La tâche init est aussi créé.
Les paramètres de you_run2 sont initialisés par run (pas possible en
utilisant active, tous paramètres initialisés `a 0)
Tâche 6= fonctions : exécutés de façon asynchrone
8
Taches :création
Attention : run est un opérateur
une instruction run est une expression
renvoie une valeur de type pid
proctype you_run3(byte x){ /*2 taches de type you_run3*/
printf("x = %d, pid = %d\n",x, _pid);
}
init{
pid p0, p1;
p0 = run you_run3(0);
p1 = run you_run3(1);
printf("pids: %d and %d\n", p0, p1);
}
9
Nombre de taches
active proctype splurge(int n){
pid p;
printf("n = %d\n", n);
p = run splurge(n+1);
}
on peut avoir jusqu’`a 256 tâche au même temps
une tâche termine alors qu’il atteint la fin de son code (g)
une tâche meurt (et il est supprimé) si tous les tâches instanciés après
sont
aussi morts
10
Taches : provided
provided : contraint l’exécution des tâches
11
Données: types des données de base
short, int et unsigned correspondent aux mêmes plages de C
byte, chan, mtype, et pid correspondent aux plages de unsigned char
de C
12
Données: types des données de base
Toutes les variables (tableaux inclus) sont initialisées à 0
Les tableaux multidimensionnels sont introduits avec la définition des
structures
13
Données: structure
On peut introduire des données structurées (similaire au C)
typedef Field{
14
Données: structure
typedef peut être utilisé pour introduire des tableaux multi-dimentionels
typedef Array{
byte el[4];
};
Array a[4];
On peut faire référence aux éléments de a par a[i].el[j]
15
Canaux a message
Déclaration :
chan qname = [16] of {short, byte, bool};
Envoie des messages :
qname!exp1,exp2,exp3;
exécuté seulement si le canal qname n’est pas plein
autrement, la tâche est bloquée
Réception des messages :
qname?var1,var2,var3;
exécuté seulement si le canal qname n’est pas vide
Notation équivalent :
qname!exp1(exp2,exp3);
qname?var1(var2,var3);
16
Canaux a message : protocole des
bits alternative
option -c pour afficher les opérations d’envoie et réception dans des
colonnes.
option -un pour limiter les pas affichés `a n
17
Canaux a message
Fonctions prédéfinies sur les canaux :
len(qname) = nombre de messages dans le canal
empty(qname) = vrai si le canal est vide
nempty(qname) = vrai si le canal n’est pas vide
full(qname) = vrai si le canal est plein
nfull(qname) = vrai si le canal n’est pas plein
Expressions sur les canaux :
qname?[msg0] = vrai si qname?msg0 est exécutable
qname![msg1] = vrai si qname!msg1 est exécutable
18
Canaux a message :rendez-vous
Déclaration de canaux de longueur 0 :
chan port = [0] of {byte};
Exemple :
mtype = {msgtype};
chan name = [0] of {mtype, byte };
active proctype A(){
name!msgtype(124);
name!msgtype(121);
}
active proctype B(){
byte state;
name?msgtype(state);
}
19
Canaux a message
Les variables de type chan peuvent être envoilées telles que les autres
variables
mtype = {msgtype};
chan glob = [0] of { chan };
active proctype A(){
chan loc = [0] of {mtype, byte};
glob!loc;
loc?msgtype(121);
}
active proctype B(){
chan who;
glob?who;
who!msgtype(121);
}
20
Flux de controle
Instructions de base :
Printf
Affectations
envoie et réception de messages
Instructions composées :
séquences atomiques (atomic)
pas déterministes (d_step)
sélections (if)
répétitions (do)
21
Séquences atomique :producteur
consomateur
Attention : nfull(qname) -> qname!msg0 n’est pas toujours exécutable.
22
Pas deterministes
Similaires aux séquences atomiques
Comparez
atomic { /* échange les valeurs de a et b
tmp = b;
b = a;
a = tmp;
}
avec
d_step { /* échange les valeurs de a et b
tmp = b;
b = a;
a = tmp;
}
Exécutée telle qu’une instruction unique
Différences avec atomic :
exécution déterministe
pas d’instruction goto au-dedans
l’exécution n’est peux pas être bloquée
23
sélection
Choix non-déterministe parmi les énoncés stmti pour lesquels gi est vraie
L’instruction if - fi bloque si aucune garde est vraie
I les taches parallèles peuvent débloquer une tâche en changeant la valeur
d’une variable partagée
I exemple : si y = 0, if :: y > 0 ! x := 42 fi attend jusqu’`a que y est plus
grand que 0
Abréviations standard :
I if g then stmt1 else stmt2 fi ≡ if :: g ! stmt1 :: else ! stmt2 fi
I if g then stmt1 fi ≡ if :: g ! stmt1 :: else ! skip fi
24
Sélection :exemple
Choix non-déterministe :
mtype = {a, b};
chan ch = [1] of { mtype };
active proctype A(){
ch?a;
}
active proctype B(){
ch?b;
}
active proctype C(){
if
:: ch!a;
:: ch!b;
fi
}
25
répétition
Exécution répétée d’un choix non-déterministe parmi les énoncés stmti
pour lesquels gi est vraie
Pas de blockage si aucune garde n’est vraie, par contre on sort de la
boucle
Abréviations standard :
while g do stmt1 od ≡ do :: g ! stmt1 od
26
Répétition :exemple
Compteur :
byte count;
active proctype counter(){
do
:: count++;
:: count--;
:: (count == 0) -> break;
od
}
Algorithme d’Euclide :
proctype Euclid(int x, y){
do
:: (x > y) -> x = x - y;
:: (x < y) -> y = y - x;
:: (x == y) -> break;
od;
printf("réponse: %d\n", x);
}
init{
run Euclid(36,12);
}
27
Types d’Objets
tâches
données
canaux à messages
Flux de Contrôle
Affectations
envoie et réception de messages
séquences atomiques (atomic)
pas déterministes (d_step)
sélections (if)
répétitions (do)
