|
| 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 |
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 | |