Compilation et Vérification de Programmes LOTOS

Hubert Garavel

Thèse de Doctorat, Université Joseph Fourier (Grenoble), November 1989

Résumé

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 detats finis (permettant la verification formelle de programmes LOTOS soit par reduction ou comparaison modulo des relations dequivalence, 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 detats correspondant a un programme LOTOS. Ici au contraire la traduction est effectuee en trois etapes successives (expansion, generation et simulation) sappuyant 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 linteret de la methode.

Abstract:

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.

265 pages, in French

PDF

PostScript

Excerpts:

• Appendixes A and B
  
• Appendixes C and D.

Slides of H. Garavel's thesis defense

PDF