CAESAR Reference Manual

Hubert Garavel

Rapport SPECTRE, C18, Laboratoire de Génie Informatique - Institut IMAG, Grenoble, November 1990

Abstract:

This report describes a translator from LOTOS to both interpreted Petri nets and finite state automata. This tool provides a way to verify LOTOS programs by model-checking. It applies to a large subset of LOTOS (including value expressions) and can be used in conjunction with other existing tools based on graph equivalences and/or temporal logics.

32 pages, draft, obsolete in many places

PDF

PostScript

Back to the VASY Home Page