Génération de code à partir de
spécifications de systèmes
communicants
S. Löffler
J-P. Cottin
A. Serhrouchni
Universität
Stuttgart
GL97 - 4 Décembre 1997
O. Cherkaoui
Plan










The Steam Boiler Control Specification Problem
Tâches du programme de contrôle
Courte présentation de Promela/SPIN
Spécification en Promela
Processus de développement
Simulation,Validation et Implémentation
Le compilateur
Non-Déterminisme durant l’exécution / Ordonnancement
Résultats - Implémentations distribuées
Conclusions et prospectives
Spécification du problème
de la chaudière à vapeur




Présenté à Dagstuhl lors de
“Methods for Semantics and
Specification” en juin 95
Problème réaliste, très informel
Aucun Détail (Format des
messages, Comportement
physique exact)
Nécessité de valider le
Programme de Contrôle et pas
seulement le Protocole.
Niveau
de vapeur
M2
N2
Chaudière
N1
M1
Contrôleur Pompe
de pompe
Valve
Programme de Contrôle
Tâches du programme de Contrôle







Maintenir le niveau d’eau entre N1 et N2
Le système serait endommagé si le niveau d’eau est en dessous / au
dessus de M1 / M2 pendant plus de 5 sec.
Mode Initialisation: attends les unités physiques pour être prêt.
Mode Normal: l’eau est entre les niveaux N1 et N2
Mode Dégradé: lors d’une anomalie d’un capteur
Mode de sauvetage: tentative de maintenir le système malgré les
anomalies des capteurs. Estimations des niveaux.
Mode d’arrêt d’urgence: arrêt de toutes les opérations du
système suite à un des multiples problèmes prévus.
Cycle de fonctionnement

5 Modes de fonctionnement: Initialisation, Normal,
Secours, Dégradé et Arrêt.
I
D
N
S
A
Détection de pannes prévisibles

Pompe



Contrôleur de pompe



Non indication d ’un ordre de changement d’état
Indication incohérente de changement d’état
Unité de mesure du niveau ou de la vapeur



Non respect d ’un ordre d’ouverture ou de fermeture
Changement spontanée d’état
Valeur indiquée hors limite
Valeur incompatible avec la dynamique du système
Transmission


Réception d’un message inattendu
Non réception d ’un message indispensable
Dynamique du système
v: quantité de vapeur q: quantité d’eau
W
U 2 
 v (t )
t
U1
U1
Quantité
de vapeur
-U2
0
temps
t
q (t )  q ( 0 ) 

t
P ( X ) dx 
0
 v ( x ) dx
0
  on a v ( t   )   .U 2  v ( t ) et  

 v (t )
t
 U 2 dt  v ( t )  U 2 t  Cst
v ( t   )   .U 1  v ( t )
t 
q (t ) 
 P ( x ) dx  
t
t 
haut
( v ( t ), v ( t   ),  )  q ( t   )  q ( t ) 
 P ( x ) dx  
t
bas
( v ( t ), v ( t   ),  )
Promela/SPIN






Développé par Gerard Holzmann chez AT&T (« The Design and
Validation of Computer Protocols »). Domaine Public.
Promela = Protocol Meta Language. Langage de spécification
basé sur les machines à états communicantes.
SPIN = Simple Promela Interpreter. Outil de simulation et de
validation de spécifications écrites en Promela.
L’analyseur permet plusieurs types de vérifications: Deadlocks,
Assertions, Livelocks, code mort, règles de logique temporelle,...
Un outil graphique (Xspin) permet de visualiser les machines à
états, les MSC…
SPIN produit une machine à états finis en C équivalente à celle
décrite en Promela.
Eléments de syntaxe de Promela



Processus
 Modélisent une machine à états finis
 Un processus (proctype) est défini par une partie entête
(nom, paramètres) et un bloc d’instructions
Canaux
 Emission/Réception des messages entre processus
 Canal = File d’attente bornée FIFO
Variables
 Globales: Communication via « Shared Memory »
 Locales: Internes à une machine à états finis.
Définition d’un canal



Messages: Ensemble de paramètres
Paramètres: int,short,byte,bit,bool,chan,mtype
Exemple de déclaration
Promela/SPIN: les expressions

Expressions = Constituées de termes et d’opérateurs
 ,,*,/,%
opérateurs arithmétiques






>,<,<,>,,!
&&,||,!
&,|,~,<<,>>
!,?
( ), [ ]
len,run
opérateurs de comparaison
opérateurs logiques
opérateurs de niveau bit
émission et réception de messages
groupe et index
opérateurs particuliers
Exécutabilité - Non déterminisme


Une opération (condition, affectation, envoi de message) est franchie sous
réserve de son exécutabilité. Les propositions peuvent être exécutables ou
bloquées.
2 opérateurs non déterministes

Sélection (cf. CSP) SPIN choisira une suite d’instructions dont la 1ère est
exécutable.
if
:: suite_d_instructions_1
:: suite_d_instructions_2
...
:: suite_d_instructions_n
fi

Répétition
do
:: suite_d_instructions_1
::….
od
Le langage

Processus:
 Déclaration des proctype
 Instantiation: « run »
 Processus initial: « init »

Variables locales
Exécutabilité
Non Déterminisme:
 « if..fi », « do..od »


a<2
chan cnl=[1] of {byte};
proctype ProcA(int a, chan k){
byte b;
if
:: (a<2) ; b=1
:: (a<3) ; b=2
:: (a<4) ; b=0
fi;
k!b}
proctype ProcB (chan g){
byte v;
g?v; printf( "Value:%d\n",v)}
a<4
a<3
b=1

b=2
b=0
init{
run (ProcA(1,cnl));
run (ProcB(cnl)) }
Spécification en Promela

Structure: un “proctype” for:







Programme de contrôle
Chacune des 4 pompes et leurs contrôleurs
Chaudière + Valve + Dispositif de mesure
“Unités Physiques” - proctype particulier qui sera une
interface avec le Programme de contrôle.
Définition des message en “#define”
Programme de contrôle: Spécification séquentiel
des modes d’opération.
Synchronisation / Contrainte temps réel:
5 sec. Cycle d’opération pour le programme de
contrôle.
“Unités physiques”
Programme de contrôle
Processus de Développement



Approche: Ecrire une
spécification dans un langage
formel la valider à l’aide d’un
outil.
Simuler/Valider jusqu’à ce que
ça fonctionne.
Ensuite, implémentation le
modèle validé dans un langage
de programmation.
Spécification
informelle
des besoins
Spécification
Formelle
?
Implémentation
Simulation
Validation
Simulation, Validation et
Implémentation



Jusqu’à présent: SPIN
pouvant simuler et valider
une spécification Promela
Nous désirons obtenir une
Implémentation valide
Utilisation de la même
abstraction (matrice de
changement d’état) pour la
validation et
l’implémentation.
Spécification
Promela
Abstraction
Simulation
New!
Validation
Implémentation
Réutilisation de la machine à états



Cette réutilisation est facilitée par le fait que SPIN produit des
fichiers C séparés.
On aura plusieurs proctype dans le même process Unix
Nécessité d’un ordonnanceur pour l ’implémentation.
Machine à états
pan.h
pan.t
Matrice de transitions
pan.b
Mouvements arr.
pan.c
pan.m
Mouvements avant
Non-Déterminisme durant l’exécution





Lorsqu’une machine à états offre
plusieurs possibilités, laquelle
choisir?
Différentes stratégies valides sont
possibles.
Choix aléatoire = Implémentation se
comporterait comme la simulation.
Quel proctype choisir ?
Lorsque tous les proctype sont
bloqués, l ’exécution s’arrête.
Proctype A
Proctype B
Implémentation obtenue


Un Process Unix gère tous
les proctype.
La communication avec
l ’utilisateur se fait
uniquement via l’écran
(printf ...)
chaudière
pompes
unités_physiques
Programme_de_contrôle
Code
Additionnel
Process
Unix
init
Implémentation Distribuée
init



Deux spécifications Promela,
l’une pour le programme de
contrôle, l’autre pour les unités
physiques.
Définition de canaux externes
(asynchrones)
Communication par Sockets
Unix
Process 1
control
program
Canaux
Externes
boiler
pumps
physical_units
init
Unix
Process 2
Conclusions et prospectives







Promela convient tout à fait à la description d’un problème
technique tel que celui de la chaudière à vapeur
Possibilités de bien structurer le problème
Nous n’avons pas couvert tout le problème mais on arrive déjà à un
modèle trop compliqué pour la validation exhaustive.
Le compilateur et les transmissions de messages ne sont pas
validées
L’implémentation se comporte plus ou moins comme la simulation
Champ d’application principale: prototypage rapide
Etude d’une autre démarche: SDL comme langage source et C++
ou Java comme langage cible
Descargar

GL97 Presentation