Hubert Garavel

Frédéric Lang

Radu Mateescu

Wendelin Serwe
email: wendelin.serwe@inria.fr

{hubert Garavel

Frederic Lang

CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes ⋆

Keywords: asynchronous concurrency, equivalence checking, formal methods, model checking, performance evaluation, process calculus, verification

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 2011, which is the result of a considerable development effort spanning the last five 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 2011, including compilers for various formal specification languages, equivalence checkers, model checkers, compositional verification tools, performance evaluation tools, and parallel verification tools running on clusters and grids. Finally, the paper surveys some significant case studies.

1 Introduction Among all the scientific issues related to the reliability of computer systems, concurrency has a major place, because the design of parallel systems is a complex, errorprone, and largely unmastered activity. Thirty years after the first attempts at building automated verification ⋆ 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). tools for concurrent systems, the problem is still there; it has even gained in relevance because system complexity has increased, and because concurrency is now ubiquitous, from multicore microprocessors to massively parallel supercomputers.

To ensure the reliability of a concurrent system under design, it is understood that the first step consists in establishing a precise model of the system behavior, this model usually consisting of several concurrent processes, together with a description of the data types, constants, variables, and functions manipulated by these processes. This opens the debate on the most appropriate languages to express system models, with a large choice of candidates ranging from semi-formal to formal languages.

Once a precise, if not formal, model is available, one needs automated methods to prove the correctness of the system with respect to its specification or, at least, to search for the presence of certain mistakes. Without neglecting recent progresses in theorem proving and static analysis, state space exploration techniques (among which reachability analysis and model checking) remain the most successful approaches for dealing with complex concurrent systems, especially during the design phase, when system specifications are evolving frequently.

State space exploration techniques are usually grouped in two classes: enumerative (or explicit state) techniques consider each state of the system separately, whereas symbolic (or implicit state) techniques manipulate sets of states represented using either decision diagrams (Bdds and their variants) or logical formulas whose satisfiability is determined using Sat and Smt solvers. In this paper, we will use the term enumerative instead of explicit-state in order to avoid possible confusions with the terminology about explicit and implicit models (see Section 2). Enumerative techniques, which historically were introduced first [124], are based on a forward exploration of the transition relation be-tween states (post function), making them suitable for the on-the-fly verification of specifications written in languages with arbitrary data types. Although they enable exploration of a priori fewer states than their symbolic counterparts, enumerative techniques prove to be adequate for the analysis of asynchronous parallel systems containing complex data structures.

Cadp (Construction and Analysis of Distributed Processes) 1 is a toolbox for verifying asynchronous concurrent systems. The toolbox, whose development started in 1986, is at the crossroads between several branches of computer science: concurrency theory, formal methods, and computer-aided verification. Initially, Cadp consisted of only two tools: Caesar [START_REF] Garavel | Compilation et vérification de programmes LOTOS[END_REF], a compiler and explicit state space generator for the Lotos language, and Aldébaran [START_REF] Fernandez | ALDEBARAN : un système de vérification par réduction de processus communicants[END_REF][START_REF] Fernandez | On the Fly" Verification of Behavioural Equivalences and Preorders[END_REF], an equivalence checker based on bisimulation minimization. Over the past 25 years, Cadp has been continuously improved and extended [START_REF] Fernandez | CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox[END_REF][START_REF] Garavel | An Overview of CADP[END_REF][START_REF] Garavel | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. This paper is an extended version of [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] and presents the latest release, Cadp 2011 "Zurich", which currently contains 45 tools.

Cadp now offers a comprehensive set of functionalities covering the entire design cycle of asynchronous systems: specification, interactive simulation, rapid prototyping, verification, testing, and performance evaluation. For verification, it supports the three essential approaches existing in the field: model checking, equivalence checking, and visual checking. To deal with complex systems, Cadp implements a wide range of verification techniques (reachability analysis, on-the-fly verification, compositional verification, distributed verification, static analysis) and provides a scripting language for describing elaborate verification scenarios. In addition, Cadp 2011 brings deep changes with respect to previous releases, especially the support for many different specification languages.

Related Work. There are many model checkers developed in the world. By taking the Wikipedia list of model checking tools 2 and complementing it with the list of verification tools established at the University of Brno3 , one obtains a cumulated list of 64 tools (as of January 2012). By considering only those tools that are still actively maintained (i.e., those for which at least one new version was released in 2010, 2011, or early 2012), one can restrict this list to 32 tools only, but this is still quite a number of tools that should be compared with Cadp. Moreover, there are plenty of possible criteria for such comparison. We can mention the following ones.

From an historical perspective, Cadp and Spin [START_REF] Holzmann | Design and Validation of Computer Protocols[END_REF] seem to be the two oldest model checkers still available. The development of both tools was undertaken in the 80s and is still going on with, e.g., support for 64-bit computing platforms, as well as application in recent industrial case-studies.

From a functionality perspective, Cadp provides a unique combination of features that no other tool presently offers. This can be seen by formulating four essential criteria: (C1) Does the tool support not only model-checking but also equivalence checking which, beyond being standard practice in hardware verification, plays a crucial role for component-based systems and compositional verification? (C2) Does the tool support distributed verification, i.e.

can it use the computing power and memories of a cluster of machines, rather than a single machine? (C3) Does the modeling language of the tool support concurrency, i.e. does it have some builtin notion of asynchronous parallel composition? (C4) Does the modeling language support user-defined (possibly unbounded) data types such as records, unions, lists, etc. (and not only boolean, integers, and enumerated types)?

To the best of our knowledge, Cadp is the only tool to satisfy criteria (C1) to (C4). It is followed by the Ltsmin [START_REF] Blom | LTSmin: Distributed and Symbolic Reachability[END_REF] that is interconnected to Cadp. Let us mention that another distinctive trait of Cadp is the inclusion of performance evaluation tools, in addition to functional verification tools.

A detailed comparison of Cadp with other explicitstate model checkers will be given in Section 2.

Outline. This paper gives an overview of Cadp 2011, highlighting new tools and recent enhancements. It is organized as follows. Section 2 presents the core semantic models of Cadp -namely (explicit and implicit) labeled transition systems (Ltss), Markov chains, and (parameterized) Boolean equation systems (Pbess). Section 3 describes the four languages now supported by Cadp -namely Lotos, Fsp, Exp, and Lotos NTand lists translations developed for other languages. Section 4 presents the visual checking features of Cadp. Section 5 presents the model checking features of Cadp, namely the Xtl language, the Evaluator 3.6 model checker for regular alternation-free µ-calculus, and the Evaluator 4.0 model checker for Mcl, an extension of modal µ-calculus with typed variables and data manipulation constructs. Section 6 is devoted to the equivalence checking features of Cadp -namely the Bcg Min tool for bisimulation minimization and the Bisimulator tool for on-the-fly comparison of Ltss. Section 7 presents the compositional verification features of Cadp. Section 8 describes the tools of Cadp for performance evaluation, in particular steady-state/transient analysis and simulation of Markov chains. Section 9 outlines the Cadp tools for parallel and distributed verification. Section 10 surveys some significant case studies. Finally, Section 11 summarizes the achievements and indicates directions for future work.

Architecture and Verification Technology

Compared to other explicit-state model checkers (especially Spin [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF]), Cadp has the following principles and distinctive features (some of which were already present in precursory tools rooted in concurrency theory, such as Cwb [START_REF] Cleaveland | The Concurrency Workbench[END_REF] and Cwb-Nc [START_REF] Cleaveland | The Concurrency Workbench of the New Century (Version 1.2). User's manual[END_REF]):

-Cadp supports both high-level languages with a formal semantics (process calculi) and lower level formalisms (networks of communicating automata); it also accepts connections from informal or semiformal languages that have a means to compute the post transition function.

-Contrary to most model checkers supporting only scalar types, Cadp has from the outset supported concurrent programs with complex and/or dynamic data structures (records, unions, lists, trees, etc.) provided that these data structures are not shared between concurrent processes.

-Cadp relies on action-based (rather than state-based ) semantic models inherited from concurrency theory, in which one can only refer to the observable communication actions performed by a system instead of the internal contents of states, which are supposed to be hidden and implementation dependent, and thus are not abstract enough. This encompasses the classical concepts of Ltss (for verification), discreteand continuous-time Markov chains (for performance evaluation), and extended Markovian models, such as Interactive Markov Chains (Imcs) [START_REF] Hermanns | Interactive Markov Chains and the Quest for Quantified Quality[END_REF], which combine Ltss and Markov chains. [START_REF] Fernandez | Verification of Protocol Specifications using the CESAR System[END_REF], Emc [START_REF] Clarke | Automatic Verification of Finite-State Concurrent Systems using Temporal Logic[END_REF][START_REF] Clarke | Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications[END_REF], Xesar [START_REF] Graf | What are the Limits of Model Checking Methods for the Verification of Real Life Protocols[END_REF], and Spin [START_REF] Holzmann | Design and Validation of Computer Protocols[END_REF]) were "monolithic" in the sense that they tightly combined (1) the source language used to specify the concurrent system under verification and the compiling algorithms used to generate/explore the state space of the concurrent system, and (2) the temporal logic language used to specify correctness formulas and the verification algorithms that evaluate these formulas over the state space. Cadp took a different approach and adopted a modular architecture with a clear separation between language-dependent and languageindependent aspects. Different verification functionalities are implemented in different tools, which can be reused for several languages and which are built upon well-specified interfaces that enable code factoring. -Cadp 2011 can manage state spaces as large as 10 10 explicit states; by employing compositional verification techniques on individual processes, much larger state spaces can be handled, up to sizes comparable to those reached using symbolic techniques, such as Bdds. Cadp can be seen as a rich set of powerful, interoperating software components for manipulating automata and Markov chains. All these tools are integrated in two ways: for interactive use, a graphical userinterface (named Eucalyptus) with contextual menus is provided; for batch use, a user-friendly scripting language, Svl, was designed, providing powerful verification strategies -to the best of our knowledge, the Svl feature of Cadp is unique and there is no equivalent in competing toolboxes.

Explicit state spaces. In the terminology of Cadp, an explicit state space is a state-transition graph defined extensively, meaning that the sets of states and transitions are entirely known, because they have been already computed.

In the early 90s, most verification tools represented explicit state spaces using textual file formats, which were only adequate for small graphs but would not scale satisfactorily, e.g., to millions of states. To solve this issue, Cadp was equipped in 1994 with Bcg (Binary-Coded Graphs), a portable file format for storing Ltss (with provisions for storing also Kripke structures and Kripke Transition Systems although these two models are not used in the setting of Cadp). Bcg is a binary format, which was designed to handle large state spaces (up to 10 8 states and transitions initially -this limit was raised to 10 13 in Cadp 2011 to take into account 64-bit machines). Because the Bcg format is not human readable, it comes with a collection of code libraries and utility programs for handling Bcg files.

Two key design goals for Bcg are file compactness and the possibility to encode/decode files quickly and dynamically (i.e., without requiring knowledge of the entire state space in advance); these goals are achieved using dedicated compression techniques that give significant results: usually, two bytes per transition on average, as observed on Vlts (Very Large Transition Systems) 4 , a benchmark suite used in many scientific publications. A third design goal is the need to preserve in Bcg files the source-level information (identifiers, line numbers, types, etc.) present in the source programs from which Bcg files are generated, keeping in mind that these programs could be written in a variety of languages.

Implicit state spaces. In the terminology of Cadp, an implicit state space is a state-transition graph defined comprehensively, meaning that only the initial state and the post transition function are given, such that (a fragment of) the graph is progressively explored and discovered on demand, depending on the verification goals. Handling implicit state spaces properly is a prerequisite for on-the-fly verification.

In addition to Bcg, which only applies to explicit state spaces, Cadp provides Open/Caesar [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF], a software framework for implicit state spaces, which enforces modularity by clearly separating languagedependent aspects (i.e., compiler algorithms) from language-independent aspects (i.e., state-space exploration algorithms). Open/Caesar is organized around three components: the graph module (which encapsulates all language-dependent aspects, typically code generated from a high-level source program to compute states and transitions), the library module (which provides useful generic data structures, e.g., stacks, tables, hash functions, etc.), and the exploration module (which gathers language-independent aspects, typically simulation, testcase generation, and verification algorithms). All the internal details of the graph module are hidden behind a programming interface, which provides an abstraction for states and transition labels (making them available as opaque types) and implements the transition relation by means of a higher-order iterator.

Since the introduction of the Open/Caesar architecture in 1992, each of its three modules has been progressively extended. Regarding the graph module, only Lotos was supported at first, but support for more languages (Fsp [START_REF] Magee | Concurrency: State Models and Java Programs[END_REF], Lotos NT [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF], µCrl [START_REF] Groote | The Syntax and Semantics of µCRL[END_REF], Sdl [START_REF]ITU-T. Specification and Description Language (SDL)[END_REF], and SystemC/Tlm [112]), more automata-based formalisms (Bcg, Exp [START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF], Fc2 [START_REF] Bouali | The Fc2Tools set: a Toolset for the Verification of Concurrent Systems[END_REF], and Seq [START_REF] Garavel | OPEN: A Tool for Efficient Trace-Based Verification[END_REF]) and more external tools (If [START_REF] Bozga | IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems[END_REF], Kronos [128], Ltsmin [START_REF] Blom | LTSmin: Distributed and Symbolic Reachability[END_REF], TorX [START_REF] Belinfante | Formal Test Automation: A Simple Experiment[END_REF]) has been added, either by our or other research teams. Regarding the library module, its data structures and algorithms have been continuously optimized and enriched. Regarding the exploration module, many Open/Caesar tools have been developed for simulation, random execution, model checking, equivalence checking, and test case generation. The merits of the Open/Caesar modular architecture are recognized (e.g., in [START_REF] Blom | LTSmin: Distributed and Symbolic Reachability[END_REF]: "the Open/Caesar interface has been underlying the success of the Cadp toolkit ") and a similar architecture can be found in several recent model checkers for concurrent systems, such as DiVinE5 [2], Ltsmin6 [START_REF] Blom | LTSmin: Distributed and Symbolic Reachability[END_REF], and Pat7 [START_REF] Liu | Developing Model Checkers Using PAT[END_REF].

Boolean equation systems (Bess [START_REF] Mader | Verification of Modal Properties Using Boolean Equation Systems[END_REF]). These are a useful low-level formalism for expressing analysis problems on Ltss, i.e., model checking, equivalence checking, partial order reductions, test case generation, and behavioral adaptation. A Bes is a collection of equation blocks, each defining a set of Boolean variables (left-hand sides) by propositional formulas (right-hand sides). All equations in a block have the same fixed point sign: either minimal (µ) or maximal (ν). Bess can be represented as Boolean graphs [START_REF] Andersen | Model checking and boolean graphs[END_REF] and are closely related to game graphs [116] and parity games [115]. Below is an example of Bes in which block B 0 depends on variable Y 0 defined in block B 1 :

(B0)      X0 =ν X1 ∧ X2 X1 =ν X0 ∨ X1 ∨ X2 X2 =ν Y0 ∧ X3 X3 =ν true      (B1)      Y0 =µ Y1 ∨ Y2 Y1 =µ false Y2 =µ Y2 ∧ Y3 Y3 =µ Y0 ∨ Y1 ∨ Y3     
The Caesar Solve library [START_REF] Mateescu | A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems[END_REF][START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF] of Open/Caesar contains a collection of linear-time algorithms for solving alternation-free Bess using various exploration strategies of its underlying Boolean graph (depth-first search, breadth-first search, etc.). The resolution works on the fly, the Bes being constructed (e.g., from the evaluation of a temporal logic formula on an Lts, or from the comparison of two Ltss) at the same time it is solved, new equations being added to the Bes and solved as soon as they are discovered. All the algorithms of Caesar Solve can generate diagnostics, i.e., compute a minimal (in the sense of graph inclusion) Boolean subgraph explaining why a given Boolean variable is true or false [START_REF] Mateescu | Efficient Diagnostic Generation for Boolean Equation Systems[END_REF].

New strategies have been added to Cadp 2011 for solving conjunctive Bess (arising from equivalence checking) and disjunctive Bess (arising from model checking), keeping in memory only the vertices (and not the edges) of the Boolean graphs. Currently, Cadp 2011 offers nine resolution strategies, which can solve Bess containing 10 7 variables in ten minutes on a machine with a 2 GHz Cpu. Recently, a new linear-time algorithm generalizing the detection of accepting cycles in Büchi automata was added [101], which serves for model checking fairness properties. For testing and benchmarking purposes, Cadp 2011 provides the new Bes Solve tool, which can evaluate Bess entirely constructed and stored in (gzipped) files, or built on the fly randomly according to fourteen parameters (number of variables, equation length, percentage of disjunctive and conjunctive operators, etc.).

It is known [START_REF] Liu | Simple Linear-Time Algorithms for Minimal Fixed Points[END_REF] that Bess can encode HornSat, a particular case of the Sat problem. Thus, Caesar Solve can be used to solve large instances of HornSat (containing billions of variables) in linear-time.

Parameterized Boolean equation systems.

Cadp 2011 also uses internally the Pbes (Parameterized Bes) model [START_REF] Mateescu | Vérification des propriétés temporelles des programmes parallèles[END_REF], which extends the Bes model by adding typed data parameters and arbitrary Boolean expressions over these parameters. For instance, the following Pbes checks whether factorial (m) = n:

X(m, n) =µ   (n > 0) ∧ (m = 0) ⇒ (n = 1) ∧ (m > 0) ⇒ n%m = 0 ∧ X(n/m, m -1)

 

The Pbes model was originally invented as a means of representing the model checking of Mcl formulas (µ-calculus extended with typed data), implemented in the Evaluator 4.0 model checker now available in Cadp 2011 (see Section 5). Recently, this model received much attention from the model checking community [START_REF] Groote | Parameterised Boolean Equation Systems[END_REF], which investigates two approaches: symbolic resolution or instantiations towards Bess followed by on-the-fly resolution, the latter being somehow close to Sat-solving. Beyond verification, Pbess can express other problems such as evaluation of parameterized Horn-clauses or Datalog queries over data-bases [START_REF] Liu | Simple Linear-Time Algorithms for Minimal Fixed Points[END_REF].

Specification languages

A major addition to Cadp 2011 compared with earlier versions is the support for several specification languages, while previously only Lotos was supported.

Support for the LOTOS language

Lotos [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF] is a formal specification language standardized by Iso to describe communication protocols. It is composed of two different languages in one: a data part, based on algebraic abstract data types, and a control part, which is a process calculus combining the best features of Ccs [104], Csp [START_REF] Hoare | Communicating Sequential Processes[END_REF], and Circal [103]. For this reason, Cadp provides two Lotos compilers, both sharing a common front-end.

Compiling the data part. The Caesar.adt compiler [START_REF] Garavel | Compilation of LOTOS Abstract Data Types[END_REF][START_REF] Garavel | ADT : un compilateur pour les types abstraits algébriques du langage LOTOS[END_REF] translates the data part of a Lotos program (i.e., a collection of sorts, constructors, and functions defined by algebraic equations) into executable C code. The translation aims at verification efficiency, by first optimizing memory (which is essential for state space exploration, where every bit counts), then time. The compiler automatically recognizes certain classes of the usual types (natural numbers, enumerations, tuples, etc.), which are implemented optimally. The algebraic equations of Lotos are translated using a patternmatching compilation algorithm for rewrite systems with priority. This required deviations from standard Lotos (e.g., introducing a distinction between constructor and non-constructor operations, and turning the algebraic equations into a system of rewrite rules with priorities), which were found to be acceptable in practice. Amusingly, most of the compiler is itself written using Lotos abstract data types, so Caesar.adt is used to bootstrap itself.

The version of Caesar.adt included in Cadp 2011 enables values of complex types (such as tuples, unions, lists, trees, strings, sets, etc.) to be represented "canonically", meaning that these values are stored in tables, represented in normal form as table indexes and thus are stored only once in memory. A technical challenge was to make this feature optional: the user can selectively store certain types in tables, while other types remain implemented as before.

Compiling the control part. The Caesar compiler [START_REF] Garavel | Compilation and Verification of LOTOS Specifications[END_REF][START_REF] Garavel | State Space Reduction for Process Algebra Specifications[END_REF] translates an entire Lotos program (reusing the C code generated by Caesar.adt) into C code that can be used either for generating an explicit Lts (encoded in the Bcg format) or an implicit Lts (represented using the Open/Caesar programming interface), or for rapid prototyping (using the Exec/Caesar programming interface, which enables the connection with a real-world environment). The subset of Lotos accepted by Caesar must obey certain constraints, which forbid unbounded dynamic creation of processes and non-terminal recursion in process calls; practically, these constraints are acceptable in most cases.

The translation is done using several intermediate steps, so as to perform, for efficiency reasons, as many computations as possible at compile-time. The Lotos program is first translated into a simplified language named SubLotos, then into a (hierarchical) Petri net extended with atomic transitions, typed local/global variables, and arbitrary combinations of conditions and actions attached to Petri net transitions. This Petri net is then simplified by applying a collection of optimizations on its control and data flows, and finally transformed into C code. Caesar can generate C code for different purposes, namely an Open/Caesar graph module, an optimized stand-alone program for Lts generation, or C code for co-simulation and rapid prototyping according to the Exec/Caesar framework [START_REF] Garavel | System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation[END_REF].

In addition to various bug fixes, the version of Caesar included in Cadp 2011 delivers increased performance, particularly by introducing dynamically resizable state tables and by optimizing the generated C code for the amount of physical memory available. Also, the reduction techniques based on data flow analysis [START_REF] Garavel | State Space Reduction for Process Algebra Specifications[END_REF], which typically reduce state spaces by several orders of magnitude, have been enhanced by applying data-flow optimizations iteratively, following the hierarchical structure of the Petri net: for 22% of the benchmarks, the number of states is divided by 2.4 on average (on certain benchmarks, it is divided by 25).

Support for the FSP language

Fsp (Finite State Process) is a concise algebraic notation for concurrent processes [START_REF] Magee | Concurrency: State Models and Java Programs[END_REF], supported by the Ltsa (Labelled Transition System Analyser ) 8 verification tool designed at Imperial College (London, United Kingdom). Fsp and Ltsa are particularly suited for students to practice with academic examples.

Although Fsp and Lotos share many fundamental concepts, they differ slightly in their expressiveness. On the one hand, Fsp provides a priority operator that has no equivalent in Lotos. On the other hand, Lotos enables abstract data types to be defined by the user, while Fsp provides Booleans, integers, labels, and predefined numeric functions only. Also, Lotos enables sequential and parallel composition operators to be combined with only few restrictions, while Fsp imposes a strict separation between sequential and parallel processes, so that parallel processes cannot be composed in sequence.

Cadp 2011 supports the Fsp language, following the translation approach of [START_REF] Lang | Translating FSP into LOTOS and Networks of Automata[END_REF], implemented in two new tools. The Fsp2Lotos tool translates each sequential Fsp process into a Lotos process, and each par-8 http://www.doc.ic.ac.uk/ltsa allel Fsp process into an Exp [START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF] network of communicating processes with priorities. The Fsp.Open tool provides a transparent interface between Fsp and the Open/Caesar environment, which thus enables every Fsp specification to be explored using any tool in the Open/Caesar exploration module. These tools have been validated on more than 1000 Fsp examples, for which the Ltss generated by Cadp were found to be strongly bisimilar to those generated by Ltsa.

For the Fsp user community, Cadp 2011 brings the following advantages: it can handle Fsp programs with non-guarded process recursion; it can handle larger Fsp programs than Ltsa, due to the particular attention to performance issues in Cadp and to the support of 64-bit architectures, whereas Ltsa suffers from Java's 32-bit limitations; finally, Cadp offers many tools that complement the functionalities provided by Ltsa.

Support for the LOTOS NT language

A major new feature of Cadp 2011 is the support of Lotos NT [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF], a specification language derived from the Iso standard E-Lotos [START_REF]ISO/IEC. Enhancements to LOTOS (E-LOTOS)[END_REF]. Lotos NT is an attempt [START_REF] Garavel | Towards a Second Generation of Formal Description Techniques -Rationale for the Design of E-LOTOS[END_REF][START_REF] Garavel | Défense et illustration des algèbres de processus[END_REF][START_REF] Garavel | Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular[END_REF] at merging the most salient features of process calculi (concurrency, abstraction, congruence results) into mainstream programming languages (imperative and functional languages for sequential programming). Contrary to Lotos, which gathers two different languages into one, Lotos NT exhibits a single unified language, in which the data part can be seen as a subset of the control part (i.e., functions are a particular case of processes): absence of such a nice symmetry in Lotos is a drawback and a cause of its steep learning curve.

Lotos NT has convenient features that Lotos is lacking: it has a set of predefined data types (Booleans, natural numbers, integers, reals, characters, and strings); it provides short-hand notations for lists, sets, arrays, intervals, and predicate types; it eases the definition of inductive types by automatically generating common operations (equality and order relations, field accessors, etc.); it enables typing of communication channels [START_REF] Garavel | On the Introduction of Gate Typing in E-LOTOS[END_REF]; it introduces the notion of modules. Similar to the Lotos compilers of Cadp, Lotos NT can import hand-written, external C code that implements Lotos NT types and functions; under some conditions, it is also possible to combine Lotos and Lotos NT code into the same specification.

As an example, Figures 1 and2 give an excerpt of a Lotos NT model of the Mcs queue lock [102, Figure 5] for N processes trying to access a common resource; this model is part of a study of mutual exclusion protocols [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF]. The Mcs queue lock ensures mutual exclusion by means of a queue of waiting processes implemented in shared memory. A global variable (modeled as process "Lock") contains the index of the last element of the queue (or "nil" if the resource is free); this variable is modifiable by atomic fetch-and-store and compare-andswap operations. The elements of the queue are pairs of the index of the next element and a Boolean flag indicating whether the resource is still locked by some preceding process; all elements are modeled as a shared array "m", accesses to which are managed by process "Memory". To acquire the lock, process "P" with identifier "pid" modifies the index of the last element to point to "m[pid]", initialized to "(nil, false)", and then waits until the resource is released by the immediately preceding process (by setting the flag to true). Each access to a shared variable is modeled by a rendezvous communication on one of the gates "L" or "M", using four or five offers (i.e., data parameters): in all cases, the first offer defines the operation to be executed, and the last offer indicates the executing process.

The feedback received about Lotos NT from both academia and industry is highly positive: it is observed that people quickly start writing meaningful Lotos NT specifications without the need for a long prior training. As of January 2010, the Vasy team has switched from Lotos to Lotos NT for all its modeling activities, and Lotos NT is used internally in companies such as Bull, Cea/Leti, and STMicroelectronics.

Cadp 2011 includes a set of tools (Lpp preprocessor, Lnt2Lotos translator, and Lnt.Open connector to Open/Caesar) that implement Lotos NT by translation to Lotos, which enables one to reuse the Caesar and Caesar.adt compilers to analyze and execute Lotos NT specifications. To reduce the translation complexity, many semantic checks are deferred to the Caesar.adt and Caesar compilers that will run on the generated, possibly incorrect Lotos code.

The translation of Lotos NT data part into Lotos (which is, to some extent, the reverse of the translation performed by Caesar.adt) requires compilation of functions defined in imperative-style into rewrite systems with priorities. It reuses an existing algorithm [108] for translating a subset of the C language into Horn clauses, but largely extends this algorithm to handle reference-passing parameters, pattern matching ("case" statements), loop interruptions ("break" statements), multiple "return" statements within function bodies, uncatchable exceptions ("raise" statements), and overloading of function names.

The translation of the Lotos NT control part into Lotos process algebraic terms borrows from a prior translation of Chp into Lotos [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF], which was adapted and optimized for Lotos NT. The translation is tricky because Lotos is much less "regular" than Lotos NT for certain aspects (sequential composition, functionality typing for process termination) and because Lotos lacks certain concepts (graphical parallel composition [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF], type checking for communication channels). Surprisingly, the state spaces generated from Lotos NT programs are in general not larger than those generated from "equivalent" Lotos programs, due to the precise

Support for the EXP language

Exp is a language for describing a network of communicating Ltss, represented as a set of Bcg files. In its current version, 2.0 [START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF], Exp offers an expressive syntax for handling compositions of processes in various languages. It provides the parallel composition, hiding, renaming, and cutting operators of Ccs [104], Csp [111], Lotos [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF], E-Lotos [START_REF]ISO/IEC. Enhancements to LOTOS (E-LOTOS)[END_REF], Lotos NT, and µCrl [START_REF] Groote | The Syntax and Semantics of µCRL[END_REF], as well as synchronization vectors and priorities. Hiding, renaming, and cutting operators are generalized, so that gate and/or label sets can be represented using regular expressions.

Figure 3 illustrates an Exp network of Ltss corresponding to an instance of the Mcs queue lock for five processes, where only the gates "ENTER" and "LEAVE" are made observable. Each of "Pi.bcg" (i ∈ 1..5), "Lock.bcg", and "Memory.bcg" is a Bcg file encoding the Lts corresponding respectively to one of the five concurrent processes or to a shared variable.

Support for other languages

Numerous other languages have been connected to Cadp 2011. Figure 4 with bibliographic references; arcs without labels correspond to work in progress; dotted arcs correspond to manual translations. These translation approaches have the merit of unifying the landscape of concurrent languages, which is currently scattered among multiple, incompatible proposals. Also, they significantly help to progress the development of the Lotos and Lotos NT compilers, by providing Vasy with many programs, different from those that humans usually write; these programs reveal compiler mistakes and suggest new compiler optimizations for state space reduction and/or better performance.

Visual Checking

Cadp contains tools to visualize explicit and implicit state spaces.

For explicit state spaces, the Bcg Draw and Bcg Edit (see Figure 5) tools enable Ltss encoded in the Bcg format to be visualized and edited interactively.

For implicit state spaces, the Ocis (Open/Caesar Interactive Simulator, see Figure 6) tool enables step-bystep simulation with backtracking. Simulation scenarios, which are trees describing the execution paths fol- Xtl (eXecutable Temporal Language) [START_REF] Mateescu | XTL: A Meta-Language and Tool for Temporal Logic Model-Checking[END_REF] is a functional language dedicated to the exploration and querying of an explicit Lts encoded in the Bcg format. Xtl handles (sets of) states, labels, and transitions as basic data types, enabling temporal logic operators to be implemented using their fixed point characterizations. Temporal logic operators can be mixed with non-standard properties (e.g., counting states, transitions, etc.) and, more generally, with arbitrary computations described as recursive functions exploring the Lts. Xtl specifications can include reusable libraries of operators (15 such libraries are available in Cadp) and can also be interfaced with external C code for specific computations.

Evaluator 3.x [100] evaluates formulas of Rafmc (the regular alternation-free µ-calculus) on an implicit Lts on the fly. Rafmc incorporates the Pdl [START_REF] Fischer | Propositional Dynamic Logic of Regular Programs[END_REF] modalities containing regular formulas over transition sequences, which are much more concise and intuitive than their fixed point counterparts: for instance, safety properties are simply expressed using the modality "[R] false", which forbids the transition sequences characterized by the regular formula R. The tool works by reformulating the model checking problem as a Bes resolution, which is performed using the linear-time local algorithms of the Caesar Solve library [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF]. According to the shape of the formula, the most memory-efficient algorithm of the library is selected automatically: e.g., all formulas of Actl [105] or Pdl are evaluated using algorithms optimized to store only states, and not transitions, of the Lts. The tool produces examples and counterexamples, which are general Lts subgraphs (i.e., may contain branches and/or cycles), and also enables the definition of reusable libraries of property patterns, such as [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF] Mcl contains action predicates with value extraction, fixed point operators parameterized with data values, quantifiers over finite data domains, regular formulas extended with counters, and constructs inspired from functional programming languages ("let", "if-then-else", "case", "while", "repeat", etc.).

Second, Mcl adds fairness operators, inspired from those of Pdl-∆ [117], which characterize complex, unfair cycles consisting of infinite repetitions of regular 9 http://cadp.inria.fr/resources/evaluator/rafmc.html subsequences. These operators belong to Lµ 2 , the µcalculus fragment of alternation depth two and were shown to subsume Ctl * [125]. Although Lµ 2 has, in the worst case, a quadratic model checking complexity [START_REF] Emerson | Efficient Model Checking in Fragments of the Propositional Mu-Calculus[END_REF], the fairness operators of Mcl are evaluated in linear-time using an enhanced resolution algorithm of Caesar Solve [101].

We illustrate below the features of Mcl by means of two data-based temporal properties related to the Mcs protocol described in Figure 1. The first property expresses that processes access the shared resource in mutual exclusion, i.e., after a process i entered its critical section, it is impossible that another process j also enters its critical section as long as process i does not leave its critical section. This can be expressed in Mcl using a necessity modality that forbids the occurrence of undesirable execution sequences:

[ true* . { ENTER ?i:Nat } . ( not { LEAVE !i } )* .
{ ENTER ?j:Nat where j <> i } ] false Note how the process identifier i is captured by the first action predicate and is reused later in the formula in the "where" clause. This formula is fully parametric, in the sense that it does not depend on the number N of processes, and therefore it can be reused as it is for verifying any instantiation of the Mcs.

The second property specifies the absence of starvation for each process i, i.e., the absence of cycles on which every process executes at least one action, but process i does not enter its critical section. This can be expressed in Mcl by using the saturation operator "[R]-|", which forbids the infinite repetition of a transition sequence characterized by the regular formula R:

[ true* ] forall i:Nat among {1...N } .
[ for j:Nat from 1 to N do ( not { ENTER ... !i } )* . { ?G:String ... !j where (j = i) implies (G <> "ENTER") } end for ]-| Note the usage of the "for" regular formula to describe the concatenation of N subsequences corresponding to each process j. The fact that the formula uses a precise order of the occurrence of actions executed by processes j (from 1 to N ) does not restrict its generality, because the absence of a cycle containing a particular ordering of the actions is equivalent to the absence of cycles containing any ordering of these actions (this is similar to the counting construction used for transforming a generalized Büchi automaton into a standard one).

Equivalence checking

Equivalence checking is useful to guarantee that some properties verified on one graph are also satisfied by another. Alternatively, equivalence checking can be used to minimize a graph by collapsing its equivalent states. Concurrency theory produced many graph equivalence relations, including strong bisimulation [104] and branching bisimulation [123], as well as stochastic/probabilistic extensions of strong and branching bisimulations (which take into account the notion of lumpability [START_REF] Kemeny | Finite Markov Chains[END_REF]) for models combining features from Ltss and Markov chains. From the beginning, equivalence checking has been a key feature of Cadp, first with the Aldébaran tool [START_REF] Fernandez | ALDEBARAN : un système de vérification par réduction de processus communicants[END_REF][START_REF] Fernandez | On the Fly" Verification of Behavioural Equivalences and Preorders[END_REF] and, since 1999, with the Bcg Min 1.0 tool for minimization of explicit graphs using various partition-refinement algorithms ( [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF] for strong bisimulation, [START_REF] Groote | An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence[END_REF] for branching bisimulation, and [START_REF] Hermanns | Bisimulation Algorithms for Stochastic Process Algebras and their BDD-based Implementation[END_REF] for stochastic/probabilistic extensions). The functionalities of these two tools have been progressively subsumed by improved tools, namely Bcg Min 2.0 and Bisimulator, available in Cadp 2011.

Bcg Min 2.0 enables an explicit Lts to be minimized according to various equivalence relations. It implements partition-refinement algorithms based on the notion of state signature, originally designed for strong and branching bisimulations [START_REF] Blom | Distributed state space minimization[END_REF]. Intuitively, the signature of a state is the set of all couples "(transition label, block of the target state)" of the outgoing transitions (possibly following some compressed sequence of internal transitions in the case of branching bisimulation). Refinement of the state partition consists in dispatching states with different signatures to different blocks until the fixpoint has been reached, each block thus corresponding to a class of equivalent states. Bcg Min 2.0 extends this algorithm to the stochastic/probabilistic extensions of strong and branching bisimulations, by incorporating lumpability in the computation of signatures.

For strong and branching bisimulations, tests on more than 8000 Bcg graphs show that Bcg Min 2.0 is 20 times faster and uses 1.3 times less memory than Bcg Min 1.0. For stochastic/probabilistic bisimulations, Bcg Min 2.0 is more than 500 (occasionally, 8500) times faster and uses 4 times less memory. Large graphs of more than 10 8 states and 10 9 transitions have been minimized in just a few hours, using less than 100 Gbytes Ram.

Bisimulator [START_REF] Bergamini | BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking[END_REF][START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF][START_REF] Mateescu | Improved On-the-Fly Equivalence Checking using Boolean Equation Systems[END_REF] compares an implicit Lts (usually, describing a protocol ) with an explicit Lts (usually, describing the expected service) on the fly, by encoding the problem as a Bes, which is solved using the linear-time local algorithms of the Caesar Solve [START_REF] Mateescu | CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems[END_REF] library of Cadp. This encoding generalizes and, because of optimizations applied on the fly depending on the Lts structure, outperforms the pioneering on-the-fly equivalence checking algorithms [START_REF] Fernandez | On the Fly" Verification of Behavioural Equivalences and Preorders[END_REF]. For typical cases, e.g., when the service Lts is deterministic and/or free of hidden/invisible (τ ) actions, the tool automatically chooses an appropriate memory-efficient Bes resolution algorithm, which stores only the states, and not the transitions.

Bisimulator implements seven equivalence relations (strong, observational, branching, τ * .a [START_REF] Fernandez | On the Fly" Verification of Behavioural Equivalences and Preorders[END_REF], safety [START_REF] Bouajjani | Safety for Branching Time Semantics[END_REF], trace, and weak trace [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF]) and their associated preorders, thus being one of the richest on-thefly equivalence checkers available. For non-equivalent Ltss, the tool can generate a counterexample, i.e., a directed acyclic graph containing the minimal set of transition sequences that, if traversed simultaneously in the two Ltss, lead to couples of non-equivalent states. Minimal-depth counterexamples can be obtained using breadth-first strategies for Bes resolution. The tool is also equipped with on-the-fly reductions modulo τ -compression (collapse of τ -cycles) and τ -confluence (elimination of redundant interleavings), which preserve branching equivalence and can improve performance by several orders of magnitude.

Besides the classical usage as equivalence checker, Bisimulator is also employed by the Ocis graphical simulator of Cadp in order to check on the fly whether a given execution scenario (represented as an Lts) is accepted or not by the specification under simulation.

Compositional Verification

Compositional verification is a way to avoid state explosion for the enumerative verification of complex concurrent systems which can be expressed as collections of sequential processes composed in parallel, either in a flat or hierarchical manner.

In its simplest form [START_REF] Fernandez | ALDEBARAN : un système de vérification par réduction de processus communicants[END_REF][START_REF] Malhotra | A Tool for Hierarchical Design and Simulation of Concurrent Systems[END_REF]113,127,118,119,122], compositional verification consists in replacing each sequential process by an abstraction, simpler than the original process but still preserving the properties to be verified on the whole system. In Cadp, abstracting a process is done by minimizing its corresponding Lts modulo an appropriate equivalence or preorder relation (e.g., a bisimulation relation, such as strong or branching equivalence). If the system has a hierarchical structure, minimization can also be applied at every intermediate level in the hierarchy. This approach is possible as long as the equivalence or preorder relation is a congruence for the parallel composition operator.

Although this simple form of compositional verification has been applied successfully to some complex systems (e.g., [START_REF] Fernandez | A Toolbox for the Verification of LOTOS Programs[END_REF][START_REF] Chehaibar | Specification and Verification of the Power-Scale Bus Arbitration Protocol: An Industrial Experiment with LOTOS[END_REF] in the case of the Lotos language), it may be counter-productive in some other cases: generating the Lts of each process separately may lead to state explosion, whereas the generation of the whole system of concurrent processes might succeed if processes constrain each other when composed in parallel. This issue has been addressed by refined compositional verification approaches [START_REF] Graf | Compositional Minimization of Finite State Systems[END_REF][START_REF] Cheung | Enhancing Compositional Reachability Analysis with Context Constraints[END_REF]126,[START_REF] Cheung | Compositional Reachability Analysis of Finite-State Distributed Systems with User-Specified Constraints[END_REF][START_REF] Cheung | Context Constraints for Compositional Reachability[END_REF][START_REF] Graf | Compositional Minimisation of Finite State Systems using Interface Specifications[END_REF][START_REF] Krimm | Compositional State Space Generation from LOTOS Programs[END_REF][START_REF] Cheung | Compositional Analysis of Complex Distributed Systems[END_REF][START_REF] Giannakopoulou | Model Checking for Concurrent Software Architectures[END_REF], which enable the Lts of each separate process to be generated by taking into account interface constraints (also known as environment constraints or context constraints). These constraints express the behavioral restrictions imposed on each process by synchronization with its neighbor processes. Taking into account the environment of each process enables the elimination of states and transitions that are not reachable in the Lts of the whole system. Depending on the approach, interface constraints can be either written by the user or generated automatically.

The Cadp toolbox contains various tools dedicated to compositional verification, among which Exp.Open 2.0, Projector 3.0, and Svl play a central role (in addition to Bcg Min already presented in Section 6).

Exp.Open 2.0 is a compiler that takes a network of communicating Ltss in the Exp language, compiles it into an intermediate model based on synchronization vectors, and finally produces an Open/Caesar graph module. Exp.Open 2.0 implements partial order reductions preserving either (stochastic) branching bisimulation, weak traces, or deadlocks.

Projector 3.0 implements behaviour abstraction [START_REF] Graf | Compositional Minimisation of Finite State Systems using Interface Specifications[END_REF][START_REF] Krimm | Compositional State Space Generation from LOTOS Programs[END_REF] of a process given as an Open/Caesar graph module, by taking into account interface constraints provided in the form of an Lts (the environment of the process) and a set of labels (on which the graph module interacts with its environment). The output is an Lts in the Bcg format. If the interface constraints are written by the user, then validation predicates are generated in the Lts and checked afterwards by Exp.Open, when composing the resulting Lts with its environment.

Svl (Script Verification Language) [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF][START_REF] Lang | Compositional Verification using SVL Scripts[END_REF] is both a high level language for expressing complex verification scenarios and a compiler dedicated to this language. Svl can be seen as a process algebra extended with operations on Ltss, e.g., minimization (also called reduction), abstraction, comparison, deadlock/livelock detection, etc., which orchestrates calls to the Cadp tools.

The order in which processes are composed and minimized influences the efficiency of compositional verification. Svl thus implements various compositional verification strategies, in which the order can be either specified by the user (explicitly, or implicitly through the hierarchy of the concurrent processes), or determined automatically using heuristics such as "smart reduction" [START_REF] Crouzen | Smart Reduction. In Proceedings of Fundamental Approaches to Software Engineering FASE[END_REF] (also enabling orders that are independent of the hierarchy of concurrent processes).

Figure 7 illustrates the compositional Lts generation of "mcs.bcg", an instance of the Mcs queue lock for five processes where only the gates "ENTER" and "LEAVE" are made observable, followed by its comparison with the expected service modulo branching bisim- ulation. A diagnostic of the comparison is stored in file "mcs diag branching.bcg". The file "mcs.lnt" contains the code shown in Figure 1, where in addition each process "Pi [NCS, ENTER, LEAVE, L, M]" (i ∈ 1..5) is defined as the instance "P [NCS, ENTER, LEAVE, L, M] (Pid (i))" and where the process "Service" models the expected service. The value 7 of variable DE-FAULT SMART LIMIT indicates that any combination of no more than seven processes can be selected at each step of compositional Lts generation. In this example, all seven processes are first minimized and then composed all together in a single step, producing an Lts with 408, 762 states and 2, 043, 810 transitions. By contrast, direct generation produces an Lts that is about ten times larger (4, 231, 969 states and 21, 159, 845 transitions). The Lts "mcs.bcg" reduces finally to 651 states and 1295 transitions.

Performance Evaluation

During the last decade, Cadp has been enhanced for performance evaluation operating on extended Markovian models encoded in the Bcg format (see details in [START_REF] Coste | Ten Years of Performance Evaluation for Concurrent Systems Using CADP[END_REF]).

In the example of the Mcs queue lock, an interactive Markov chain [START_REF] Hermanns | Interactive Markov Chains and the Quest for Quantified Quality[END_REF] can be obtained by first inserting symbolic delay transitions "Lambda", "Mu", and "Nu" in the Lotos NT model, for instance by parallel composition with a dedicated process "Latency" shown in Besides Bcg Min (which supports stochastic/probabilistic extensions of strong and branching bisimulations), the Exp.Open tool [START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF] now supports also the parallel composition of extended Markovian models, implementing maximal progress of internal transitions in choice with stochastic transitions. New tools have been added, namely Determinator [START_REF] Hermanns | A Set of Performance and Dependability Analysis Components for CADP[END_REF], which eliminates stochastic nondeterminism in extended Markovian models on the fly using a variant of the algorithm presented in [START_REF] Deavours | An Efficient Well-Specified Check[END_REF], and the Bcg Steady and Bcg Transient tools, which compute, for each state s of an extended Markovian model, the probability of being in s either on the long run (i.e., in the "steady state") or at each time instant t in a discrete set provided by the user. These tools can also compute the throughputs of transitions chosen by the user.

More recently, the new Cunctator on-the-fly steady-state simulator for extended Markovian models has been added to Cadp. The tool explores a random execution sequence in the model until a non-Markovian transition or a deadlock state is found, or the sequence length or virtual time (obtained by summing up the Markovian information present on transitions) reaches a maximum value specified by the user, or the user interactively halts the simulation. Upon termination, the throughputs of labeled transitions chosen by the user are displayed, together with information such as the number of τ -transitions encountered and the presence of nondeterminism (i.e., states with more than one outgoing τtransition). The context of a simulation can be saved and restored for starting subsequent simulations, enabling one to implement convergence criteria (e.g., based on confidence intervals) by executing series of increasingly long simulations in linear time. For nondeterministic models, Cunctator selects between conflicting τtransitions according to one of three scheduling policies (the first, the last, or a randomly chosen transition). Thus, launching simulations using different scheduling policies provides more insight about the stochastic behavior of the model. Compared to Bcg Steady, which computes exact throughputs, Cunctator consumes less memory but achieving the same accuracy may require more time.

In the Mcs example, Bcg Steady or Cunctator can be used to study the performance by computing the throughput of the transitions labeled with "ENTER" (see [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF] for more details).

Parallel and Distributed Methods

Verification algorithms based on state space exploration have high computing and memory requirements and, thus, are often limited by the capabilities of one single sequential machine. However, the limits can be pushed out by new algorithms capable of exploiting processing resources offered by networks of workstations, clusters, grids, etc.

Cadp was among the first toolboxes to release tools for distributed model checking. The first step was to parallelize the state space construction, which is a bottleneck for verification because storing all reachable states requires a considerable amount of memory. For this purpose, the Distributor and Bcg Merge tools [START_REF] Garavel | Parallel State Space Construction for Model-Checking[END_REF][START_REF] Garavel | DISTRIBUTOR and BCG MERGE: Tools for Distributed Explicit State Space Generation[END_REF] split the generation of an Lts across several machines, each machine building only a fragment of the entire Lts. Interestingly, certain essential Distributor features, such as the Pbg (Partitioned Bcg Graph) format and the graphical monitor that displays in real-time the progress of generation across all the machines, have been replicated in competing verification toolsets.

The second step was the integration into Cadp 2011 of a collection of new software tools (Pbg Cp, Pbg Mv, Pbg Rm, and Pbg Open) to manipulate an Lts in the Pbg format, and their connection to Open/Caesar.

The third step was the parallelization of on-the-fly verification itself. Therefore we designed a distributed version of the Caesar Solve library to solve Boolean equation systems on the fly using several machines, thus enabling the development of parallel model and equivalence checkers.

Applications

As much as possible, we try to confront Cadp with complex (often industrial) case studies in several domains. Distributed systems. In collaboration with academic teams and industrial companies, we have used Cadp for modeling and analysing various distributed middleware protocols and systems. We can mention the following:

the consensus protocol used by the CO4 distributed knowledge system [106] -a cluster file system built on top of Arias, a virtual shared memory across distributed machines running Aix [107] -a dynamic reconfiguration protocol for agent-based applications [START_REF] Cornejo | Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications[END_REF] the deployment of the Scalagent platform for distributed Java agents [121], in the framework of a collaborative project aimed at the implementation of a safe, flexible architecture (based on Java components) enabling the remote management of uninterruptible power supplies the Synergy reconfiguration protocol [START_REF] Boyer | Specifying and Verifying the Synergy Reconfiguration Protocol with LOTOS NT/CADP[END_REF] a self-configuration protocol for distributed applications in the cloud [114] In addition to verification, the performance evaluation features of Cadp have been applied to compare 27 mutual exclusion protocols in the shared memory setting [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF].

High-performance computing. High-performance computing, particularly cache coherency protocols [START_REF] Chehaibar | Specification and Verification of the Power-Scale Bus Arbitration Protocol: An Industrial Experiment with LOTOS[END_REF], has been a recurrent topic since 1996 in the framework of a collaboration with Bull, the European leader in this field. Notably, we have used Cadp to verify critical parts of the Tera 10 super-computer (installed at Cea), which was Europe's most powerful computer in 2006. 10 We have also used Cadp to evaluate the performance of the Scsi-2 bus arbitration protocol [START_REF] Garavel | On Combining Functional Verification and Performance Evaluation using CADP[END_REF] and of Mpi implementations on Cc-Numa architectures [START_REF] Chehaibar | Modeling Multiprocessor Cache Protocol Impact on MPI Performance[END_REF]. Embedded systems on chip. The formal modeling, functional verification, and performance evaluation of hardware architectures with a high degree of asynchronous concurrency have been the subject of collaborations with Bull, STMicroelectronics, and the Cea/Leti laboratory (Grenoble, France) since 2004. A first step was the development of a translation from the Chp description language for asynchronous circuits into Lotos, subsequently enabling verification with Cadp [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF]. We have used Cadp to study the performance prediction of the xSTream architecture [START_REF] Coste | Towards Performance Prediction of Compositional Models in Industrial GALS Designs[END_REF], a complex graphical processing unit described in SystemC/Tlm [START_REF] Garavel | Verification of an Industrial SystemC/TLM Model using LOTOS and CADP[END_REF], and the dynamic task dispatcher of the Platform 2012 architecture [START_REF] Lantreibecq | Model Checking and Cosimulation of a Dynamic Task Dispatcher Circuit Using CADP[END_REF].

Avionics. We have used Cadp in the framework of collaborations with Airbus since 2005. In particular, we have developed a connection from the Fiacre intermediate language [START_REF] Berthomieu | FI-ACRE: An Intermediate Language for Model Verification in the TOPCASED Environment[END_REF] to Cadp. We have also verified several avionics systems using Cadp, namely a ground/plane communication protocol based on Tftp [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF], an equipment failure management protocol and an air-traffic control subsystem 11 .

The Cadp Web site also provides 40 properly packaged and documented case studies 12 . Other researchers from many institutions worldwide have also applied Cadp to real case studies; a comprehensive database of 152 such case studies (from 1990 to 2011) published in the scientific literature is available on line 13 . The case studies cover application domains as diverse as the following (in alphabetical order): avionics, bioinformatics, business processes, cognitive systems, communication protocols, component-based systems, constraint programming, control systems, coordination architectures, critical infrastructures, cryptography, database protocols, distributed algorithms, distributed systems, e-commerce, e-democracy, embedded software, grid services, hardware design, hardware/software co-design, healthcare, human-computer interaction, industrial manufacturing systems, middleware, mobile agents, model-driven engineering, networks, object-oriented languages, performance evaluation, planning, radiotherapy equipment, real-time systems, security, sensor networks, service-oriented computing, software adaptation, software architectures, stochastic systems, systems on chip, telephony, transport safety, and Web services.

Conclusion

Concurrency theory is now 40-year old; formal methods are 35-year old; model checking verification is nearly 30-11 http://gforge.enseeiht.fr/docman/view.php/52/4316/ B4-INRIA_VASY.pdf 12 http://cadp.inria.fr/demos.html 13 http://cadp.inria.fr/case-studies year old. To push theoretical ideas into reality and to obtain new scientific results, significant effort must be put into software development and confrontation with industrial applications.

This was indeed the case with Cadp 2011 which, besides all aforementioned new tools and major enhancements, also required large amounts of programming work: porting to various processors (Itanium, PowerPC, Sparc, x86, x64), operating systems (Linux, Mac OS X, Solaris, Windows) and C compilers (gcc 3, gcc 4, Intel, and Sun); careful code cleanup to remove all compiler and lint warnings, not only in the C code of the Cadp tools themselves, but also in the C code that they may generate (this ensures that all compiler warnings received by end-users are related to some mistakes in their Lotos or Lotos NT code); significant documentation effort; intensive nonregression testing using thousands of Lotos and Lotos NT programs, Bcg files, temporal logic formulas, Boolean equation systems, etc. together with a new tool named Contributor that will allow Cadp users to send such test cases to the Vasy team.

The relevance of these efforts and the maturity of Cadp can be estimated from its dissemination and impact figures. Cadp is distributed free of charge to universities and public research centers (academic licenses) and commercially to companies (professional licenses). As of July 2011, academic and commercial licences have been signed with more than 441 universities, public research institutes, and global corporations. Since July 2011, the academic distribution scheme was simplified: a signed license contract is no longer required, and Cadp is now immediately available to (1) any scientist who can demonstrate employment in a university or a public research center by providing a valid professional e-mail address and Web page, and (2) any student who matches the above conditions or who is recommended by a professor.

As of January 2012, 152 case-studies have been tackled using Cadp (see Section 10); 61 research software applications have been developed using Cadp14 ; numerous academic courses are using Cadp to teach concurrency 15 ; the Cadp user forum currently gathers more than 200 registered members with 1340 messages exchanged.

Regarding future work, we plan to develop a native Lotos NT compiler, to connect even more concurrent languages to Cadp, and add new verification tools that exploit massively parallel computing platforms. The latter research area is especially difficult, because it superposes the algorithmic complexities of verification and of distributed programming; yet this is the only way to exploit parallel computing resources, which are becoming pervasive.

Fig. 1 .

 1 Fig. 1. Lotos NT model of the Mcs queue lock (excerpt -an instantation of the Mcs queue lock for five processes is shown in Figure 2)

Fig. 2 .

 2 Fig. 2. Instantiation of the Mcs queue lock for five processes

Fig. 3 .

 3 Fig. 3. Mcs queue lock for five processes in the Exp 2.0 language

Fig. 5 .

 5 Fig. 5. Bcg Edit

Fig. 6 .

 6 Fig. 6. Open/Caesar Interactive Simulator

5

 5 Model CheckingCadp contains three model checkers operating on explicit and implicit Ltss.

9 .

 9 Evaluator 4.0 [101] is a new model checker handling formulas written in Mcl (Model Checking Language), which conservatively extends Rafmc with two kinds of features. First, Mcl adds data-handling mechanisms to parse and exploit structured transition labels (containing a channel/gate name and a list of values exchanged), generated from value-passing specification languages.

Fig. 7 .

 7 Fig. 7. Compositional generation and verification with Svl

Fig. 8 .

 8 Fig. 8. Delay insertion for the Mcs queue lock

Figure 8 ,

 8 Figure 8, and subsequently instantiating these symbolic transitions with concrete rates by renaming the corresponding transitions in the generated Lts.Besides Bcg Min (which supports stochastic/probabilistic extensions of strong and branching bisimulations), the Exp.Open tool[START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF] now supports also the parallel composition of extended Markovian models, implementing maximal progress of internal transitions in choice with stochastic transitions. New tools have been added, namely Determinator[START_REF] Hermanns | A Set of Performance and Dependability Analysis Components for CADP[END_REF], which eliminates stochastic nondeterminism in extended Markovian models on the fly using a variant of the algorithm presented in[START_REF] Deavours | An Efficient Well-Specified Check[END_REF], and the Bcg Steady and Bcg Transient tools, which compute, for each state s of an extended Markovian model, the probability of

  10 http://vasy.inria.fr/doc/inedit-69-en.pdf

-

  Relying on action-based models enables equivalence checking, i.e., the comparison of specifications for equality or inclusion; this corresponds to the notions of bisimulations for Ltss and aggregation/lumpability for Markov chains. Also, the possibility of replacing a state space by an equivalent but smaller one is fundamental in compositional verification.

-As a consequence, the model checkers of Cadp are based on branching-time (rather than linear-time) logics, which are adequate with bisimulation reductions. -Cadp is equipped with an original software architecture designed to enable modularity in model checking tools. Early model checkers (such as Cesar [110,

  gives a global picture; dark grey boxes indicate the languages and software components included in Cadp 2011; light grey boxes indicate the languages for which Vasy has developed translators and connections to Cadp 2011, these translators being distributed separately from Cadp 2011; arcs are labeled

	Sam	eb3	Wsdl-Bpel	π-calculus	Sdl	Aadl
	[58]	[20]	[120]		[98]		[5]
	Bip	Fsp	Lotos NT	Fiacre	Chp
	[81]		[85]	[13]	[5]	[53]
		Exp	Lotos	[69, 109]	SystemC/Tlm
			[39, 55, 54]
		[84]			[68]
			Open/Caesar

Fig. 4. Connection of the input languages of Cadp 2011 hide all but "ENTER", "LEAVE" in par M, L in par in "P1.bcg" || "P2.bcg" || "P3.bcg" || "P4.bcg" || "P5.bcg" end par || par in "Lock.bcg" || "Memory.bcg" end par end par end hide

http://cadp.inria.fr

http://en.wikipedia.org/wiki/List_of_Model_Checking_Tools

http://anna.fi.muni.cz/yahoda

http://cadp.inria.fr/resources/benchmark_bcg.html

http://divine.fi.muni.cz/

http://fmt.cs.utwente.nl/tools/ltsmin

http://www.comp.nus.edu.sg/~pat

http://cadp.inria.fr/software

http://cadp.inria.fr/training

Acknowledgments. The authors are grateful to H. Hermanns (Saarland University) and to I. Bellicot, S. Bouland, D. Champelovier, X. Clerc, N. Coste, J. Fereyre, Y. Genevois, Y. Guerte, C. Helmstetter, J. Henri, R. Hérilier, A. Kaufmann, R. Lacroix, N. Lépy, C. McKinty, S. Mériot, J. Merle, E. Oudot, L. Paternault, O. Ponsini, V. Powazny, S. Robert, G. Salaün, G. Smeding, J. Stöcker, D. Thivolle, M. Vidal, A. Wijs, and M. Zidouni (Inria/Vasy), who contributed during the past five years to software development, porting, testing, and/or maintenance of Cadp. The authors are also grateful to the 40 scientists outside Vasy who reported bugs and suggestions for enhancements during that period.