|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
CAESAR Reference Manual
Hubert Garavel
Rapport SPECTRE, C18, Laboratoire de Génie Informatique - Institut IMAG, Grenoble, November 1990
April 2016: This document is now obsolete. Its contents have been moved (and updated) to three manual pages of CADP, the CAESAR, CAESAR.ADT, and LOTOS manual pages.
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 (obsolete document) |  |
 PostScript |