PostScript
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
Abstract:
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 | |
PostScript |
| Slides of H. Garavel's lecture at PSTV'90 | |