Abstract: 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.