Dimitris Vekris

Frédéric Lang

Catalin Dima

Radu Mateescu

Verification of EB3 specifications using CADP

Keywords: Process Algebras, Information Systems, eb 3, LOTOS NT, Model Checking, Verification

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The eb 3 method [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] is an event-based paradigm tailored for information systems (ISs). eb 3 has been used in the research projects selkis [MIL + 11] and eb 3 sec [JFG + 10], whose primary aim is the formal specification of ISs with security policies. In the eb 3 sec project, real banking industry case studies have been studied, describing interaction with brokers, customers and external financial systems. The selkis project deals with two case studies from the medical domain. The first one draws data records from medical imaging devices. The access to these records is done via web-based applications. The second one deals with availability and confidentiality issues for medical emergency units evolving in a great mountain range, like the Alps in that case.

A typical eb 3 specification defines entities, associations, and their respective attributes. The process algebraic nature of eb 3 enables the explicit definition of intra-entity constraints, making them easy for the IS designer to review and understand. Yet, its particular feature compared to classical process algebras, such

Correspondence and offprint requests to: Dimitris Vekris, Email: Dimitrios.Vekris@u-pec.fr as CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], lies in the use of attribute functions, a special kind of recursive functions evaluated on the system execution trace. Combined with guards, attribute functions facilitate the definition of complex inter-entity constraints involving the history of events. The use of attribute functions simplifies system understanding, enhances code modularity, and streamlines maintenance. However, given that ISs are complex systems involving data management and concurrency, a rigorous design process based on formal specification using eb 3 must be completed with effective formal verification features.

Existing attempts for verifying eb 3 specifications are based on translations from eb 3 to other formal methods equipped with verification capabilities. A first line of work [START_REF] Gervais | Synthesizing B Specifications from eb 3 Attribute Definitions[END_REF][START_REF] Gervais | Refinement of eb 3 Process Patterns into B Specifications[END_REF] focused on devising translations from eb 3 attribute functions and processes to the B method [START_REF]The B-Book -Assigning programs to meanings[END_REF], which opened the way for proving invariant properties of eb 3 specifications using tools like Atelier B [Cl]. The B method is mainly used to verify safety properties over system specifications. A full-scale verification of B specifications is impossible under the classical B method. As a result, the B models of [START_REF] Gervais | Synthesizing B Specifications from eb 3 Attribute Definitions[END_REF][START_REF] Gervais | Refinement of eb 3 Process Patterns into B Specifications[END_REF] were not suitable for verifying liveness properties.

On the other hand, it is known that temporal logic can deal both with safety and liveness properties. Hence, another approach concerned with the verification of temporal logic properties of eb 3 specifications by means of model checking techniques was taken. For this purpose, the formal description and verification of an IS case-study using six verification tools was undertaken in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF][START_REF] Chossart | Évaluation d'outils de vérification pour les spécifications de systèmes d'information[END_REF]. This study revealed the necessity of branching-time logics for accurately characterizing properties of ISs, and also the fact that process algebraic languages are suitable for describing the behaviour and synchronization of IS entities. However, no attempt of providing a systematic translation from eb 3 to a target language accepted as input by a model checker was made so far.

At first sight, given that eb 3 has structured operational semantics based on a labelled transition system (LTS) model, its translation to a process algebra may seem straightforward. However, this exercise proved to be rather complex, the main difficulty being to translate a history-based language (the control-flow depends on the entire system trace) to a process algebra with standard LTS semantics. On the other hand, the original trace-based semantics defined for finite-state systems in [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] denoted Sem T gives rise to unbounded memory models as the current trace is part of the current system state and, therefore, in the absence of good abstractions capable of reducing them to finite-state models, only bounded model-checking can be applied [BCC + 99]. This restriction is present in the original approach [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] and the subsequent model-checking attempt [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] even if all entities considered in the IS are finite.

To overcome this difficulty, [START_REF] Vekris | Efficient Operational Semantics eb 3 for Verification of Temporal Properties[END_REF] proposes a formal semantics for eb 3 that treats attribute functions as state variables, the so-called attribute variables. Intuitively, coding attribute functions as part of the system state is beneficial from a model-checking point of view as the new formalisation dispenses with the system trace. The derived memory semantics denoted Sem M serves as the basis for applying a simulation strategy of attribute variables in LNT, a new generation process algebraic specification language inspired from E-LOTOS [START_REF]ISO/IEC. Enhancements to LOTOS (E-LOTOS)[END_REF]. In the same paper, Sem M are shown to be equivalent to Sem T . Again no complete translation of eb 3 to LNT is provided. Contribution 1. Based on the efficient memory Sem M given in [START_REF] Vekris | Efficient Operational Semantics eb 3 for Verification of Temporal Properties[END_REF], we propose a rigorous translation algorithm from eb 3 to LNT [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator -Version 5[END_REF]. As far as we know, this is the first attempt to provide a general translation from eb 3 to a classical value-passing process algebra. Since our primary objective was to provide temporal property verification features for eb 3 , we focused our attention on LNT, which is one of the input languages accepted by the CADP verification toolbox [START_REF] Garavel | CADP 2010: A toolbox for the construction and analysis of distributed processes[END_REF], and hence is equipped with on-the-fly model checking for action-based, branching-time logics involving data. Another important ingredient of the translation was the multiway value-passing rendezvous of LNT, which enabled to obtain a one-to-one correspondence between the transitions of the two LTSs underlying the eb 3 and LNT descriptions, and hence to preserve strong bisimulation. The presence of array types and of usual programming language constructs (e.g., loops and conditionals) in LNT was also helpful for specifying the memory, the Kleene star-closure operators, and the eb 3 guarded expressions containing attribute function calls. At last, the constructed data types and pattern-matching mechanisms of LNT enabled a natural description of eb 3 data types and attribute functions. 2. We implemented our translation in the eb 3 2lnt tool, thus making possible the analysis of eb 3 specifications using all the state-of-the-art features of the CADP toolbox, in particular the verification of data-based temporal properties expressed in MCL [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] using the on-the-fly model checker EVALUA-TOR 4.0. The formal correctness proof of equivalence for eb 3 specifications and the corresponding LNT specifications can be found in [START_REF] Vekris | Verification of eb 3 specifications with the aid of model-checking techniques[END_REF].

The paper is organized as follows:

• Section 2 presents the functional requirements of an IS and the related eb 3 specification that serves as the basis for introducing eb 3 's syntax in Section 3. • Section 4 discusses the verification requirements that will be addressed in this paper and Section 5 explains why existing literature does not suffice to address them. • Section 6 presents the memory semantics Sem M of eb 3 and compares it in terms of efficiency to the standard traced-based semantics Sem T . • Section 7 gives an overview of the eb 3 and LNT languages.

• Section 8 introduces MCL briefly.

• Section 9 presents our translation from eb 3 to LNT, implemented by the eb 3 2lnt translator.

• Section 10 shows how eb 3 2lnt, CADP and MCL can be used for verifying the correctness requirements of an IS. • Section 11 summarizes the results and draws up lines for future work.

Example

We present the syntax of eb 3 by way of an intuitive example. First, we give the functional requirements of a library management system: R1. A book can be acquired by the library. It can be discarded, but only if it has not been lent. R2. An individual must join the library in order to borrow a book. R3. A member can relinquish library membership only when all his loans have been returned. R4. A member cannot borrow more than the loan limit defined at the system level for all users.

The eb 3 specification intended to satisfy these requirements is presented in Figure 1. Note that process main is the parallel interleaving between m instances of process book executed an arbitrary but bounded number of times (Kleene Closure * ) and p instances of process member executed an arbitrary but bounded number of times. Process book stands for a book acquisition "Acquire (bId )" followed by its eventual discard "Discard (bId )". The attribute function "borrower (T, bId )" looks for actions of the form "Lend (mId , bId )" or "Return (bId )" in the trace T and returns the current borrower of book bId denoted as "borrower (front (T), bId )" or ⊥ if the book is not lent. In process book , action "Discard (bId)" is thus guarded to guarantee that book bId cannot be discarded if it is currently lent. Process loan stands for a book loan "Lend (bId , mId )" followed by an eventual return to the library "Return (bId )". The attribute function "nbLoans (T, mId )" inspects for actions of the form "Lend (bId , mId )" incrementing the current number of mId 's loans and inspects for actions of the form "Return (bId )" decrementing the current number of mId 's loans. In process loan, action "Lend (bId , mId )" is thus guarded to guarantee that book bId is not currently being lent and member mId 's loans is inferior to NbLoans. Process member stands for a member registration followed by an arbitrary but bounded number of loans and an eventual membership annulment.

The Language EB 3

The eb 3 method has been specially designed to specify the functional behaviour of ISs. A standard eb 3 specification comprises:

1. a class diagram representing entity types and associations for the IS being specified, 2. a process algebra specification, denoted by main, describing the IS, i.e., the valid traces of execution describing its behaviour, 3. a set of attribute function definitions, which are recursive functions on the system execution trace, and 4. input/output rules to specify outputs for input traces, or SQL expressions used to specify queries on the class diagram. We limit the presentation to the process algebra and the set of attribute functions. The eb 3 syntax is presented in Figure 2 and the eb 3 memory semantics Sem M [START_REF] Vekris | Efficient Operational Semantics eb 3 for Verification of Temporal Properties[END_REF] are given in Figure 3 as a set of Rules named M 1 to M 11 . Both figures are commented below. The equivalence of the original trace semantics Sem T [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] and Sem M can be found in [START_REF] Vekris | Efficient Operational Semantics eb 3 for Verification of Temporal Properties[END_REF].

) : T = match last (T) with ⊥ : v 0 | α 1 (x 1 ) : v 1 | . . . | α q (x q ) : v q [| : v q+1 ] S ::= P (x) = E E ::= λ α (v) E 1 .E 2 E 1 | E 2 E 0 * E 1 |[∆]| E 2 |x : V : E 0 |[∆]|x : V : E 0 C ⇒ E P (v)
We write x, y, x 1 , x 2 , . . . for variables and v, w, v 1 , v 2 , . . . for data expressions over user-defined domains, such as integers, Booleans and more complex domains that we do not give formally, for conciseness. Let Act be a set of actions written ρ, ρ 1 , ρ 2 , . . . and Lab be a set of labels written α, α 1 , α 2 , . . .. Each action ρ is either the internal action written λ, or a visible action of the form "α (v)", where α ∈ Lab. Hence, visible actions consist of labels and data vectors. The notion of eb 3 actions coincides with the notion of CSP internal actions [START_REF] Hoare | Communicating Sequential Processes[END_REF]. We also use the overlined notation as a shorthand notation for lists, e.g., x denotes a list of variables x 1 , . . . , x n of arbitrary length. An eb 3 specification consists of a set of attribute function definitions A 1 , . . . , A n , and of a set of process definitions of the form "P (x) = E", where P is a process name and E is a process expression.

Attribute functions. Attribute function definitions are denoted by the symbol A in the grammar of Figure 2. We assume a set of labels Lab = {α 1 , . . . , α q } (λ not included). Each α j has formal parameters x j . Attribute functions {f 1 , . . . , f n } are defined recursively on the current trace T representing the history of actions with the aid of functions last (T) which denotes the last action of the trace, and front (T) which denotes the trace without its last action. The symbol ⊥ represents the undefined value. In particular, both

(M 1 ) ρ ρ -→ √ (M 7 ) E 1 ρ -→ E 1 E 2 ρ -→ E 2 E 1 |[∆]| E 2 ρ -→ E 1 |[∆]| E 2 in (ρ, ∆) (M 2 ) E 1 ρ -→ E 1 E 1 .E 2 ρ -→ E 1 .E 2 (M 8 ) E 1 ρ -→ E 1 E 1 |[∆]| E 2 ρ -→ E 1 |[∆]| E 2 ¬in (ρ, ∆) (M 3 ) E 2 ρ -→ E 2 √ .E 2 ρ -→ E 2 (M 9 ) √ |[∆]| √ λ -→ √ (M 4 ) E 1 ρ -→ E 1 E 1 | E 2 ρ -→ E 1 (M 10 ) E 0 ρ -→ E 0 C ⇒ E 0 ρ -→ E 0 C [ f (T, v) := f[ v ] ] (M 5 ) E 0 * λ -→ √ (M 11 ) E[x := v] ρ -→ E P (v) ρ -→ E P (x) = E (M 6 ) E 0 ρ -→ E 0 E 0 * ρ -→ E 0 .E 0 *
Fig. 3. eb 3 memory semantics Sem M last (T) and front (T) match ⊥ when the trace is empty. The symbol (wildcard) matches all actions not matched by any of the preceding action patterns α 1 (x 1 ), . . . , α q (x q ). Note that the attribute functions f i share the same vector of formal parameters y, which we call attribute vector 1 , modulo renaming, and, therefore, have the same arity, which is by no means restrictive in terms of language expressiveness. Each v i for i ∈ {0, . . . , n} is an expression of the same type as f 's return type built over the variables y ∪ x i . In real eb 3 specifications with distinct formal parameters y i each corresponding to every f i , y can be formalized as the union of the y i , i ∈ 1..n. We also assume that the attribute functions are ordered, so that for all h ∈ 1..n, i ∈ 1..n, j ∈ 1..q, every function call of the form "f h (T, . . .)" occurring in w j i satisfies h < i and every call of the form "f h (front (T), . . .)" satisfies h ≥ 0. Such an ordering can be constructed if the eb 3 specification does not contain circular dependencies between function calls, which would potentially lead to infinite attribute function evaluation. In particular, the definition of an attribute function f i cannot contain recursive calls of the form "f i (T, . . .)", but only recursive calls of the form "f i (front (T), . . .)". Note that this does not limit the expressiveness of eb 3 attribute functions, because every recursive computation on data expressions only (which keeps the trace unchanged) can be described using standard functions and not attribute functions. The eb 3 specification of Figure 1 satisfies this ordering, as the definition of borrower contains calls of the form "borrower (front (T), bId )", while the definition of nbLoans contains calls of the form "nbLoans (front (T), mId )" and "borrower (T, bId )".

Process expressions. Expressions are built over variables, constants, and standard operations. An action ρ is the simplest process expression, whose semantics are given by Rule M 1 . The symbol √ (which is not part of the user syntax) denotes successful execution. The trace T of an eb 3 specification at a given moment consists of the sequence of visible actions executed since the start of the system. (Note therefore that λ does not appear in the trace.) At system start, the trace is empty. If T denotes the current trace and action ρ can be executed, then T.ρ denotes the trace just after executing ρ.

eb 3 processes can be combined with classical process algebra operators such as the sequence "E 1 .E 2 " (M 2 , M 3 ), the choice "E 1 | E 2 " (M 4 ) and the Kleene closure "E 0 * " (M 5 , M 6 ). Rules (M 7 to M 9 ) define parallel composition "E 1 |[∆]| E 2 " of E 1 , E 2 with synchronization on ∆ ⊆ Lab. The condition "in (ρ, ∆)" is true iff the label of ρ belongs to ∆. The symmetric Rules for choice and parallel composition have been omitted for brevity. Expressions "E 1 ||| E 2 " and "E 1 || E 2 " are equivalent respectively to "E

1 |[∅]| E 2 " and "E 1 |[Lab]| E 2 ".
1 each y ∈ y is called attribute parameter correspondingly Quantification is permitted for choice and parallel composition. If V is a set of expressions {v 1 , . . . , v n }, "|x : V : E 0 " and "|[∆]|x : V : E 0 " stand respectively for "E 0

[x := v 1 ] | . . . | E 0 [x := v n ]" and "E 0 [x := v 1 ] |[∆]| . . . |[∆]| E 0 [x := v n ]"
, where "E[x := v]" denotes the replacement of all occurrences of x by v in E. For instance, "||x : {1, 2, 3} : a (x)" stands for "a (1) || a (2) || a (3)".

At last, named processes can be instantiated as usual (M 11 ). Given an eb 3 process expression E, we write vars (E) for the set of variables occurring free in E.

Verification Requirements

We need to verify that the eb 3 specification of Figure 1 satisfies the functional requirements of the simplified library management system presented in Section 2. To this end, we divide them into liveness and safety properties. Liveness properties express the possibility that a certain event will take place and safety properties express the certitude that a certain event will never take place. Requirements R1 and R3 are typical liveness properties and requirements R2 and R4 are typical safety properties.

Related Works

Following the technique of [START_REF] Gervais | Synthesizing B Specifications from eb 3 Attribute Definitions[END_REF][START_REF] Gervais | Refinement of eb 3 Process Patterns into B Specifications[END_REF], one may devise a translation from the eb 3 specification of Figure 1 to the B method. This approach suffices to verify requirements R2 and R4, since safety properties can be formalized in the B method, but the verification of requirements R1 and R3 cannot be addressed by way of classical refinement techniques. An important class of liveness properties can be verified in Event-B [START_REF]Modeling in Event-B: System and Software Engineering[END_REF] as explained in [START_REF] Hoang | Reasoning about liveness properties in Event-B[END_REF][START_REF] Groslambert | Verification of LTL on B Event System[END_REF]. In [START_REF] Hoang | Reasoning about liveness properties in Event-B[END_REF], the system is defined as an Event-B model and the liveness property φ in question is expressed in Linear Tree Logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF]. Then, the Büchi automaton corresponding to φ is translated to an equivalent Event-B model that is added to the initial Event-B model. Finally, the consistency of the final model implies the satisfaction of φ. In [START_REF] Groslambert | Verification of LTL on B Event System[END_REF], the liveness property φ is expressed as proof obligations of the Event-B model, whose resolution implies the satisfaction of φ. More recent work [STW + 14] in the field sets a framework for preserving liveness and fairness properties in LTL along successive refinement steps of Event-B machines. The refinement of events is allowed among the possible refinement steps of this scheme.

However, the use of LTL is usually inadequate for the verification of liveness properties over ISs. The reason lies in the presence of loops in the IS specification leading to infinite paths. To see this, let's consider a certain class of liveness properties called reachability properties. Reachability properties can be expressed in Computational Tree Logic (CTL) [START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF] formulas "AG(ψ ⇒ EF φ)" that are satisfied if for all states that are reachable from the initial states of the system, where formula ψ is valid, there is a sequence of transitions that lead to states of the system, where formula φ is valid. Reachability properties cannot be expressed and verified in LTL. Instead, only branching-time logics like CTL can be used for this purpose. Hence, the verification techniques of [HA11, Gro06, STW + 14] are not applicable here.

In [ETL + 04], the authors propose the translation of eb 3 specifications to equivalent CSP B [ST05, TSB03] specifications. CSP B is an hybrid method that combines features of CSP and the B method. The dynamic behaviour of the IS in question is directly cast to a CSP specification. CSP shares common process algebraic features with eb 3 . The system state inherent to the attribute function definitions has to be defined explicitly via the state variables of a B specification. Then, every CSP action execution triggers a unique operation of the B specification that has an immediate effect on the state variables. The properties over the CSP B specification have to be expressed in CSP and the verification is carried out by the FDR2 model checker [START_REF]Failures-Divergences Refinement[END_REF]. Liveness properties expressed as temporal properties can be cast to FDR2 as explained in [START_REF] Leuschel | How to make FDR spin: LTL model checking of CSP by refinement[END_REF]. As a result, both liveness and safety properties of the library specification can be verified with the aid of refinement checking and the FDR2 model checker. Although the method of [ETL + 04] is systematic, the translation of eb 3 specifications to equivalent CSP B models is not automatic, but still necessitates user intervention.

On the other hand, it is known that temporal logic can deal both with safety and liveness properties. Hence, another approach concerned with the verification of temporal logic properties of eb 3 specifications by means of model checking techniques is taken. For this purpose, the formal description and verification of the library management system specification [START_REF] Gervais | Combinaison de spécifications formelles pour la modélisation des systèmes d'information[END_REF] using six verification tools are undertaken in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF][START_REF] Chossart | Évaluation d'outils de vérification pour les spécifications de systèmes d'information[END_REF] namely SPIN [START_REF] Holzmann | The Spin Model Checker: Primer and Reference Manual[END_REF], NuSMV [CCG + 02], FDR2, CADP, ALLOY [START_REF] Jackson | Software Abstractions[END_REF] and ProB [START_REF] Leuschel | ProB: A model checker for B[END_REF]. SPIN, CADP and FDR2 are called explicit model checkers. In CADP and FDR2, the transition system describing the system specification is constructed explicitly prior to the property verification, whereas in the case of SPIN, the property is verified while the transition system is constructed in parallel (on-the-fly verification). Nu-SMV belongs to a group of model-checkers called symbolic model checkers. In symbolic model checking language specifications, the transition system is given in the form of Boolean formula. ALLOY is a language based on first-order logic. Moreover, ALLOY models are defined purely as sets and relations on these sets. Properties are expressed as boolean expressions and verification is reduced to the SAT problem. It is worth mentioning that ALLOY's language used to model the system is the same as the language used to specify the property we need to verify. The same applies to PROB, whereas Spin, CADP, NuSMV use either action-based or state-based temporal logics.

In the case of ALLOY and the case of reachability properties, the authors of [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] specified (manually) ad hoc traces leading to the states of the system model satisfying these properties, which is the reason why ALLOY was proven to be the most efficient among the six verification tools used in the paper. The drawback of this approach is that it necessitates good knowledge of the underlying transition system by the user. As a whole, the study in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] revealed the necessity of branching-time logics for accurately characterizing properties of ISs, and the fact that process algebraic languages are suitable for describing the behaviour and synchronization of IS entities. However, no attempt of providing a systematic translation from eb 3 to a target language accepted as input by a model checker is made so far.

In [START_REF] Mammar | Proof-based verification approaches for dynamic properties: application to the information system domain[END_REF], the verification of reachability properties "AG(ψ ⇒ EF φ)" with the aid of the B method is undertaken. The goal of this study is to construct a program p that refines a reachability property q in the sense that the set of execution paths related to program p is strictly a subset of the execution paths related to the satisfaction of reachability formula q. The construction of p follows the algorithmic refinement laws of Morgan [Mor98] that are intended to decompose q into a sequence of properties, which can be trivially refined by simple system transitions (actions). This method is not automatic, as the user is asked to specify the program that refines the given specification.

In this article, we address the problem of automatic translation (no user intervention) of eb 3 models to equivalent LNT models knowing that:

• LNT is one of the input languages accepted by the CADP verification toolbox featuring full-blown temporal property validation capabilities, and that • the model checking on LNT models allows branching-time reasoning, hence allowing the verification of liveness properties on IS specifications.

Memory Semantics

We define the memory semantics Sem M [START_REF] Vekris | Efficient Operational Semantics eb 3 for Verification of Temporal Properties[END_REF] and demonstrate by way of example why Sem M surpasses the original trace-based memory Sem T [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF] in terms of efficiency. For defining the Sem M semantics for attribute functions, attribute functions are turned into state variables (the memory M = {f 1 , . . . , f n }) carrying the effect of the system trace on their corresponding values. This avoids keeping the (ever-growing) trace leading to a finite state model. If f i (T, x 1 : T 1 , . . . , x l : T l ) is an attribute function, we construct |T 1 |×. . .×|T l | state variables denoted by f i , where |T i | (i ∈ 1..l) stands for T i 's cardinality. Then, f i denoting f i 's update upon execution of α j (v j ) is given as follows:

M = {f 1 , . . . , f n } (1) f i [ x] = w j i [ f h (T, v h ) ← f h [ v h ] | h < i ] (2) [ f h (front (T), v h ) ← f h [ v h ] | h ≥ 0 ] (x) for j > 0 (3)
where the notation . denotes the evaluation of data expressions based on the classic interpretations for Peano Arithmetic, Set Theory and Boolean Logic under the current memory M (implicit both in Figure 3 and above) carries the values of attribute variables. If action α j (v j ) can be executed, then M denotes the memory after its execution. By definition, the inert action λ has no effect on the memory M, i.e. M = M. The memory M is successively updated from f 1 , .., f n to M = {f 1 , . . . , f n } as depicted in Definition (3). Calls of the form f h (T, v h ) within w j i are replaced by already-updated f h [ v h ], since f h takes T as argument for h < i. Calls of the form f h (T, v h ) are replaced by the value of f h [ v h ], since f h takes front (T) as argument for h ≥ 0. This computation caters for the complete discharge of the trace T from w j i , while consistently

Memory State borrower[b 1 ] borrower[b 2 ] nbLoans[m 1 ] nbLoans[m 2 ] A ⊥ ⊥ ⊥ ⊥ A' ⊥ ⊥ ⊥ ⊥ B ⊥ ⊥ ⊥ ⊥ B' ⊥ ⊥ ⊥ 0 C ⊥ ⊥ 0 0 D m 1 ⊥ 1 0 Fig. 4. Evolution of Atrribute variables
updating the memory M. We denote by M 0 = {f 0 1 , . . . , f 0 n } the memory at system start, which corresponds to "T = [ ]" and "j = 0" and set f 0 i [ x] = ⊥ for every parameter vector x and every i ∈ {1, . . . , n}. The guarded expression process "C ⇒ E 0 " (M 10 ) can execute E 0 if the Boolean condition C holds under memory M, which is denoted by the side condition "

C [ f i (T, v) := f i [ v ] ] " such that "M = {f 1 , . . . , f n }".
Since C may contain calls to attribute functions of the form f (T, v), the evaluation of C necessitates their replacement by their corresponding attribute variables f[ v ]. The trace T is discharged from C and, hence, the evaluation of the guard C does not depend on T. Note that the evaluation of C and the execution of the first action ρ in E 0 are simultaneous, i.e., no action is allowed in concurrent processes in the meantime. We call this property the guard-action atomicity. This property is essential for consistency as, by side effects, the occurrence of actions in concurrent processes could implicitly change the value of C before the guarded action has been executed.

Execution. We demonstrate how the memory semantics Sem M works for the simplified library management system, whose specification (processes and attribute functions) in eb 3 is given in Figure 1. As an example, we set m = p = NbLoans = 2, i.e. we consider two books b 1 and b 2 , and two members m 1 and m 2 . The memory has four cells:

M = (borrower [b 1 ], borrower [b 2 ], nbLoans[m 1 ], nbLoans[m 2 ]).
The first two cells keep the two values of the attribute function borrower (T, •) for a given trace T, and the last two keep the values of nbLoans (T, •). After every step, the new value of each cell can be calculated from the previous memory and the action that has just been executed. The memory is initially set to (⊥, ⊥, ⊥, ⊥). After the trace "Acquire (b 1 ).Acquire (b 2 ).Register (m 1 ).Register (m 2 )" the memory contains (⊥, ⊥, 0, 0). If the action "Lend (b 1 , m 1 )" is then executed, the new memory is (m 1 , ⊥, 1, 0). For instance, the new value m 1 for borrower [b 1 ] is obtained from the Rule "Lend (bId , mId ) : mId " in the definition of the attribute function borrower (see Fig. 1), and the new value 1 for nbLoans[m 1 ] by the Rule "Lend (bId , mId ) : nbLoans (front (T), mId ) + 1" of the attribute function nbLoans, where the value of nbLoans (front (T), m 1 ) corresponds to the value of nbLoans[m 1 ] in the previous memory state (value 0). The evolution of attribute variables is depicted in Figure 4, where (A') is the state after the execution of Acquire (b 1 ), (B) is the state the moment succeeding the execution of Acquire (b 2 ), (B') is the state the moment succeeding the execution of Register (m 1 ), (C) is the state the moment succeeding the execution of Register (m 2 ) and (D) is the state the moment succeeding the execution of Lend (b 1 , m 1 ).

Figure 5 depicts the evolution of process expression main describing the library management system in states (A), (B), (C), and (D). Transition (C)→(D) entails the evaluation of the following guard:

(borrower (T, b 1 ) = ⊥) ∧ (nbLoans (T, m 1 ) < 2) (4)
where T corresponds to the system trace at state (C), i.e. T = T C . Condition (4) illustrates the conditions under which member m 1 can lend book b 1 (notably if the book is available and the number of loans carried out by m 1 is inferior to two). We concentrate on the evaluation of the attribute function call "borrower (T, b 1 )" w.r.t. Sem M and then we compare it with the evaluation of "borrower (T, b 1 )" w.r.t. the where "borrower B [b 1 ]" is the (stocked) attribute variable at state (B'). Following the attribute function definition of borrower in Figure 1, the evaluation of "borrower (T C , b 1 )" w.r.t. Sem T (the standard ML-like evaluation of recursive functions denoted as . T to mark the difference with the . evaluation) triggers the complete traversal of the whole trace as demonstrated below:

main (A) Acquire (b 2 ). Acquire (b 1 ) -------------------→ borrower (T B , b 1 ) = ⊥ → Discard (b 1 ). book (b 1 ) * ||| borrower (T B , b 2 ) = ⊥ → Discard (b 2 ). book (b 2 ) * ||| ( ||| mId : MID : member (mId) * ) (B) Register (m 2 ). Register (m 1 ) ----------------------→ borrower (T C , b 1 ) = ⊥ → Discard (b 1 ). book (b 1 ) * ||| borrower (T C , b 2 ) = ⊥ → Discard (b 2 ). book (b 2 ) * ||| ( ||| bId : BID : loan (m 1 , bId ) * ). Unregister (m 1 ). member (m 1 ) * ||| ( ||| bId : BID : loan (m 2 , bId ) * ). Unregister (m 1 ). member (m 2 ) * (C) Lend (b 1 , m 1 ) -----------→ borrower (T D , b 1 ) = ⊥ → Discard (b 1 ). book (b 1 ) * ||| borrower (T D , b 2 ) = ⊥ → Discard (b 2 ). book (b 2 ) * ||| (Return(b 1 ). loan(m 1 , b 1 ) * ||| loan(m 1 , b 2 ) * ). Unregister (m 1 ). member (m 1 ) * ||| ( ||| bId : BID : loan (m 2 , bId ) * ). Unregister (m 1 ). member (m 2 ) * (D)
borrower (T C , b 1 ) T = borrower (front (T C ), b 1 ) T = borrower (T B , b 1 ) T = borrower (front (T B ), b 1 T = borrower (T B , b 1 ) T = borrower (front (T B ), b 1 ) T = borrower (T A , b 1 ) T = borrower (front (T A ), b 1 ) T = borrower (T A , b 1 ) T = ⊥ T = ⊥
from which follows directly that Sem M is computationally more efficient than Sem T .

B ::= stop null G (O 1 , . . . , O n ) where E B 1 ; B 2 if E then B 1 else B 2 end if var x : T in B end var x := E loop L in B end loop break L select B 1 [] . . . [] B n end select par G 1 , . . . , G m in B 1 || . . . || B n end par P [G 1 , . . . , G n ] (E 1 , . . . , E n ) O ::= !E ?x

The Language LNT

LNT aims at providing the best features of imperative and functional programming languages and valuepassing process algebras. It has a user friendly syntax and formal operational semantics defined in terms of labeled transition systems (LTSs). LNT is supported by the LNT.OPEN tool of CADP, which allows the on-the-fly exploration of the LTS corresponding to a LNT specification.

We present the fragment of LNT that serves as the target of our translation. LNT terms B also called as behaviours are built from actions, choice (select), conditional (if ), sequential composition (;), breakable loop (loop and break) and parallel composition (par). Communication is carried out by rendezvous on gates, written G, G 1 , . . . , G m , and may be guarded using Boolean conditions on the received values (where clause). LNT allows multiway rendezvous with bidirectional (send/receive) value exchange on the same gate occurrence, each offer O being either a send offer (!) or a receive offer (?), independently of the other offers. Expressions E are built from variables, type constructors, function applications and constants. Labels L identify loops, which can be escaped using "break L" from inside the loop body. Processes are parameterized by gates and data variables. LNT syntax and semantics are formally defined in SOS style in [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator -Version 5[END_REF].

MCL

MCL is an extension of the alternation-free modal µ-calculus [EL + 86] with action predicates enabling value extraction, modalities containing extended regular expressions on transition sequences, quantified variables and parameterized fixed point operators, programming language constructs, and fairness operators encoding generalized Büchi automata. These features make possible a concise and intuitive description of safety, liveness, and fairness properties involving data, without sacrificing the efficiency of on-the-fly model checking, which has a linear-time complexity for the dataless MCL formulas [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF].

In particular, MCL consists of data expressions e, action formulas α and state formulas φ. Let a set of data variables X and a set of function identifiers F with standard interpretation. Data expressions e are defined as follows:

e ::= x | f (e 1 , . . . , e n ),
where x ∈ X and f ∈ F denoting typed function identifiers.

Action formulas α consist of:

• action patterns of the form {c !e 1 . . . !e n } such that, if action {c v 1 . . . v n } occurs, v k matches expression e k for k ∈ {1, . . . , n}, • action patterns of the form {c ?x 1 : T 1 . . . ?x n : T n }2 such that, if action {c v 1 . . . v n } occurs, v k is assigned to variable x k for k ∈ {1, . . . , n}, and • usual Boolean operators.

To sum up, the abstract syntax of action formulas α is given by the following grammar: Note also that fixed point operations fall within the scope of an even number of negations (MCL formulas µ(. . .)Y.φ and ν(. . .)Y.φ are syntactically monotonic) [START_REF] Kozen | Results on the Propositional µ-calculus[END_REF]. For the efficiency of model checking, mutual recursion between minimal and maximal fixed point operators is not allowed [EL + 86].

α ::= {c !e 1 . . . !e n } | {c ?x 1 : T 1 . . . ?x n : T n } | ¬α | α 1 ∧ α 2 | α * Let propositional variables Y ∈ Y that denote functions F : T 1 × . . . × T n → 2 S ∈ F,
We assign values to propositional variables x ∈ X appearing in expressions e and action formulas α that are denoted as δ : X → T 1 ∪ . . . ∪ T n . Moreover, we assign functions to all free propositional variables Y appearing in MCL state formulas that are denoted as ρ : Y → F. Notations "µY.φ" and "νY.φ" denote the corresponding fixed points of monotonic functions over Y → 2 S .

Other useful operators like if and case can also be used to construct MCL formulas. Their definition is found in [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF].

Action patterns are enriched with additional features such as the wilcard clause any that matches any value and the "where V " clause denoting that the pattern-matching takes place on condition that condition V evaluates to true. Remark that parameters ?x : T can appear syntactically in V .

The abstract syntax of MCL state formulas is given by the following grammar:

φ ::= e | ¬φ | φ 1 ∨ φ 2 | α φ | µY. φ | exists x 1 : T 1 , . . . , x n : T n . φ | Y (e 1 , . . . , e n ) | let x 1 : T 1 := e 1 , . . . , x n : T n := e n in φ end let | if φ 1 then φ 1 elsif φ 2 then φ 2 else φ 3 end if | case e is p 1 → φ 1 | . . . | p n → φ n end case
The necessity modality is the dual of possibility modality "[ α ] φ = ¬ α ¬φ". The maximal fixed point operator is the dual of the minimal fixed point operator: "ν(. . .)Y.φ = ¬µ(. . .)Y.¬φ[Y /¬Y ]", where [Y /¬Y ] denotes the syntactic substitution of Y by ¬Y . Note that " α * φ" is syntactic sugar for "µY (φ ∨ β Y )".

MCL's expressiveness is not limited to safety and liveness properties. Deadlock freedom is formalized as "[ true * ] true true". The fair reachability [START_REF] Queille | Fairness and Related Properties in Transition Systems-A Temporal Logic to Deal with Fairness[END_REF] of an action a is formalized as "[ (¬a) * ] (¬a) * .a true". For more complex fairness properties, we use the infinite looping operator ∆β of P DL-∆ [START_REF] Streett | Propositional Dynamic Logic of Looping and Converse[END_REF], denoted as β@ in MCL, which states the existence of an infinite (unfair) sequence made by concatenating subsequences satisfying β.

Let's consider the following MCL example: 9. Translation of EB 3 to LNT 9.1. Translation of attribute functions.

Ordering attribute functions as described in Section 6 allows the memory to be updated consistently, from f 1 to f n in turn. At every instant, already-updated values correspond to calls of the form f h (T, . . .) (the value of f h on the current trace), whereas calls of the form f h (front (T), . . .) are replaced by accesses to a copy g of the memory f , which was made before starting the update. This encoding thus enables the trace parameter to be discharged from function calls, ensuring that while updating f i , accesses to f h with h < i necessarily correspond to calls with parameter T.

The process M is defined in Figure 7. It runs an infinite loop, which "listens" to all possible actions α j of the system. At this point, we recall the existence of unique attribute function definition f i (T : T , y 1 : T 1 , . . . , y s : T s ) : T (see Figure 2 for details). Each attribute variable f i is an array with s dimensions, where s is the common arity for attribute functions f i minus 1, because the trace parameter is now discharged. Each dimension of array f i , thus, corresponds to one formal parameter in y i , so that:

f i [ord (v 1 )] . . . [ord (v s )]
process M [α 1 , . . . , α q , λ : any] is var f , g : T , y : T at , x : T ac in upd 0 1 ; . . . ; upd 0 n ; loop

g := f select α 1 (?x, !f ); upd 1 1 ; . . . ; upd 1 n [] . . . [] α q (?x, !f ); upd q 1 ; . . . ; upd q n [] λ (!f )
end select end loop end var end process Fig. 7. LNT code for the memory process implementing the attribute functions

upd j i . = enum (y, f i [ord (y)] := mod (w j i )) enum ([ ], B) . = B enum (y k :: z, B) . = y k := first k ; loop L k in enum (z, B) if y k = last k then y k := next k (y k ) else break L k end if end loop mod (w 0 i ) . = w 0 i f h (T, y) := f h [ord (y)] ∀h < n f h (front (T), y) := ⊥ ∀h ∈ {1, . . . , n} mod (w j i ) = w j i f h (T, y) := f h [ord (y)] ∀h < n f h (front (T), y) := g h [ord (y)]
∀h ∈ {1, . . . , n} , if j = 0 Fig. 8. LNT code for expression upd j i of Figure 7 encodes the current value of:

f i (T, v 1 , . . . , v s ),
where ord (v k ) is a predefined LNT function that denotes the ordinate of the value that corresponds to variable v k , i.e., a unique number between 1 and the cardinal number |D k | of domain D k that stocks elements of type T k . Expression upd j i for i ∈ {1, . . . , q} and j ∈ {1, . . . , q} of Figure 7 is used to implement the effect of action α j (x) on attribute variables f i . Its definition is given in Figure 8. In particular, upd j i is defined by way of auxiliary function enum. For vector z = (z 1 , . . . , z o ), y k :: z is equivalent notation for (y k , z 1 , . . . , z o ) and [ ] stands for the empty vector. For each type T k , we assume the existence of functions first k that returns the first element of type T , last k that returns the last element of type T k , and next k (x) that returns the successor of x on condition that the type of variable x is T k (following the total order induced by ord). For example, let

T k = {m 1 , m 2 , m 3 }. Then, it is first k = m 1 , next k (m 1 ) = m 2 , next k (m 2 ) = m 3 and last k = m 3 .
According to the definition of "enum (y x :: z, B)" of Figure 8, the loop structure is employed to assign to y k the current element of domain D k (the first element of D k is assigned at first) and a recursive call to enum (z, B) is taken. If y k has not been assigned the last value of D k , which is expressed by condition y k = last k , the next value of D k is assigned to y k via y k := next k (y k ) and enum (z, B) is called once again. Otherwise, the program breaks from the loop structure. This approach guarantees that, when computing the effect of actions on attribute variables via assignment B, all attribute variables are taken into consideration.

Note also that enum depends on function mod (E) which transforms an expression E by syntactically replacing function calls by array accesses as described previously. Namely according to the definition of mod (w j i ) of Figure 8, expressions of the form "f h (T, y)" are replaced by f h [ord (y)] and expressions of the form "f h (front (T), y)" are replaced by g h [ord (y)] for all h < n. Recall at this point that the initial values of attribute variables g are by convection equal to ⊥, which entails the replacement of attribute function calls of the form "f h (front (T), y)" in eb 3 type (1) value expressions w 0 i by ⊥ for all h ∈ {1, . . . , n}. Notation y : T at is an abbreviation for "y 1 : T 1 , . . . , y s : T s " and T denotes the vector (T, . . . , T ) of size n that is equal to the number of attribute function names in the system.

Expression next k (x) is implemented as LNT expression "val (ord (x)+1)". Note that in LNT assignment "x := val (i)" identifier val stands for the predefined LNT function that returns the i-th element of given ordered set denoting the domain of x's type. Such functions are available in LNT for all finite types.

Similarly, assuming common parameter vector x . = (x 1 , . . . , x p ) for all action labels α j for all j ∈ {1, . . . , q} or, equivalently, action name definitions of the form α j (x 1 : T 1 , . . . , x p : T p ) for all j ∈ {1, . . . , q}, we define "x : T ac " that is equivalent to "x 1 : T 1 , . . . , x p : T p ", where types T 1 , . . . , T p are not to be confused with the types corresponding to the attribute parameters y k ∈ y for k ∈ {1, . . . , s} as seen earlier. Then, upon synchronization on action α j (?x, !f ) with the LNT process corresponding to eb 3 's main process (see translation of processes below), the values of all attribute variables f i for i ∈ {1, . . . , n} are updated using function upd j i . As an example, we demonstrate how the definition of Figure 7 regarding the memory process, applies to the eb 3 specification of the library management system for one book and two members. Member and book IDs are defined in the LNT program as follows:

type MID is m 1 , m 2 , m ⊥ with "eq", "ne", "ord", "val" end type type BID is b 1 , b ⊥ with "eq", "ne", "ord", "val" end type Identifier eq (ne) denotes the equality (inequality) operator among member IDs or book IDs. The bottom value for member IDs is denoted as m ⊥ and the bottom value for book IDs is denoted as b ⊥ . In the following, the type referring to the number of books possessed by each member of the library is denoted as an array NB and the type referring to the current borrower of each book is denoted as an array BOR. Hence, NB and BOR are defined in LNT as follows:

type NB is array[0..2] of NAT end type type BOR is array[0..1] of MID end type Now, we need to explain how the execution of communication label LEND modifies attribute variable vectors "borrower : BOR" and "nbLoans : NB ". First, we remark that, according to the eb 3 specification of the library management system, the execution of eb 3 action "Lend (bId, mId)" modifies attribute variables borrower[bId] and nbLoans[mId]. Hence, following the definition of Figure 7, we need an auxilliary variable bId to go through all possible values of book IDs, i.e. the elements that inhabit BID's domain, in order to simulate the modification of borrower[bId ] in case that book bId is lent to member mId . In each iteration of the loop construct, it is checked if bId is equal to the current value of bId , in which case borrower[bId ] is set to the current borrower, i.e. mId . Then, it is checked if bId is equal to the last element of BID's domain, i.e. b 1 , in which case the program control breaks from the loop construct. Otherwise, bId is assigned the next element in the ordered set of BID's domain, i.e. "bId := val (ord (bId ) + 1)", and the execution of the loop construct is repeated.

Similarly, we need an auxiliary variable mId to go through all possible values of member IDs, i.e. the elements that inhabit MID's domain, in order to simulate the modification of nbLoans[bId ] in case that book bId is lent to member mId . In each iteration of the loop construct, it is checked if mId coincides with the current value of mId , in which case nbLoans[mId ] is increased by one. Then, it is checked if mId is equal to the last element of MID's domain, i.e. m 2 , in which case the program control breaks from the loop construct. Otherwise, mId is assigned the next element in the ordered set of MID's domain, i.e. "mId := val (ord (mId ) + 1)", and the execution of the loop construct is repeated. bId := b 1 ; loop L 1 in if (bId eq bId ) then borrower [ord (bId )] := m ⊥ end if ; if (bId eq b 1 ) then break L 1 else bId := val (ord (bId ) + 1) end if end loop; end select end loop end var end process Note that LNT statement "borrower := BOR(m ⊥ )" is equivalent to "borrower[ord (b 1 )] := m ⊥ ". Similarly, "nbLoans := N B(0)" is equivalent to "nbLoans[ord (m 1 )] := 0; nbLoans[ord (m 2 )] := 0". Note that the initial number of loans is set to 0, whereas according to Figure 1 it should be set to ⊥. The reason is that it is impossible to define Nat ⊥ of Figure 1 without recourse to complex LNT data structures. Hence, the symbol ⊥ of Figure 1 is basically matched to the symbol 0 in the above LNT program, the symbol 0 of Figure 1 is matched to 1 in the above LNT program etc.

Optimizations.

Notice that the inert action λ has been removed from the previous LNT specification, since λ is does not appear in the program script and, as a result, it is supposed not to affect the control flow.

Similarly, attribute variable vector f = (nbLoans, borrower) is removed from the parameter vector of communication labels that synchronize with expressions of the form "α (v, ?f ) where mod (C)" present in other LNT processes (see Figure 9), for which the corresponding guard mod (C) makes no use of attribute variable vector f . In particular, this optimization applies to communication labels Acquire, Register , Unregister and Return. The static analysis of LNT specifications cater for an efficient discovery of all guards, as well as their related communication labels.

The only coordinates of attribute variable vector f = (nbLoans, borrower) passed as parameters to the communication labels "α (v, ?f ) where mod (C)" are exactly those appearing in mod (C). Notice, for example, that vector nbLoans is not a subset of the parameter vector passed to communication label Discard , since the static analysis of the LNT specification reveals that no corresponding guard to Discard makes use of nbLoans.

The code referring to attribute variables that remain unchanged during a communication is omitted. This is the case for communication labels Acquire, Discard , Register and Unregister in the previous LNT code.

It turns out that the code simulating the effect of eb 3 action "Lend (bId , mId )" on attribute variables borrower[bId ] and nbLoans[mId ] can be optimized based on the simple observation that attribute variables borrower[bId ] for bId = bId and nbLoans[mId ] for mId = mId remain unaffected. Hence, the corresponding part of process M regarding eb 3 action "Lend (bId , mId )" can be modified as follows: A similar approach applies to communication label Ret. The optimized LNT specification of the library management system is given in the appendix. Note that this optimization technique is applicable whenever the in offers of the communication label in question, i.e. the parameters marked with ?, suffice to determine

t (λ, C) = λ (?f ) where mod (C) (1) t (α (v), C) = α (v, ?f ) where mod (C) (2) t (E 1 .E 2 , C) = t (E 1 , C); t (E 2 , true) (3) t (C ⇒ E 0 , C) = t (E 0 , C andthen C ) (4) t (E 1 | E 2 , C) = select t (E 1 , C) [] t (E 2 , C) end select (5) t (|x : V : E 0 , C) = var x := any V ; t (E 0 , C) end var (6) t (E 0 * , true) = loop L E0 in select λ (?f ); break L E0 [] t (E 0 , true) end select end loop (7) t (E 1 |[∆]| E 2 , true) = par ∆ in t (E 1 , true) || t (E 2 , true) end par (8) t (|[∆]|x : V : E 0 , true) = par ∆ in E 0 [x := v 1 ] || . . . || E 0 [x := v n ] end par where V = {v 1 , . . . , v n } (9) t (P (v), true) = P [α 1 , . . . , α q , λ] (v) (10)
In all other cases:

t (E 0 , C) =                  if mod (C) then t (E 0 , true) else stop end if if C does not use attribute functions par α 1 , . . . , α q , λ in t (E 0 , true) || pr C [α 1 , . . . , α q , λ] (vars (C)) end par otherwise (11)
Fig. 9. Translation from eb 3 process to LNT process which attribute variables are modified. Based on our experience with eb 3 specifications, this optimization technique is often applicable on the corresponding LNT specifications. It is also incorporated on our tool eb 3 2lnt.

Translation of processes.

We define a translation function t from an eb 3 process expression to an LNT process. Most eb 3 constructs are process algebra constructs with a direct correspondence in LNT. The main difficulty arises in the translation of guarded process expressions of the form "C ⇒ E 0 " in a way that guarantees the guard-action atomicity. This led us to consider a second parameter for the translation function t, namely the condition C, whose evaluation is delayed until the first action occurring in the process expression E 0 . The definition of t (E, C) is given in Figure 9. An eb 3 specification E 0 will then be translated into:

par α 1 , . . . , α q , λ in t (E 0 , true) || M [α 1 , . . . , α q , λ] end par
and every process definition of the form "P (x) = E" will be translated into the process:

process P [α 1 , . . . , α q , λ : any] (x : type (x)) is t (E, true) end process,

where {α 1 , . . . , α q } = Lab. The Rules of Figure 9 can be commented as follows:

• Rule (1) translates the λ action. Note that λ cannot be translated to the empty LNT statement null, because execution of λ may depend on a guard C, whose evaluation requires the memory to be read, so as to get attribute variable values. This is done by the LNT communication action λ (?f ). The guard C is evaluated after replacing calls to attribute functions (all of which have the form f i (T, v i )) by the appropriate attribute variables, using function mod defined in Figure 7. Rule (2) is similar but handles visible actions.

• Rule (3) translates eb3 sequential composition into LNT sequential composition, passing the evaluation of C to the first process expression.

• Rule (4) makes a conjunction between the guard of the current process expression with the guard already accumulated from the context.

• Rules (5) and ( 6) translate the choice and quantified choice operators of eb 3 into their direct LNT counterpart.

• Rule (7) translates the Kleene closure into a combination of LNT loop and select, following the identity

E 0 * = λ | E 0 .E 0 * .
• Rule (8) translates eb 3 parallel composition into LNT parallel composition.

• Rule (9) translates eb 3 quantified parallel composition into LNT parallel composition by expanding the type V of the quantification variable, since LNT does not have a quantified parallel composition operator.

• Rule (10) translates an eb 3 process call into the corresponding LNT process call, which requires gates to be passed as parameters.

• Rules (7) to (10) only apply when the guard C is trivially true. In the other cases, we must apply Rule (11), which generates code implementing the guard. If C does not use attribute functions, i.e., does not depend on the trace, then it can be evaluated immediately without communicating with the memory process (first case). Otherwise, the guard evaluation must be delayed until the first action of the process expression E 0 . When E 0 is either a Kleene closure, a parallel composition, or a process call, identifying its first action syntactically is not obvious. One solution would consist in expanding E 0 into a choice in which every branch has a fixed initial action 3 , to which the guard would be added. We preferred an alternative solution that avoids the potential combinatorial explosion of code due to static expansion. A process pr C (defined in Figure 10) is placed in parallel to t (E 0 , true) and both processes synchronize on all actions. Process pr C imposes on t (E 0 , true) the constraint that the first executed action must satisfy the condition C (then branch). For subsequent actions, the condition is relaxed (else branch).

process pr C [α 1 , . . . , α q , λ : any] (vars (C) : type (vars (C))) is Note that the equivant LNT process of eb 3 process main is placed in parallel to memory process M . Moreover, the simulation of eb 3 quantified parallel synchronization operator (that has no equivalent operator in LNT) is applied to eb 3 expressions "|||bId : BID : book (bId ) * " and "|||mId : MID : member (mId ) * " and the eb 3 Kleene Closure operator is simulated as described in Figure 9. The body of LNT processes book and member is defined as below: where (borrower [ord (bId)] eq m ⊥ ) and (nbLoans [ord (mId)] eq 1) ; Return (bId) end var end process

var start : bool, x : T ac , f : T in start := true; loop L in select if start then start := false; select α 1 (?x, ?f ) where mod (C) [] . . . [] α q (?x, ?f ) where mod (C) [] λ (?f ) where mod (C) end select else select α 1 (?x, ?f ) [] . . . [] α q (?x, ?f ) [] λ (?f ) end select end if [] break L end select
process
The following example illustrates and justifies the use of process pr C as a means to solve the guard-action atomicity problem. Consider the eb 3 system:

C ⇒ Lend (b 1 , m 1 ) ||| Return (b 2 ),
where C denotes the Boolean condition: borrower (T, b 1 ) = ⊥ ∧ nbLoans (T, m 1 ) < NbLoans and Lab = {Lend , Return}. The LNT code corresponding to this system is the following:

par Lend , Return, λ in par Lend , Return, λ in par Lend (b 1 , m 1 , ?f ) || Return (b 2 , ?f ) end par || pr C [Lend , Return, λ] (b 1 , m 1 ) end par || M [Lend , Return, λ] end par
The first action executed by this system may be either Lend or Return. We consider the case where R15. A member cannot borrow more than the loan limit defined at the system level for all users.

We expressed all the above requirements using the property specification language MCL [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF]. We show below the MCL formulation of two requirements from the list above, which denote typical safety and liveness properties. Requirement R2 is expressed in MCL as follows:

[ true * .{ACQUIRE ?B : string}.(not {DISCARD !B}) * .{ACQUIRE !B} ] false
This formula uses the standard safety pattern "[β] false", which forbids the existence of transition sequences matching the regular formula β. Here the undesirable sequences are those containing two Acquire operations for the same book B without a Discard operation for B in the meantime. The regular formula true * matches a subsequence of (zero or more) transitions labeled by arbitrary actions. Note the use of the construct "?B : string", which matches any string and extracts its value in the variable B used later in the formula. Therefore, the above formula captures all occurrences of books carried by Acquire operations in the model. Requirement R12 is formulated in MCL as follows:

[ true * .{RESERVE ?M : string ?B : string}.

(not ({TAKE !M !B} or {TRANSFER !M !B})) * ] (not ({TAKE !M !B} or {TRANSFER !M !B})) * . {CANCEL !M !B} true
This formula denotes a liveness property of the form "[β 1 ] β 2 true", which states that every transition sequence matching the regular formula β 1 (in this case, book B has been reserved by member M and subsequently neither taken nor transferred) ends in a state from which there exists a transition sequence matching the regular formula β 2 (in this case, the reservation can be cancelled before being taken or transferred). Requirement R7 can be formulated as follows:

[ true * . {RESERVE ?M : string ?B : string} . (not

({TAKE !M !B} or {CANCEL !M !B})) * . {RESERVE !M !B} ] false
All requirements formulated in MCL can be found in Appendix C. Using eb 3 2lnt, we translated the eb 3 specification of the library management system to LNT. The resulting specification was checked against all the 15 requirements, formulated in MCL, using the EVAL-UATOR 4.0 model checker of CADP. The experiments were performed on an Intel(R) Core(TM) i7 CPU 880 at 3.07GHz. Table 1 shows the results for several configurations of the IS, obtained by instantiating the number of books (m) and members (p) in the IS. All requirements were shown to be valid on the IS specification. The second and third line of the table indicate the number of states and transitions of the LTS corresponding to the LNT specification. The fourth line gives the time needed to generate the LTS and the other lines give the verification time for each requirement.

Note that the number of states generated increases with the size of m and p as EVALUATOR 4.0 applies explicit techniques for state space generation. According to Table 1, verifying the library management system becomes intractable for more than four members and four books. This misbehaviour is mainly attributed to the presence of parallel compositions between members and books as well as the loose synchronisation between these components leading to exponential growth of the state space.

Comparison with [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] We recall that CADP was used in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] for the verification of a version of the library management system with similar functionalities. According to the same paper, the time needed to generate the corresponding LTS for NbLoans = 1, was 970.2 sec approximately, the average time needed to verify the system requirements was 74.63 sec and no information is provided for the size of the LTS, which means that no reliable comparison of the two works is possible. Note also that the LNT specification, to whom the results of Table 1 are related, was automatically generated by eb 3 2lnt, whereas the results of [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] correspond to a manual LNT specification of the library management system.

Regarding the other verification tools employed in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF], only verification with ALLOY outperforms our verification scheme with CADP, which is normal as in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] in the case of reachability properties for example the traces needed to satisfy them are specified by the user, which implies that automatic verification with ALLOY as done in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] is not automatic and therefore not adequate.

Conclusion

We proposed an approach for equipping the eb 3 method with formal verification capabilities by reusing already available model checking technology. Our approach relies upon a new translation from eb 3 to LNT, which provides a direct connection to all the state-of-the-art verification features of the CADP toolbox. The translation, based on alternative memory semantics of eb 3 [VD13] instead of the original trace semantics [START_REF] Frappier | eb 3 : an entity-based black-box specification method for information systems[END_REF], was automated by the eb 3 2lnt translator and validated on several examples of typical ISs. So far, we experimented only the model checking of MCL data-based temporal properties on eb 3 specifications. However, CADP also provides extensive support for equivalence checking and compositional LTS construction, which can be of interest to IS designers. We also provided a formal proof of the translation from eb 3 to LNT that can be found in [START_REF] Vekris | Verification of eb 3 specifications with the aid of model-checking techniques[END_REF], which could serve as reference for translating eb 3 to other process algebras as well.

eb 3 2lnt offers insight to interested readers on:

• how to code global state as a process running parallel to the principal system specification, and • how to solve the atomicity problem (imposing the simultaneous evaluation of C with the execution of the first action of E in expressions of the form C ⇒ E) by a way of another process running to the principal system specification.

On the other hand, the main limitation of the proposed translation is that model-checking becomes intractable for specifications describing multiple concurrent processes as is the case for the library specification for more than four members and four books. This inconvenience is attributed mainly to:

• the frequent use of parallel composition operators in eb 3 specifications that lead to the exponential growth of execution traces, and • the fact that CADP employs explicit techniques instead of symbolic techniques for state space generation.

Another drawback of the proposed translation arises at the stage of property verification. Properties should be expressed in MCL, which implies that eb 3 users should be familiar with MCL's syntax. However, one should note that the whole scale of MCL formulas can be used for the verification of eb 3 specifications, despite the fact that the emphasis of this paper is given on safety and liveness properties.

As future work, we plan to study abstraction techniques for verifying properties regardless of the number of entity instances that participate in the IS, following the approaches for parameterized model checking [ABJ + 99]. This study will establish the fact that verifying systems with many components (members and books in our case) is equivalent to verifying systems with the same structure as before, but less components. In particular, we will observe how the insertion of new functionalities into an IS affects this issue, and we will formalize this in the context of eb 3 specifications.

B. LNT Code for the Extended Library Management System

We give the LNT code for the extended Library Management System (NbLoans = 1). This code is generated by eb 3 2lnt except the functions "add reservation","cancel reservation", "last reservation", "nil reservation" and "is reserved ", which are coded by hand, since our compiler does not support user-defined eb 3 types and (non-attribute) functions. We also define type "RESERV " to simplify the coding. By convention, for every type T we have ord (⊥) = 0, ord (first T ) = 1, etc. end macro R 1 ("B1") and R 1 ("B2") and R 1 ("B3") This is a classical liveness property. The second conjunct of "R 1 (B)" expresses the eventuality that a book be withdrawn from the library before it is reacquired. ({LEND !M ?any : string} or {TAKE !M ?any : string}) ] false ) end macro R 4 ("M1") and R 4 ("M2") and R 4 ("M3")

The first conjunct or "R 4 (M )" expresses the fact that a member cannot borrow a book if (s)he has not registered to the library. The second conjunct expresses that if a member relinquishes his/her membership, (s)he may not lend a book neither via the regular loan action LEND nor the reservation action RESERVE.

Requirement R5 "A book can be reserved only if it has been borrowed or already reserved by some member " {RESERVE ?any : string !B} ] false ) end macro R 5 ("B1") and R 5 ("B2") and R 5 ("B3")

The first conjunct expresses the obligation for a book not to be lent in order to be added to the reservation list. The second conjunct complements the first in the sense that at least one loan cycle is completed in the beginning of the transition sequence via "{ RETURN !B }" thus making the book available for loan again. The third conjunct denies any reservation history for the book in question. All possible loan operations should be excluded as well.

Requirement R6 "A book cannot be reserved by the member who is borrowing it" [ true * .{LEND ?M : string ?B : string} .

(not ({RETURN !B} or {TRANSFER ?M 2 : string !B})) * . {RESERVE !M !B} ] false

The difficulty here lies in the fact that the borrower may transfer the book to another member. For this reason, the following formula is false. In this case (as well as for the subsequent requirements R9, R11, R13, R14, and R15), we only check the property for a specific book (B1) and members (M1, M2). So doing, we exploit the symmetry of the specification (all books and members have similar behaviour), which is crucial to avoid the exponential state space explosion.

Requirement R9 "A member cannot renew a loan or give the book to another member if the book is reserved " This property corresponds to the pattern "α 1 does not occur between α 2 and α 3 ", which is expressed by the following scheme, easily recognizable in this formula: [ true * . α 2 . (not α 3 ) * . α 1 . (not α 3 ) * . α 3 ] false Requirement R13 "A member can relinquish library membership only when all his loans have been returned and all his reservations have either been used or cancelled " This property is dependent on the maximum number NbLoans of books a member can have at any time in his/her possession. In the above, NbLoans was set to two.

BID = {b 1

 1 , . . . , b m }, MID = {m 1 , . . . , m p } book (bId : BID) = Acquire (bId ) . (borrower (T, bId ) = ⊥) ⇒ Discard (bId ) loan (mId : MID, bId : BID) = (borrower (T, bId ) = ⊥) ∧ (nbLoans (T, mId ) < NbLoans) ⇒ Lend (bId , mId ) . Return (bId ) member (mId : MID) = Register (mId ) . (|||bId : BID : loan (mId , bId ) * ) . Unregister (mId ) main = (|||bId : BID : book (bId ) * ) ||| (|||mId : MID : member (mId ) * ) nbLoans (T : T , mId : MID) : Nat ⊥ = borrower (T : T , bId : BID) : MID ⊥ = match last (T) with match last (T) with ⊥ : ⊥ ⊥ : ⊥ | Lend (bId , mId ) : | Lend (bId , mId ) : mId nbLoans (front (T), mId ) + 1 | Return (bId ) : ⊥ | Register (mId ) : 0 | : borrower (front (T), bId ) | Unregister (mId ) : ⊥ end match | Return (bId ) : if mId = borrower (T, bId ) then nbLoans (front (T), mId ) -1 else nbLoans (front (T), mId ) end if | : nbLoans (front (T), mId ) end match

Fig. 1 .

 1 Fig.1. eb 3 specification of a library management systemEB 3 ::= A 1 ; . . . ; A n ; S 1 ; . . . ; S m A ::= f (T : T , y : T ) : T = match last (T) with ⊥ : v 0 | α 1 (x 1 ) : v 1 | . . . | α q (x q ) : v q [| : v q+1 ] S ::= P (x) = E E ::= λ α (v) E 1 .E 2 E 1 | E 2 E 0 * E 1 |[∆]| E 2 |x : V : E 0 |[∆]|x : V : E 0 C ⇒ E P (v)

Fig. 2 .

 2 Fig. 2. eb 3 syntax

Fig. 5 .

 5 Fig. 5. Sample execution

Fig. 6 .

 6 Fig. 6. LNT syntax (limited to the fragment used in this paper)

  where T 1 , . . . , T n are domains and S is the state space. State formulas consist of data expressions, propositional variables Y ∈ Y, boolean operators, quantifiers and fixed point operators.

[

  true * . {RESERVE ?M : string ?B : string} . (not ({TAKE !M !B})) * . {RESERVE !M !B} ] falseThe expression inside [ . ] describes the set of execution paths starting with a bounded number of actions (denoted as true * ) followed by a RESERVE action of book B by member M , a bounded number of actions that are not TAKE actions of B by M and a RESERVE action of book B by member M . Finally, false notation is used to denote that the paths described inside [ . ] are not possible (safety property).

[]

  Lend (?bId , ?mId , !nbLoans, !borrower); borrower [ord (bId )] := mId ; nbLoans [ord (mId )] := nbLoans [ord (mId )] + 1

  Requirement R3 "An acquired book can be discarded only if it is neither borrowed nor reserved " [ true * . {?G : string ?any : string ?B : string where (G = "LEND") or (G = "TAKE")} .(not {RETURN !B}) * . {DISCARD !B} ] false and [ true * .{RESERVE ?any : string ?B : string} . (not ({CANCEL ?any : string !B} or {RETURN !B})) * . {DISCARD !B} ] false Requirement R4 "A person must be a member of the library in order to borrow a book " macro R 4 (M ) = ( [ (not {JOIN !M }) * . ({LEND !M ?any : string} or {TAKE !M ?any : string}) ] false and [ true * .{LEAVE !M } . (not {JOIN !M }) * .

macro R 5

 5 (B) = ( [ (not ({LEND ?any : string !B} or {TAKE ?any : string !B})) * . {RESERVE ?any : string !B} ] false and [ true * . {RETURN !B} . (not ({LEND ?any : string !B} or {TAKE ?any : string !B})) * . {RESERVE !B} ] false and [ (not ({LEND ?any : string !B} or {TAKE ?any : string !B} or {TRANSFER ?any : string !B} or {RESERVE ?any : string !B})) * .

[

  true * . {LEND ?M : string ?B : string} . (not ({RETURN !B})) * . {RESERVE !M !B} ] false Requirement R8 "A book cannot be lent to a member if it is reserved" macro R 8 (B, M 1 , M 2 ) = ( [ true * . {RESERVE !M 1 !B} . (not ({TAKE !M 1 !B} or {CANCEL !M 1 !B})) * . {LEND !M 2 !B} ] false )end macro R 8 ("B1", "M1", "M2")

macro R 9

 9 (B, M ) = ( [ true * . {RESERVE !M !B} . (not ({TAKE !M !B} or {CANCEL !M !B})) * . {RENEW !B} ] false ) end macro R 9 ("B1", "M1")Requirement R10 "A member is allowed to take a reserved book only if he owns the oldest reservation"[ true * . {RESERVE ?M 1 : string ?B : string} . (not ({TAKE !M 1 !B} or {CANCEL !M 1 !B} or {TRANSFER !M 1 !B})) * . {RESERVE ?M 2 : string !B where M 2 = M 1 } . (not ({TAKE !M 1 !B} or {CANCEL !M 1 !B} or {TRANSFER !M 1 !B})) * . {TAKE !M 2 !B} ] falseThis property has been rephrased in the following way: If two members reserve a book, the first member to get it, is the first to have ordered it. Requirement R11 "A book can be taken only if it is not borrowed " macro R 11 (B, M ) = ( [ true * . ({LEND !M !B} or {TAKE !M !B}) . (not ({RETURN !B})) * . ({LEND !M !B} or {TAKE !M !B}) . (not ({RETURN !B})) * . {RETURN !B} ] false ) end macro R 11 ("B1", "M1")

  macro R 13 (B, M ) = ( [ true * . ({LEND !M !B} or {TAKE !M !B}) . (not ({RETURN !B} or {TRANSFER !"M2" !B} or {TRANSFER !"M3" !B})) * . {LEAVE !M } . (not ({RETURN !B} or {TRANSFER !"M2" !B} or {TRANSFER !"M3" !B})) * .({RETURN !B} or {TRANSFER !"M2" !B} or {TRANSFER !"M3" !B}) ] false and[ true * . {RESERVE !M !B} . (not ({TAKE !M !B} or {CANCEL !M !B})) * . {LEAVE !M } . (not ({TAKE !M !B} or {CANCEL !M !B})) * . ({TAKE !M !B} or {CANCEL !M !B}) ] false ) end macro R 13 ("B1", "M1")Requirement R14 "Ultimately, there is always a procedure that enables a member to leave the library"macro R 14 (M ) = ( [ true * . {JOIN !M } . (not {LEAVE !M }) * ] (not {LEAVE !M }) * . {LEAVE !M } true ) end macro R 14 ("M1")Requirement R15 "A member cannot borrow more than the loan limit defined at the system level for all users" macro R 15 (M ) = ( [ true * . let B 1 : string := "B1", B 2 : string := "B2" in({LEND !M !B 1 } or {TAKE !M !B 1 }) . (not ({TRANSFER ?M 2 : string !B 1 } or {RETURN !B 1 })) * .({LEND !M !B 2 } or {TAKE !M !B 2 }) end let ] false ) end macro R 15 ("M1")

  Example Revisited. The main process of the LNT specification describing the library management system is defined as follows:

	||
	M [Acquire, Discard , Register , Unregister , Lend , Return]
	end par
	end process
	end loop
	end var
	end process
	Fig. 10. Process pr C
	end select
	end loop
	||
	par
	loop L in
	select break L [] member [Register , Unregister , Lend , Return] (m 1 )
	end select
	end loop
	||
	loop L in
	end select
	end loop
	end par
	end par

process Main [Acquire, Discard , Register , Unregister , Lend , Return : any] is par Acquire, Discard , Register , Unregister , Lend , Return in par loop L in select break L [] book [Acquire, Discard ] (b 1 ) select break L [] member [Register , Unregister , Lend , Return] (m 2 )

  book [Acquire, Discard : any] (bId : BOOKID) is var borrower : BOR in Acquire(bid); Discard (bId, ?borrower) where (borrower [ord (bId)] eq m ⊥ ) end var end process process member [Register , Unregister , Lend , Return : any] (mId : MEMBERID) is The definition of LNT process member depends on LNT process loan, whose definition is given below:

	Register (mId);
	loop L in
	select break L [] loan [Lend , Return] (mId, b1)
	end select
	end loop;
	Unregister (mId)
	end process

process loan [Lend , Return : any] (mId : MEMBERID, bId : BOOKID) is var borrower : BOR, nbLoans : NB in (* NbLoans is set to 1 *) in Lend (bId, mId, ?nbLoans, ?borrower)

Table 1 .

 1 Model checking results for the library management system

	(m, p) (3,2)	(3,3)	(3,4)	(4,3)
	states 1,002	182,266	8,269,754 27,204,016
	trans. 5,732 1,782,348 105,481,364 330,988,232
	time	1.9s	14.4s	31'39s	140'22s
	R1	0.3s	1.8s	5'19s	20'13s
	R2	0.2s	2.9s	9'26s	36'7s
	R3	0.2s	9.4s	97'46s	26'47s
	R4	0.2s	1.7s	5'15s	18'40s
	R5	0.2s	2.2s	6'46s	21'52s
	R6	0.2s	4.1s	38'30s	10'19s
	R7	0.2s	7.4s	65'22s	24'33s
	R8	0.2s	2.2s	6'52s	22'27s
	R9	0.2s	2.3s	6'38s	22'29s
	R10	0.3s	13.3s	43'59s	62'07s
	R11	0.3s	2.5s	6'36s	22'14s
	R12	0.3s	4.0s	10'47s	45'09s
	R13	0.4s	4.3s	11'46s	36'07s
	R14	0.3s	3.6s	10'41s	37'33s
	R15	0.2s	2.8s	7'53s	28'56s

  process Main [Acquire, Discard , Register , Unregister , Lend , Return : any] is par Acquire, Discard , Register , Unregister , Lend ,

	Return in
	par
	loop L in
	select break L [] book [Acquire, Discard ] (b 1 )
	end select
	end loop
	||
	par
	loop L in
	select break L [] member [Register , Unregister , Lend , Return] (m 1 )
	end select
	end loop
	||
	loop L in
	select break L [] member [Register , Unregister , Lend , Return] (m 2 )
	end select
	end loop
	end par
	end par
	||
	M [Acquire, Discard , Register , Unregister , Lend , Return]
	end par
	end process
	end module

  process M [Acquire, Discard , Register , Lend , Take, Renew , Return, Reserve, Cancel , Unregister , Transfer : any] is var mId : mId , bId : BID, acquired : ACQUIR, borrower : BOR, nbLoans : NB , reservation : RESERV in acquired := ACQUIR(false); borrower := BOR(m ⊥ ); Lend (?bId , ?mId , !acquired, !borrower, !reservation, !nbloans); Take, Renew , Return, Reserve, Cancel , Transfer : any] (mId : MID, bId : BID) is var acquired : ACQUIR, borrower : BOR, reservation : RESERV , nbLoans : NB in select Take, Renew , Return, Reserve, Cancel , Transfer ] (m 1 , b 1 ) end select end loop || loop L 2 in select break L 2 [] member [Lend , Take, Renew , Return, Reserve, Cancel , Transfer ] (m 1 , b 2 ) Take, Renew , Return, Reserve, Cancel , Transfer ] (m 2 , b 1 ) end select end loop || loop L 2 in select break L 2 [] member [Lend , Take, Renew , Return, Reserve, Cancel , Transfer ] (m 2 , b 2 ) end select end loop end par; var nbLoans : NB , bId : BID, reservation : RESERV in Unregister (m 2 , ?nbLoans, ?reservation) where ((nbLoans [ord (m 2 )] eq 1) and (is reserved (m 2 , reservation [ord (b 1 )]) eq false) and (is reserved (m 2 , reservation [ord (b 2 )]) eq false)) . MCL Formulas for Requirements R1 to R15 Requirement R1 "A book can always be acquired by the library when it is not currently acquired " macro R 1 (B) = ( [ (not {ACQUIRE !B}) * ] {ACQUIRE !B} true and [ true * . {DISCARD !B} . (not {ACQUIRE !B}) * ] {ACQUIRE !B} true )

	|| process member [Lend , Lend (!bId , !mId , ?acquired, ?borrower, ?reservation, ?nbloans) loop L 1 in select break L 1 [] book [Acquire, Discard ] (b 2 ) end select end loop end par
	||	nbLoans := NB (0); reservation : RESERV (NIL); where ((acquired [ord (bId )] eq true) and (borrower[ord (bId )] eq m ⊥ ) and
	loop select [] Discard (?bId , !borrower, !reservation); Acquire (?bId ); acquired [ord (bId )] := true acquired [ord ()] := false [] Register (?mId ); nbLoans [ord (mId )] := 1 [] Unregister (?mId !nbLoans !reservation) nbLoans [ord (mId )] := 0 (nbLoans[ord (mId )] lt 2) and par (nil reservation (reservation [ord (bId )] eq true)) loop L 1 in select break L 1 [] loop L in select break L [] Register(m 1 ); Renew (!bId , ?acquired, ?borrower, ?reservation) par where ((acquired [ord (bId )] eq true) and (borrower[ord (bId )] eq mId ) and loop L 2 in select break L 2 [] (nil reservation (reservation [ord (bId )]) eq true)) end select end loop; select Return (!bId , ?acquired, ?borrower) member [Lend , end select end loop; end par; end var end select end loop || loop L 1 in select break L 1 [] Register(m 2 ); par loop L 2 in select break L 2 [] [] borrower [ord (bId )] := m ⊥ end loop end var end process process book [Acquire, Discard : any] (bId : BID) is var acquired : ACQUIR, borrower : BOR, reservation : RESERV in Acquire(bId ); Discard (bId , ?borrower, ?reservation) where ((borrower [ord (bId )] eq m ⊥ ) and Transfer (!mId , !bId , ?acquired, ?borrower, ?reservation, ?nbLoans) where ((acquired [ord (bId )] eq true) and (borrower [ord (bId )] eq mId ) and (nbLoans [ord (mId )] gt 0) and (nbLoans [ord (mId )] lt 2) and (nil reservation (reservation [ord (bId )]) eq true)) end var member [Lend , end var
	(nil reservation (reservation[ord (bId )]) eq true)) end select end select end loop;
	end var end var end par
	end process end process ||
		Transfer ]
	end par
	end process
	end module

borrower [ord (bId )] := mId ; nbLoans [ord (mId )] := nbLoans [ord (mId )] + 1 [] Reserve (?mId , ?bId , !acquired, !borrower, !reservation); reservation [ord (bId )] := add reservation(mId , reservation [ord (bId )]) [] Take (?mId , ?bId , !acquired, !borrower, !reservation, !nbLoans); borrower [ord (bId )] := mId ; nbLoans [ord (mId )] := nbLoans [ord (mId )] + 1; reservation [ord (bId )] := cancel reservation(mId , reservation [ord (bId )]) [] Cancel (?mId , ?bId ); reservation [ord (bId )] := cancel reservation(mId , reservation [ord (bId )]) [] Transfer (?mId , ?bId , !acquired, !borrower, !reservation, !nbLoans); nbLoans [ord (borrower [ord (bId )])] := nbLoans [ord (borrower [ord (bId )])] -1; borrower [ord (bId )] := mId ; nbLoans [ord (mId )] := nbLoans [ord (mId )] + 1 [] Renew (?bId , !acquired, !borrower, !reservation) [] Return (?bId , !acquired, !borrower); nbLoans [ord (borrower [ord (bId )])] := nbLoans [ord (borrower [ord (bId )])] -1; where ((acquired [ord (bId )] eq true) and (borrower[ord (bId )] eq mId )) [] var mId : MID in mId := any MID where ((mId ne m ⊥ ) and (mId ne m ⊥ )); Transfer (!mId , !bId , ?acquired, ?borrower, ?reservation, ?nbLoans) where ((acquired [ord (bId )] eq true) and (borrower [ord (bId )] eq mId ) and (nbLoans [ord (mId )] gt 0) and (nbLoans [ord (mId )] lt 2) and (nil reservation (reservation [ord (bId )]) eq true)) end var end select [] Reserve (!mId , !bId , ?acquired, ?borrower, ?reservation, ?nbLoans) where ((acquired [ord (bId )] eq true) and (borrower[ord (bId )] ne m ⊥ ) and (borrower[ord (bId )] ne mId ) and (is reserved (mId , reservation [ord (bId )]) eq false); select Take (!mId , !bId , ?acquired, ?borrower, ?reservation, ?nbloans) where ((acquired [ord (bId )] eq true) and (borrower[ord (bId )] eq m ⊥ ) and (nbLoans[ord (mId )] lt 2) and (last reservation (mId , reservation [ord (bId )]) eq true)) [] Cancel (!mId , !bId ) end select [] Return (!bId , ?acquired, ?borrower) where ((acquired [ord (bId )] eq true) and (borrower[ord (bId )] eq mId )) [] var mId : MID in mId := any MID where ((mId ne m ⊥ ) and (mId ne m ⊥ )); process Main [Register , Lend , Take, Renew , Return, Reserve, Cancel , Unregister , Acquire, Discard : any] is par Register , Lend , Take, Renew , Return, Reserve, Cancel , Unregister , Acquire, Discard in par par loop L 1 in select break L 1 [] book [Acquire, Discard ] (b 1 ) end select end loop var nbLoans : NB , bId : BID, reservation : RESERV in Unregister (m 1 , ?nbLoans, ?reservation) where ((nbLoans [ord (m 1 )] eq 1) and (is reserved (m 1 , reservation [ord (b 1 )]) eq false) and (is reserved (m 1 , reservation [ord (b 2 )]) eq false)) M [Acquire, Discard , Register , Lend , Take, Renew , Return, Reserve, Cancel , Unregister , C

T k denotes x k 's type as well as the corresponding domain of elements that can be assigned to x k

Such a form, commonly called head normal form[START_REF] Bergstra | Handbook of Process Algebra[END_REF], is used principally in the context of the process algebra ACP[START_REF] Bergstra | Algebra of Communicating Processes with Abstraction[END_REF] to analyse the behaviour of recursive processes.

The code for the memory M is then given as follows:

process

Lend is executed first. According to the LNT semantics, it results from the multiway synchronization of the following three actions:

• "Lend (b 1 , m 1 , ?f )" in the above expression,

• "Lend (?b, ?m, ?f ) where borrower [ord(b 1 )] = ⊥ ∧ nbLoans[ord(m 1 )] < NbLoans" in process pr C (at this moment, start is true, see Fig. 10), and • "Lend (?b, ?m, !f )" in process M (see Fig. 7). Thus, in pr C at synchronization time, f is an up-to-date copy of the memory stored in M , b = b 1 , and m = m 1 . The only condition for the synchronization to occur is the guard mod (C), whose value is computed using the up-to-date copy f of the memory. In case mod (C) evaluates to true, no other action (susceptible to modifying f ) can occur between the evaluation of mod (C) and the occurrence of Lend as both happen synchronously, thus achieving the guard-action atomicity. Once Lend has occurred, Return can occur without any condition, as the value of start has now become false.

We developed an automatic translator tool from eb 3 specifications to LNT, named eb 3 2lnt, implemented using the Ocaml Lex/Yacc compiler construction technology. It consists of about 900 lines of OCaml code. We applied eb 3 2lnt on a benchmark of eb 3 specifications, which includes variations of the library management system.

We noticed that, for each eb 3 specification, the code size of the equivalent LNT specification is twice as big. Part of this expansion is caused by the fact that LNT is more structured than eb 3 : LNT requires more keywords and gates have to be declared and passed as parameters to each process call. By looking at the Rules of Figure 9, we can see that the other causes of expansion are Rule (5), which duplicates the condition C, and Rule (9), which duplicates the body E 0 of the quantified parallel composition operator "|[∆]|x : V : E 0 " as many times as there are elements in the set V . Both expansions are linear in the size of the source eb 3 code. However, in the case of a nested parallel composition "

the expansion factor is as high as the product of the number of elements in the respective sets V 1 , . . . , V n , which may be large. If E 0 is a big process expression, the expansion can be limited by encapsulating E 0 in a parameterized process "P E0 (x 1 , . . . , x n )" and replacing duplicated occurrences of E 0 by appropriate instances of P E0 .

Case Study Revisited

We illustrate below the application of the eb 3 2lnt translator in conjunction with CADP for analyzing an extended version of the IS library management system, whose description in eb 3 can be found in Annex C of [START_REF] Gervais | Combinaison de spécifications formelles pour la modélisation des systèmes d'information[END_REF]. With respect to the simplified version presented in Section 3, the IS enables e.g., members to renew their loans and to reserve books, and their reservations to be cancelled or transferred to other members on demand. The desired behaviour of this IS was characterized in [START_REF] Frappier | Comparison of model checking tools for information systems[END_REF] as a set of 15 requirements expressed informally as follows: R1. A book can always be acquired by the library when it is not currently acquired. R2. A book cannot be acquired by the library if it is already acquired.

R3. An acquired book can be discarded only if it is neither borrowed nor reserved. R4. A person must be a member of the library in order to borrow a book. R5. A book can be reserved only if it has been borrowed or already reserved by some member. R6. A book cannot be reserved by the member who is borrowing it. R7. A book cannot be reserved by a member who is reserving it. R8. A book cannot be lent to a member if it is reserved. R9. A member cannot renew a loan or give the book to another member if the book is reserved. R10. A member is allowed to take a reserved book only if he owns the oldest reservation. R11. A book can be taken only if it is not borrowed. R12. A member who has reserved a book can cancel the reservation at anytime before he takes it. R13. A member can relinquish library membership only when all his loans have been returned and all his reservations have either been used or cancelled. R14. Ultimately, there is always a procedure that enables a member to leave the library. module library is type mId is m 1 , m 2 , m ⊥ with "eq", "ne", "ord", "val" end type type BID is b 1 , b ⊥ with "eq", "ne", "ord", "val" end type type NB is array[0. , m ⊥ with "eq", "ne", "ord", "val" end type type BID is b 1 , b 2 , b ⊥ with "eq", "ne", "ord", "val" end type type MIDLIST is NIL, CONS (HD : MID, T L : MIDLIST ) with "eq", "ne" end type type ACQUIR is array[0.