In: Logrippo, L.; et al.: Protocol Specification, Testing and Verification, X. Proceedings of the IFIP WG 6.1 Tenth International Symposium, 1990, Ottawa, Ont., Canada, pages 379-394. Amsterdam, Netherlands: North-Holland, 1990.
Abstract: 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, and 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 with those of other LOTOS tools. The paper also proposes ideas to deal with the state explosion problem arising in verification by model-checking.
Keywords: compilation (and) verification (of) LOTOS specifications; CAESAR system, verification (of) LOTOS specifications (by) model-checking; state explosion problem; temporal logics; automata equivalences.