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


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


Cumulated slides (in English) about CAESAR_SOLVE by R. Mateescu
Cumulated slides (in French) about CAESAR_SOLVE by R. Mateescu