For the most recent entries see the Petri Nets Newsletter.

Compilation and Verification of LOTOS Specifications.

Garavel, H.; Sifakis, J.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography