Abstract
Cadp (Construction and Analysis of Distributed Processes) is a comprehensive software toolbox that implements the results of concurrency theory. Started in the mid 80s, Cadp has been continuously developed by adding new tools and enhancing existing ones. Today, Cadp benefits from a worldwide user community, both in academia and industry. This paper presents the latest release Cadp 2010, which is the result of a considerable development effort spanning the last four years. The paper first describes the theoretical principles and the modular architecture of Cadp, which has inspired several other recent model checkers. The paper then reviews the main features of Cadp 2010, including compilers for various formal specification languages, equivalence checkers, model checkers, performance evaluation tools, and parallel verification tools running on clusters and grids.
This work has been partly funded by Bull, by the French National Agency for Research (project OpenEmbedd), by the French Ministry of Economics and Industry (Aerospace Valley project Topcased), and by the Conseil Général de l’Isère (Minalogic project Multival).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andersen, H.R.: Model Checking and Boolean Graphs. TCS 126(1), 3–30 (1994)
Bergamini, D., Descoubes, N., Joubert, C., Mateescu, R.: BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 581–585. Springer, Heidelberg (2005)
Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: FIACRE: An Intermediate Language for Model Verification in the Topcased Environment. In: ERTS (2008)
Blom, S., Orzan, S.: Distributed state space minimization. STTT 7, 280–291 (2005)
Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the Lotos NT to Lotos Translator (Version 5.1). Tech. Report INRIA/VASY, 117 pages (2010)
Chossart, R.: Évaluation d’outils de vérification pour les spécifications de systèmes d’information. Mémoire maître ès sciences, Univ. de Sherbrooke, Canada (2010)
Cleaveland, R., Li, T., Sims, S.: The Concurrency Workbench of the New Century (Version 1.2). User’s Manual (2000)
Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)
Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten Years of Performance Evaluation for Concurrent Systems Using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 128–142. Springer, Heidelberg (2010)
Deavours, D.D., Sanders, W.H.: An Efficient Well-Specified Check. In: 8th International Workshop on Petri Nets and Performance Models, PNPM 1999 (1999)
Fernandez, J.-C.: ALDEBARAN : un système de vérification par réduction de processus communicants. Thèse de Doctorat, Univ. J. Fourier, Grenoble (1988)
Fernandez, J.-C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: Cadp (Caesar/Aldebarab Development Package): A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Fernandez, J.-C., Mounier, L.: “On the Fly” Verification of Behavioural Equivalences and Preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)
Garavel, H.: Compilation et vérification de programmes Lotos. Thèse de Doctorat, Univ. J. Fourier, Grenoble (1989)
Garavel, H.: Compilation of Lotos Abstract Data Types. In: FORTE (1989)
Garavel, H.: OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 68. Springer, Heidelberg (1998)
Garavel, H.: Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular. In: LIX Colloquium on Emerging Trends in Concurrency Theory. ENTCS, vol. 209 (2008)
Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Verification. In: FORTE. IFIP (2001)
Garavel, H., Lang, F., Mateescu, R.: An Overview of Cadp 2001. EASST Newsletter 4, 13–24 (2002)
Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
Garavel, H., Mateescu, R., Bergamini, D., Curic, A., Descoubes, N., Joubert, C., Smarandache, I., Stragier, G.: DISTRIBUTOR and BCGMERGE: Tools for Distributed Explicit State Space Generation. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 445–449. Springer, Heidelberg (2006)
Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, p. 217. Springer, Heidelberg (2001)
Garavel, H., Salaün, G., Serwe, W.: On the Semantics of Communicating Hardware Processes and their Translation into Lotos for the Verification of Asynchronous Circuits with Cadp. SCP 74(3), 100–127 (2009)
Garavel, H., Serwe, W.: State Space Reduction for Process Algebra Specifications. TCS 351(2), 131–145 (2006)
Garavel, H., Sifakis, J.: Compilation and Verification of Lotos Specifications. In: PSTV. IFIP (1990)
Garavel, H., Sighireanu, M.: A Graphical Parallel Composition Operator for Process Algebras. In: FORTE/PSTV (1999)
Garavel, H., Thivolle, D.: Verification of GALS systems by combining synchronous languages and process calculi. In: Păsăreanu, C.S. (ed.) Model Checking Software. LNCS, vol. 5578, pp. 241–260. Springer, Heidelberg (2009)
Garavel, H., Turlier, P.: Caesaradt: un compilateur pour les types abstraits algébriques du langage Lotos. In: Actes du CFIP (1993)
Helmstetter, C.: TLM.Open: a SYSTEMC /TLM Front-End for the CADP Verification Toolbox, http://hal.archives-ouvertes.fr/hal-00429070/
Helmstetter, C., Ponsini, O.: A Comparison of Two SystemC/TLM Semantics for Formal Verification. In: MEMOCODE (2008)
Hermanns, H.: Interactive Markov Chains and the Quest for Quantified Quality. In: Hermanns, H. (ed.) Interactive Markov Chains. LNCS, vol. 2428, p. 57. Springer, Heidelberg (2002)
Hermanns, H., Joubert, C.: A Set of Performance and Dependability Analysis Components for CADP. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 425–430. Springer, Heidelberg (2003)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
ISO/IEC. Lotos — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization, Geneva (1989)
ISO/IEC. Enhancements to Lotos (Elotos). International Standard 15437:2001, International Organization for Standardization, Geneva (2001)
Khan, A.M.: Connection of Compositional Verification Tools for Embedded Systems. Mémoire master 2 recherche, Univ. J. Fourier, Grenoble (2006)
Lang, F.: Exp.Open 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70–88. Springer, Heidelberg (2005)
Lang, F., Salaün, G., Hérilier, R., Kramer, J., Magee, J.: Translating FSP into LOTOS and Networks of Automata. FACJ 22(6), 681–711 (2010)
Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. Bertz, Berlin (1997)
Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, Chichester (2006)
Mateescu, R.: Vérification des propriétés temporelles des programmes parallèles. Thèse de Doctorat, Institut National Polytechnique de Grenoble (April 1998)
Mateescu, R.: Efficient Diagnostic Generation for Boolean Equation Systems. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, p. 251. Springer, Heidelberg (2000)
Mateescu, R.: Caesarsolve: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems. STTT 8(1), 37–56 (2006)
Mateescu, R., Garavel, H.: Xtl: A Meta-Language and Tool for Temporal Logic Model-Checking. In: STTT. BRICS (1998)
Mateescu, R., Salaün, G.: Translating Pi-Calculus into LOTOS NT. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 229–244. Springer, Heidelberg (2010)
Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. SCP 46(3), 255–281 (2003)
Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)
Ponsini, O., Fédèle, C., Kounalis, E.: Rewriting of imperative programs into logical equations. SCP 56(3), 363–401 (2005)
Ponsini, O., Serwe, W.: A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOS. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 278–293. Springer, Heidelberg (2008)
Schewe, S.: Solving Parity Games in Big Steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 449–460. Springer, Heidelberg (2007)
Stevens, P., Stirling, C.: Practical Model-Checking Using Games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 85. Springer, Heidelberg (1998)
Thivolle, D.: Langages modernes pour la vérification des systèmes asynchrones. PhD thesis, Univ. J. Fourier Grenoble and Polytechnic. Univ. of Bucharest (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garavel, H., Lang, F., Mateescu, R., Serwe, W. (2011). CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19835-9_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-19835-9_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19834-2
Online ISBN: 978-3-642-19835-9
eBook Packages: Computer ScienceComputer Science (R0)