Compilation and Verification of LOTOS Specifications

Hubert Garavel and Joseph Sifakis

Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), pages 379-394, June 1990


The ISO specification language LOTOS is a Formal Description Technique for concurrent systems. This paper presents the main features of the CAESAR system, intended for formal verification of LOTOS specifications by model-checking. This tool compiles a subset of LOTOS into extended Petri Nets, then into state graphs, which can be verified by using either temporal logics or automata equivalences. The design choices and the principles of functioning of CAESAR are described and compared to those of other LOTOS tools. The paper also proposes ideas to deal with the state explosion problem arising in verification by model-checking.

18 pages, full revised version


Slides of H. Garavel's lecture at PSTV'90