Compilation et vérification de programmes LOTOS
Hubert Garavel · HAL (Le Centre pour la Communication Scientifique Directe) · 1989
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