Compilation et vérification de programmes LOTOS
Résumé
LOTOS (Language Of Temporal Ordering Specification) is a language for
the description of concurrent and communicating systems, standardized by ISO
and CCITT to allow formal definition of telecommunication protocols and
services. LOTOS is based on algebraic abstract types to specify data structures
and on a process calculus, close to CSP and CCS, to express control structures.
This thesis proposes a compiling technique which allows to translate
a significant subset of LOTOS into both interpreted Petri nets (which may
serve as a basis for executable code generation) and finite state automata
(which allow formal validation of LOTOS programs, either by reduction and
comparison according to equivalence relations, or by evaluation of temporal
logics formulas).
The method is different from existing approaches, based on term
rewriting, that directly build the state graph corresponding to a given LOTOS
program. Conversely, translation is achieved by three successive steps
(expansion, generation and simulation) dealing with intermediate semantic
models (namely SUBLOTOS language and networks).
It involves a static and global analysis of program behaviours. It can handle
data structures, that have to be compiled by already known algorithms.
These compiling principles are fully implemented in the software tool
CAESAR. Its demonstrated performances confirm the interest of the approach
the description of concurrent and communicating systems, standardized by ISO
and CCITT to allow formal definition of telecommunication protocols and
services. LOTOS is based on algebraic abstract types to specify data structures
and on a process calculus, close to CSP and CCS, to express control structures.
This thesis proposes a compiling technique which allows to translate
a significant subset of LOTOS into both interpreted Petri nets (which may
serve as a basis for executable code generation) and finite state automata
(which allow formal validation of LOTOS programs, either by reduction and
comparison according to equivalence relations, or by evaluation of temporal
logics formulas).
The method is different from existing approaches, based on term
rewriting, that directly build the state graph corresponding to a given LOTOS
program. Conversely, translation is achieved by three successive steps
(expansion, generation and simulation) dealing with intermediate semantic
models (namely SUBLOTOS language and networks).
It involves a static and global analysis of program behaviours. It can handle
data structures, that have to be compiled by already known algorithms.
These compiling principles are fully implemented in the software tool
CAESAR. Its demonstrated performances confirm the interest of the approach
LOTOS (Language Of Temporal Ordering Specification) est un langage
de description de systemes paralleles communicants, normalise par l'ISO et le
CCITT afin de permettre la definition formelle des protocoles et des services
de telecommunications. Le langage utilise des types abstraits algebriques pour
specifier les donnees et un calcul de processus proche de CSP et CCS pour
exprimer le controle.
Cette these propose une technique de compilation permettant de traduire
un sous-ensemble significatif de LOTOS vers un modele reseau de Petri
interprete (pouvant servir a produire du code executable) puis vers un
modele automate d'etats finis (permettant la verification formelle de programmes
LOTOS soit par reduction ou comparaison modulo des relations d'equivalence, soit
par evaluation de formules de logiques temporelles).
La methode employee differe des approches usuelles basees sur la
reecriture de termes, qui construisent directement le graphe d'etats
correspondant a un programme LOTOS.
Ici au contraire la traduction est effectuee en trois etapes successives
(expansion, generation et simulation) s'appuyant sur des modeles semantiques
intermediaires (le langage SUBLOTOS et le modele reseau). Elle met en oeuvre
une analyse statique globale du comportement des programmes.
Elle prend en compte les donnees, celles-ci devant etre compilees
au moyen dalgorithmes deja existants.
Ces principes de compilation ont ete entierement implementes dans
le logiciel CAESAR. Les performances obtenues confirment l'interet de la methode.
de description de systemes paralleles communicants, normalise par l'ISO et le
CCITT afin de permettre la definition formelle des protocoles et des services
de telecommunications. Le langage utilise des types abstraits algebriques pour
specifier les donnees et un calcul de processus proche de CSP et CCS pour
exprimer le controle.
Cette these propose une technique de compilation permettant de traduire
un sous-ensemble significatif de LOTOS vers un modele reseau de Petri
interprete (pouvant servir a produire du code executable) puis vers un
modele automate d'etats finis (permettant la verification formelle de programmes
LOTOS soit par reduction ou comparaison modulo des relations d'equivalence, soit
par evaluation de formules de logiques temporelles).
La methode employee differe des approches usuelles basees sur la
reecriture de termes, qui construisent directement le graphe d'etats
correspondant a un programme LOTOS.
Ici au contraire la traduction est effectuee en trois etapes successives
(expansion, generation et simulation) s'appuyant sur des modeles semantiques
intermediaires (le langage SUBLOTOS et le modele reseau). Elle met en oeuvre
une analyse statique globale du comportement des programmes.
Elle prend en compte les donnees, celles-ci devant etre compilees
au moyen dalgorithmes deja existants.
Ces principes de compilation ont ete entierement implementes dans
le logiciel CAESAR. Les performances obtenues confirment l'interet de la methode.
Fichier principal
tel-000043391.pdf (1.31 Mo)
Télécharger le fichier
tel-00004339.pdf (229.31 Ko)
Télécharger le fichier
Format : Autre