Construction and Analysis of Distributed Processes

Construction and Analysis of Distributed Processes
Developer(s) the INRIA CONVECS team (formerly VASY team)
Initial release 1986, 2930 years ago
Stable release
"Stony Brook", December 2015
Operating system Solaris on x86/x64 processors, Linux on x86/x64 processors, Windows (XP, Vista, 7 or 8), Mac OS X 10.6 or higher
Type Toolbox for designing communication protocols and distributed systems
Website cadp.inria.fr

CADP [1] (Construction and Analysis of Distributed Processes) is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team (formerly by the VASY team) at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.

The purpose of the CADP toolkit is to facilitate the design of reliable systems by use of formal description techniques together with software tools for simulation, rapid application development, verification, and test generation.

CADP can be applied to any system that comprises asynchronous concurrency, i.e., any system whose behavior can be modeled as a set of parallel processes governed by interleaving semantics. Therefore, CADP can be used to design hardware architecture, distributed algorithms, telecommunications protocols, etc. The enumerative verification (also known as explicit state verification) techniques implemented in CADP, though less general that theorem proving, enable an automatic, cost-efficient detection of design errors in complex systems.

CADP includes tools to support use of two approaches in formal methods, both of which are needed for reliable systems design:

History

Work began on CADP in 1986, when the development of the first two tools, CAESAR and ALDEBARAN, was undertaken. In 1989, the CADP acronym was coined, which stood for CAESAR/ALDEBARAN Distribution Package. Over time, several tools were added, including programming interfaces that enabled tools to be contributed: the CADP acronym then became the CAESAR/ALDEBARAN Development Package. Currently CADP contains over 50 tools. While keeping the same acronym, the name of the toolbox has been changed to better indicate its purpose: Construction and Analysis of Distributed Processes.

Major releases

Code name Date
Twente June 1997
Liege January 1999
Ottawa July 2001
Edinburgh December 2006
Zurich December 2013
Amsterdam December 2014
Stony Brook December 2015

Prior to release "Twente", there were several releases named from "A" to "Z".

Between major releases, beta releases are often available, providing early access to new features and improvements. For more information on beta releases, see the CADP website.

CADP features

CADP offers a wide set of functionalities, ranging from step-by-step simulation to massively parallel model checking. It includes:

CADP is designed in a modular way and puts the emphasis on intermediate formats and programming interfaces (such as the BCG and OPEN/CAESAR software environments), which allow the CADP tools to be combined with other tools and adapted to various specification languages.

Models and verification techniques

Verification means comparison of a complex system against a set of properties characterizing the intended functioning of the system (for instance, deadlock freedom, mutual exclusion, fairness, etc.).

Most of the verification algorithms in CADP are based on the labeled transition systems (or, simply, automata or graphs) model, which consists of a set of states, an initial state, and a transition relation between states. This model is often generated automatically from high level descriptions of the system under study, then compared against the system properties using various decision procedures. Depending on the formalism used to express the properties, two approaches are possible:

Although these techniques are efficient and automated, their main limitation is the state explosion problem, which occurs when models are too large to fit in computer memory. CADP provides software technologies for handling models in two complementary ways:

Languages and compilation techniques

Accurate specification of reliable, complex systems requires a language that is executable (for enumerative verification) and has formal semantics (to avoid any as language ambiguities that could lead to interpretation divergences between designers and implementors). Formal semantics are also required when it is necessary to establish the correctness of an infinite system; this cannot be done using enumerative techniques because they deal only with finite abstractions, so must be done using theorem proving techniques, which only apply to languages with a formal semantics.

CADP acts on a LOTOS description of the system. LOTOS is an international standard for protocol description (ISO/IEC standard 8807:1989), which combines the concepts of process algebras (in particular CCS and CSP and algebraic abstract data types. Thus, LOTOS can describe both asynchronous concurrent processes and complex data structures.

LOTOS was heavily revised in 2001, leading to the publication of E-LOTOS (Enhanced-Lotos, ISO/IEC standard 15437:2001), which tries to provide a greater expressiveness (for instance, by introducing quantitative time to describe systems with real-time constraints) together with a better user friendliness.

Several tools exist to convert descriptions in other process calculi or intermediate format into LOTOS, so that the CADP tools can then be used for verification.

Licensing and installation

CADP is distributed free of charge to universities and public research centers. Users in industry can obtain an evaluation license for non-commercial use during a limited period of time, after which a full license is required. To request a copy of CADP, complete the registration form at.[3] After the license agreement has been signed, you will receive details of how to download and install CADP.

Tools summary

The toolbox contains several tools:

A number of tools have been developed within the OPEN/CAESAR environment:

The connection between explicit models (such as BCG graphs) and implicit models (explored on the fly) is ensured by OPEN/CAESAR-compliant compilers including:

The CADP toolbox also includes additional tools, such as ALDEBARAN and TGV (Test Generation based on Verification) developed by the Verimag laboratory (Grenoble) and the Vertecs project-team of INRIA Rennes.

The CADP tools are well-integrated and can be accessed easily using either the EUCALYPTUS graphical interface or the SVL[10] scripting language. Both EUCALYPTUS and SVL provide users with an easy, uniform access to the CADP tools by performing file format conversions automatically whenever needed and by supplying appropriate command-line options as the tools are invoked.

See also

References

  1. Garavel H, Lang F, Mateescu R, Serwe W: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes International Journal on Software Tools for Technology Transfer (STTT), 15(2):89-107, April 2013
  2. ISO 8807, Language of Temporal Ordering Specification
  3. CADP Online Request Form. Cadp.inria.fr (2011-08-30). Retrieved on 2014-06-16.
  4. H. Garavel. Compilation of LOTOS Abstract Data Types, in Proceedings of the 2nd International Conference on Formal Description Techniques FORTE'89 (Vancouver B.C., Canada), S. T. Vuong (editor), North-Holland, December 1989, p. 147–162.
  5. H. Garavel, J. Sifakis. Compilation and Verification of LOTOS Specifications, in Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), L. Logrippo, R. L. Probert, H. Ural (editors), North-Holland, IFIP, June 1990, p. 379–394.
  6. H. Garavel. OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing, in Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98 (Lisbon, Portugal), Berlin, B. Steffen (editor), Lecture Notes in Computer Science, Full version available as Inria Research Report RR-3352, Springer Verlag, March 1998, vol. 1384, p. 68–84.
  7. M. Hennessy, R. Milner. Algebraic Laws for Nondeterminism and Concurrency, in: Journal of the ACM, 1985, vol. 32, p. 137–161.
  8. E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications, in: ACM Transactions on Programming Languages and Systems, April 1986, vol. 8, no 2, p. 244–263.
  9. R. De Nicola, F. W. Vaandrager. Action versus State Based Logics for Transition Systems, Lecture Notes in Computer Science, Springer Verlag, 1990, vol. 469, p. 407–419.
  10. H. Garavel, F. Lang. SVL: a Scripting Language for Compositional Verification, in: Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001 (Cheju Island, Korea), M. Kim, B. Chin, S. Kang, D. Lee (editors), Full version available as Inria Research Report RR-4223, Kluwer Academic Publishers, IFIP, August 2001, p. 377–392.

External links

This article is issued from Wikipedia - version of the 1/13/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.