An overview of CADP 2001

Published 1 January 2001Open access

Hubert Garavel, Frédéric Lang, Radu Mateescu

Citations151

TL;DR

CADP is a toolbox for specifying and verifying asynchronous finite-state systems described using process algebraic languages, allowing to deal with communication protocols, distributed systems, embedded software, mobile telephony, asynchronous hardware, cryptography, security, human-computer interaction, etc.

Abstract

CADP is a toolbox for specifying and verifying asynchronous finite-state systems described using process algebraic languages. It offers a wide range of state-of-the-art functionalities assisting the user throughout the design process: compilation, rapid prototyping, interactive and guided simulation, verification by equivalence/preorder checking and temporal logic model-checking, and test generation. The languages, models, and verification techniques used in CADP have a broad application domain, allowing to deal with communication protocols, distributed systems, embedded software, mobile telephony, asynchronous hardware, cryptography, security, human-computer interaction, etc. CADP is currently used both in industrial companies and academic institutions for research and teaching purposes. During the last years, over 50 applications and case-studies performed using CADP have been reported.

Keywords

Computer Science

IEEE Transactions on ComputersGraph-Based Algorithms for Boolean Function Manipulation

8,829 Citations1986Bryant

Experimental results from applying a new data structure for representing Boolean functions and an associated set of manipulation algorithms to problems in logic design verification demonstrate the practicality of this approach.

View PDF

ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications

3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more

It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.

View PDF

Journal of the ACMAlgebraic laws for nondeterminism and concurrency

1,361 Citations1985Matthew Hennessy, Robin Milner

The paper demonstrates, for a sequence of simple languages expressing finite behaviors, that in each case observation congruence can be axiomatized algebraically and the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.

Lecture notes in computer scienceAction versus state based logics for transition systems

288 Citations1990Rocco De Nicola, Frits Vaandrager

A temporal logic based on actions rather than on states is presented and interpreted over labelled transition systems and it is proved that it has essentially the same power as CTL*, a temporal logic interpreted over Kripke structures.

Lecture notes in computer scienceOPEN/CÆSAR: An open software architecture for verification, simulation, and testing

158 Citations1998Hubert Garavel

The Open/CAEsar software architecture is presented, which allows to integrate in a common framework different languages/formalisms for the description of concurrent systems, as well as tools with various functionalities, such as random execution, interactive simulation, on-the-fly and exhaustive verification, test generation, etc.

View PDF

Acta InformaticaFairness and related properties in transition systems ? a temporal logic to deal with fairness

141 Citations1983J. P. Queille, Joseph Sifakis

It is shown that proving a property under the assumption of fairness is equivalent to proving some other property without this assumption and that the study of FCL can be made via the “unfair” logic CL, easier to study and for which several results already exist.

Lecture notes in computer scienceTest Generation Derived from Model-Checking

102 Citations1999Thierry Jéron, P. Morel

A new on-the-fly test generation algorithm is given which is an adaptation of a classical graph algorithm which also serves as a basis of some model-checking algorithms.

View PDF

Kluwer Academic Publishers eBooksSVL: A Scripting Language for Compositional Verification

91 Citations2006Hubert Garavel, Frédéric Lang

The SVL language is presented, which allows compositional verification of Lotos descriptions to be performed simply and efficiently, and a compiler for SVL has been implemented using an original compiler-generation technique based on the Enhanced Lotos language.

View PDF

Lecture notes in computer scienceCompositional state space generation from Lotos programs

89 Citations1997Jean-Pierre Krimm, Laurent Mounier

A compositional approach to generate the labeled transition system representing the behavior of a Lotos program by repeatedly alternating composition and reduction operations on subsets of its processes by generalizing to the Lotos parallel composition operator.

International Journal on Software Tools for Technology TransferSystem design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation

29 Citations2001Hubert Garavel, César Viho +1 more

An industrial experiment is presented concerning the application of the process algebraic language lotos (iso standard 8807) to the design of polykid, a cc-numa multiprocessor architecture developed by bull.

View PDF