PostScript
On-the-Fly Verification using CADP
Radu Mateescu
Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems, FMICS2003 (Trondheim, Norway), June 2003
Abstract:
On-the-fly verification consists in analysing the correctness of a finite-state concurrent system by constructing and exploring its state space incrementally. This provides a way to fight against state explosion, by enabling the detection of errors in systems with large state spaces. We give an overview of the latest on-the-fly verification techniques developed within the CADP protocol engineering toolbox. These techniques are based upon on-the-fly resolution of (alternation-free) boolean equation systems, implemented in a generic software library named CAESAR_SOLVE, which is currently used for equivalence checking and model checking.
| 5 pages | |
PostScript |
| Cumulated slides (in English) about CAESAR_SOLVE by R. Mateescu | |
| Cumulated slides (in French) about CAESAR_SOLVE by R. Mateescu | |