# Efficient Operational Semantics for *EB*³ for Verification of Temporal Properties

Dimitris Vekris, Catalin Dima

► To cite this version:

Dimitris Vekris, Catalin Dima. Efficient Operational Semantics for *EB*³ for Verification of Temporal Properties. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.133-149, 10.1007/978-3-642-40213-5_9. hal-01514655

HAL Id: hal-01514655

https://inria.hal.science/hal-01514655

Submitted on 26 Apr 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à 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.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Efficient Operational Semantics for EB³ for
Verification of Temporal Properties

Dimitris Vekris and Catalin Dima

LACL, Université Paris-Est
61 av. du Général de Gaulle
94010 Créteil, France
{dimitrios.vekris,dima}@u-pec.fr

**Abstract.** EB³ is a specification language for information systems. The core of the EB³ language consists of process algebraic specifications describing the behaviour of the entity types in a system, and attribute function definitions describing the entity attribute types. The verification of EB³ specifications against temporal properties is of great interest to users of EB³. We give here an operational semantics for EB³ programs in which attribute functions are computed during program evolution and their values are stored into program memory. By assuming that all entities have finite domains, this gives a finitary operational semantics. We then demonstrate how this new semantics facilitates the translation of EB³ specifications to LOTOS NT (LNT for short) for verification of temporal properties with the use of the CADP toolbox.

**Keywords:** Information Systems, EB³, Process Algebras, Operational Semantics, Bisimulation, Verification, Model Checking.

## 1 Introduction

The EB³ [10] method is an event-based paradigm for information systems (ISs) [17]. A typical EB³ specification defines entities, associations, and their respective attributes. The process algebraic nature of EB³ permits the explicit definition of intra-entity constraints. Yet its specificity against common state-space specifications, such as the *B method* [1] and *Z*, lies in the use of attribute functions, a special kind of recursive functions on the system trace, which combined with guards, facilitate the definition of complex inter-entity constraints involving the history of events. The use of attribute functions is claimed to simplify system understanding, enhance code modularity and streamline maintenance.

In this paper, we present part of our work regarding the verification of EB³, i.e. the detection of errors inherent in EB³ specifications. Specification errors in EB³ can be detected with the aid of static properties also known as invariants or dynamic properties known as temporal properties. From a state-based point of view, an invariant describes a property on state variables that must be preserved by each transition or event. A temporal property relates several events. Tools such as *Atelier B* [7] provide methodologies on how to define and prove invariants. In [12], an automatic translation of EB³'s attribute functions into *B*
is attempted. Although the *B Method* [1] is suitable for specifying static properties, temporal properties are very difficult to express and verify in *B*. Hence, in our attempt to verify temporal properties of *EB*³ specifications we move our attention to model-checking techniques.

The verification of *EB*³ specifications against temporal properties with the use of model checking has been the subject of some work in the recent years. [9] compares six model checkers for the verification of IS case studies. The specifications used in [9] derive from specific industrial case studies, but the prospect of a uniform translation from *EB*³ program specifications is not studied. [6] casts an IS specification into LOTOS NT (LNT for short) [5] that serves as an input language to the verification suite CADP [11]. In short, the majority of these works treat specific case studies drawn from the information systems domain leading to ad-hoc verification translations, but nonetheless lacking in generalization capability.

But the main problem in verifying *EB*³ specifications against temporal-logic properties relies in the difficulty to handle the recursive definition of attribute functions if one relies on the classical, trace-based semantics. This type of semantics necessitates an unbounded memory model, and therefore only bounded model-checking can be achieved, in the absence of good abstractions that allow constructing finite-state models. This restriction is present in the original approach [10] and the subsequent model-checking attempt [9] even if all the entities utilized in the specification are finite.

We propose a formal semantics for *EB*³ that treats attribute functions as state variables (we call these variables *attribute variables*). This semantics will serve as the basis for applying a simulation strategy of state variables in LNT. 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. Our main contribution is an operational semantics in which attribute functions are computed during program evolution and stored into program memory. We show that this operational semantics is bisimilar with the original, trace-based operational semantics.

Furthermore, we explore the implications of this result to the translation of *EB*³ specifications into LNT. LNT is a process algebra specification that derived from LOTOS [4]. As a process algebra, it shares many common features with *EB*³ and it is one of the input languages of CADP, a toolbox with state-of-the-art verification features. CADP permits the verification of system specifications against action-based temporal properties.

Translating *EB*³ specifications to LNT is not evident. The fundamental difficulties for designing a compiler from *EB*³ into LNT are summarized in [6]. In particular, LNT does not feature global variables. Accesses to local variables is restricted in parallel processes of the form “par *proc*₁ || *proc*₂ end par”, so that every variable written in *proc*₁ cannot be accessed in *proc*₂. Although, *EB*³ programmers cannot define global variables explicitly, *EB*³ permits the use of a single state variable, the system trace, in predicates of guard statements. Attribute functions can express the evolution of entity attributes in time, option
which introduces an indirect notion of state to the language. As a result, $EB^3$ expressions of the form “$C(T) \Rightarrow E$” can be written, where $C(T)$ is a predicate that refers to the system trace (the history of events) and $E$ is a valid $EB^3$ expression.

We then present how $EB^3$ specifications can be translated to LNT for verification with CADP through an intuitive example and give some conclusions and lines for future work. The automatic translation of $EB^3$ specifications into LNT is studied in the companion paper [18]. We note that the translation of our example into LNT is produced using the tool presented in [18].

## 2 $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 trace, and (4) input/output rules, to specify outputs for input traces, or SQL used to specify queries on the business model. We limit the presentation to the process algebra and the set of attribute functions used in the IS.

We then give three operational semantics for $EB^3$. The first, named Trace Semantics (*Sem*<sub>*T*</sub>), is the standard semantics defined in [10]. The second, called Trace/Memory Semantics (*Sem*<sub>*T*/*M*</sub>), is the alternative semantics, where attribute functions are computed during program evolution and their values are stored into program memory. By removing the trace from each state in *Sem*<sub>*T*/*M*</sub>, we obtain the third semantics for $EB^3$ specifications, which we name Memory Semantics, *Sem*<sub>*M*</sub>. The relevance of the *Sem*<sub>*T*/*M*</sub> semantics comes from the fact that it is pivotal in proving the bisimulation between the trace and the memory semantics.

**Case Study.** We start by providing a simple case study which serves for introducing both the syntax and the semantics of $EB^3$. In Fig.1, we give the functional requirements of a library management system and the corresponding $EB^3$ specification. The library system contains two entity types: *books* and *members*. The process *main* is the parallel interleaving between *m* instances of process *book* and *p* instances of processes describing operations on *members*. To avoid confusion, action names begin with uppercase letters, while process and attribute function names begin with lowercase letters.

The member *mId* registers to the library in order to start borrowing books, i.e. the action *Register*(*mId*). By the action *Unregister*(*mId*), (s)he relinquishes membership from the library. The book *bId* is acquired by the library so as to become available for lending, i.e. *Acquire*(*bId*). The inverse operation is expressed by the action *Discard*(*bId*). The member *mId* borrows the book *bId*, i.e. *Lend*(*bId*, *mId*) and returns it to the library after use, i.e. *Return*(*bId*). The process *book*(*bId*) denotes the lifecycle of the *book* entity *bId* from the moment of its
1. A book can be acquired by the library. It can be discarded, but only if it has not been lent.

2. An individual must join the library in order to borrow a book.

3. A member can relinquish library membership only when all his loans have been returned.

4. A member cannot borrow more than the loan limit defined at the system level for all users.

BID = {b₁, ..., bₘ}, MID = {m₁, ..., mₚ}
main = ( ||| bId : BID : book(bId) ) ||| ( ||| mId : MID : member(mId)* )
book(bId : BID) = Acquire(bId). borrower(T, bId) = ⊥ ⇒ Discard(bId)
member(mId : MID) = Register(mId). ( ||| bId : BID : loan(mId, bId)* ). Unregister(mId)
loan(mId : MID, bId : BID) = borrower(T, bId) = ⊥ ∧ nbLoans(T, mId) < NbLoans
⇒ Lend(bId, mId). Return(bId)

nbLoans(T: tr, mId: MID): Nat⊥ =

match T with

[] → ⊥

| T'. Lend(bId, mId) → nbLoans(T', mId) + 1

| T'. Register(mId) → 0

| T'. Unregister(mId) → ⊥

| T'. Return(bId) ∧ mId = borrower(T, bId)

→ nbLoans(T', mId) - 1

| T'.. → nbLoans(T', mId)

end match

borrower(T: tr, bId: BID): MID⊥ =

match T with

[] → ⊥

| T'. Lend(bId, mId) → mId

| T'. Return(bId) → ⊥

| T'.. → borrower(T', bId)

end match

<caption>Fig. 1. EB³ Specification and Attribute Function Definitions</caption>

acquisition until its eventual discard from the library. The process member(mId)
denotes the lifecycle of the member entity mId from the point of its registration
up until its membership drop. In the body of member(mId), the process expres-
sion "|||bId : BID : loan(mId, bId)*" denotes the interleaving of m instances of
the process expression loan(mId, bId)* that, according to the standard seman-
tics of the Kleene Closure operator (*), denotes the execution of loan(mId, bId),
bId = {b₁, ..., bₘ} an arbitrary, but bounded number of times. The attribute
function borrower(T, bId), where T is the current trace, returns the current bor-
rower of book bId or ⊥ (meaning undefined) if the book is not lent, by looking
for actions of the form Lend(bId, mId) or Return(bId) in the trace. In process
book(bId), the action Discard(bId) is thus guarded by borrower(T, bId) = ⊥ to
guarantee that the book bId cannot be discarded if it is currently lent.

The use of attribute functions is not adherent to standard process algebra
practices as it may naively trigger the complete traversal and inspection of the
system trace. Alternatively, one may come up with simpler specifications based
solely on process algebra operations (without attribute functions) when the func-
tional requirements imply loose interdependence between entities and associa-
tions. For instance, if all books are acquired by the library before any other
action occurs and are eventually discarded (given that there are no more de-
mands), main's code can be modified in the following manner:

main = ( ||| bId : BID : Acquire(bId) ). ( ||| mId : MID : member(mId)* ).

( ||| bId : BID : Discard(bId) )

Note that the functional requirements are not contradicted, though the system's
behaviour changes dramatically. Programming naturally in a purely process-
algebraic style without attribute functions in EB³ may not always be obvi-
ous. In some cases, ordering constraints involving several entities are quite dif-
ficult to express without guards and lead to less readable specifications than
```pascal
main (A)
    Acq(b2).Acq(b1)
borrower(T, b1) = ⊥ → Discard(b1) |||
borrower(T, b2) = ⊥ → Discard(b2) |||
( ||| mId : MID : member(mId)* ) (B)

    Reg(m2).Reg(m1)
borrower(T, b1) = ⊥ → Discard(b1) |||
borrower(T, b2) = ⊥ → Discard(b2) |||
( ||| bId : BID : loan(m1, bId)* ). Unregister(m1). member(m1)* |||
( ||| bId : BID : loan(m2, bId)* ). Unregister(m1). member(m2)* (C)

    Lend(b1, m1)
borrower(T, b1) = ⊥ → Discard(b1) |||
borrower(T, b2) = ⊥ → Discard(b2) |||
هوئر(b1). loan(m1, b1)* ||| loan(m1, b2)*).Unregister(m1). member(m1)* |||
( ||| bId : BID : loan(m2, bId)* ). Unregister(m1). member(m2)* (D)
```

<caption>Fig. 2. Sample execution</caption>

equivalent guard-oriented solutions in EB³ style. For instance in the body of `loan(mId: MID, bId: BID)`, writing the specification without the use of the guard:

$$ borrower(T, bId) = \perp \wedge nbLoans(T, mId) < NbLoans $$

that illustrates the conditions under which a `Lend` can occur (notably when the book is available and `nbLoans` is less than the fixed bound `NbLoans`), is not trivial.

**Execution.** As a means to provide the operational intuition behind the three semantics introduced later in this section, we show how the EB³ specification above is transformed through a four-step trace, assuming that the library may contain at most two books and at most two members, that is, `BID = {b₁, b₂}` and `MID = {m₁, m₂}`.

First, we associate with the attribute function `borrower` two “memory cells”, `bor[b₁]` and `bor[b₂]`, meant to encode the value computed by the function for each book ID after each trace `T`. Similarly, we associate two memory cells `nbL[m₁]`, `nbL[m₂]` to the attribute function `nbLoans`. We also set `NbLoans = 2` for the constant used in the definition of the process term `loan`.

<table><caption>Fig. 3. States for the sample execution</caption><thead><tr><th>T</th><th>M = (bor[b<sub>1</sub>], bor[b<sub>2</sub>], nbL[m<sub>1</sub>], nbL[m<sub>2</sub>])</th></tr></thead><tbody><tr><td>A</td><td>(⊥, ⊥, ⊥, ⊥)</td></tr><tr><td>B</td><td>(⊥, ⊥, ⊥, ⊥)</td></tr><tr><td>C</td><td>(⊥, ⊥, 0, 0)</td></tr><tr><td>D</td><td>(m<sub>1</sub>, ⊥, 1, 0)</td></tr></tbody></table>

Fig.2 shows how the process term `main` evolves by executing the valid trace $T_D = Acq(b_2).Acq(b_1).Reg(m_2).Reg(m_1).Lend(b_1, m_1)$, in which `Acq` stands for
Acquire and Reg for Register, respectively. During this evolution, the two attribute functions are computed according to their specifications in Fig.2, inductively on the length of the trace. Hence, initially and after the execution of actions Acq($b_2$).Acq($b_1$), the two attribute functions are undefined for both their arguments, while after the execution of the sequence of actions Reg($m_2$).Reg($m_1$) we have “nbLoans($T[C]$, $m_1$) = nbLoans($T[C]$, $m_2$) = 0” and borrower($T, $) remains undefined. These values are employed in order to check “borrower($T$, $b_1$) = $\perp$ & nbLoans($T$, $m_1$) < 2”, which leads to the possibility for member $m_1$ to lend book $b_1$, and therefore to transform the process term at (C) in the process term at (D).

On the other hand, the table in Fig.3 indicates the memory status after each (pair of) actions in the given trace. Initially, all memory cells carry the undefined value. After the trace $T[C]$, the value of memory cell $nbL_C[m_1]$ equals nbLoans($T[C]$, $m_1$), and, similarly, “$nbL_C[m_2] = nbLoans(T[C]$, $m_2)$”. Note that the constraint checked at step $C \to D$ gives the same value regardless of the utilization of the value computed recursively for the attribute functions borrower and nbLoans, or by using the corresponding memory cells. Furthermore, the execution of action Lend($b_1$, $m_1$) triggers the update of the memory cell bor[$b_1$] to $m_1$ and the incrementation of $nbL[m_1]$ to 1. This is modeled by the application of a function next, which defines the evolution of the system memory, and which is defined as follows: “$bor_D[b_1] = next(bor_C[b_1])$ $^1$m1 $^2$”, “$bor_D[b_2] = bor_C[b_2] = \perp$”, “$nbL_D[m_1] = nbL_C[m_1] + 1 = 1$” and also “$nbL_D[m_2] = 0$”.

**EB$^3$ Syntax and Sem$_T$.** We proceed with the formal definition of EB$^3$. We define a set of attribute function names AtFct = {$f_1, ..., f_n$} and a set of process function names PFct = {$P_1, ..., P_m$}. Let $\rho \in Act$ stand for an action of either form $\alpha(p_1: T_1, ..., p_n: T_n)$, where $\alpha \in lab$ $^3$ is the label of the action and $p_i, i \in 1..n$ are elements of type $T_i$, or $\lambda$, which stands for the internal action. To simplify the presentation, we assume that all attribute functions $f_i$ have the same formal parameters $\bar{x}$. An EB$^3$ specification is a set of attribute function definitions AtF and a set of process definitions ListPE.

Sem$_T$ [10] is given in Fig. 4 as a set of rules named $R_T - 1$ to $R_T - 11$. Each state is represented as a tuple $(E, T)$, where $E$ stands for an EB$^3$ expression and $T$ for the current trace. An action $\rho$ is the simplest EB$^3$ process, whose semantics are given by rules $R_T - 1, 1'$. Note that $\lambda$ is not visible in the EB$^3$ execution trace, i.e., it does not impact the definition of attribute functions. The symbol $\surd$ denotes successful execution. EB$^3$ processes can be combined with classical process algebra operators such as the sequence $(R_T - 2, 3)$, the choice $(R_T - 4)$ and the Kleene Closure $(R_T - 5, 6)$ operators. Rules $(R_T - 7, 8, 9)$ refer to the parallel composition $E_1|[(\Delta)|E_2]$ of $E_1, E_2$ with synchronization on $\Delta \subseteq lab$. The condition in($\rho$, $\Delta$) is true, iff the label of $\rho$ belongs to $\Delta$. The symmetric rules

<footnote n="1">¹ here notation next($x_C$) denotes the modification on $x$'s value in state (C) after executing transition $C \to D$</footnote>

<footnote n="2">² see borrower's script for "$T = T'.Lend(bId, mId)$" in Fig.1</footnote>

<footnote n="3">³ we assume lab = {$\alpha_1, ..., \alpha_q$}</footnote>
<figure><img src="image_2.png" /><figcaption>**Fig. 4.** $\mathbf{EB}^3$ Syntax and $\mathbf{Sem}_T$</figcaption></figure>

for *choice* and *parallel* composition have been omitted. Expression $E_1 \llbracket E_2 \rrbracket$ is equivalent to $E_1 \llbracket \emptyset \rrbracket | E_2$ and $E_1 \llbracket E_2 \rrbracket | E_1 \llbracket \text{lab} \rrbracket | E_2$.

In $R_T - 10$, the *guarded expression* process “$C(T) \Rightarrow E$” can execute $E$ if the predicate $C(T)$ holds. The syntax of $C(T)$ is given below:

$$ C(T) ::= true \mid false \mid op(C(T), \dots, C(T)) \mid f_i(T, \dots), i \in 1..n, op \in \{\wedge, \vee\} $$

This syntax is simplified in the sense that certain expressions cannot be supported in practice, e.g. "$nbLoans(T, mId) < NbLoans$" in Fig.1. To palliate this, we need to add an attribute function name $nbLoans\_lt\_NbLoans$ to AtFct and a corresponding attribute function definition that implements this inequality. Finally, "$nbLoans(T, mId) < NbLoans$" has to be replaced by $nbLoans\_lt\_NbLoans$ in the $\mathbf{EB}^3$ specification. Note also that this syntax makes strictly use of those "$f_i(T, \dots), i \in 1..n$" with Boolean return-type. Thus, the interpretation function of *guarded expressions* $\| \cdot \|$ is the standard Boolean interpretation.

Quantification is permitted for *choice* and *parallel* composition. If $V$ is a set of attributes $\{t_1, \dots, t_n\}$, $|x:V:E$ and $|[\Delta]|x:V:E$ stand respectively for
<figure><img src="image_3.png" /><figcaption>Fig. 6. Sem<sub>M</sub></figcaption></figure>

that keeps the current valuation for attribute function $f_i$ with parameter vector $\bar{x}$. $M_i$ refers to attribute function $f_i$. Given that the $EB^3$ specification is valid, there is at least one $cond_i^{j,k}$ that is evaluated true on every run. The action $\rho_j$ to occur “chooses” the corresponding $cond_i^{j,k}$ non-deterministically (in the sense that there may be many $k$ that make $cond_i^{j,k}$ evaluate to true). Function next updates $M_i$ by making use of $M_l$ for $l \ge i$ and the freshly computed next($M_l$)($\rho_j$) for $l < i$. The classic interpretations for Peano Arithmetic, Set Theory and Boolean Logic suffice to evaluate them. In $(T_{T/M}-10)$, $C[f_i \leftarrow M_i]$ denotes replacing all calls to $f_i$ in $C$ by $M_i$. The notation $\| \cdot \|$ in $\| C[f_i \leftarrow M_i] \|$ corresponds to the standard interpretation of Boolean operators.

Sem<sub>M</sub>. Sem<sub>M</sub> is given in Fig.6 as a set of rules named $S_M-1$ to $S_M-11$. Sem<sub>M</sub> derives from Sem<sub>T/M</sub> by simple elimination of T from each tuple (E, T, M) in rules $T_{T/M}-1$ upto $T_{T/M}-11$. It gives a finite state system. Intuitively, this means that the information on the history of executions is kept in M, thus rendering the presence of trace T redundant.

## 3 Bisimulation Equivalence of Sem<sub>T</sub>, Sem<sub>T/M</sub> and Sem<sub>M</sub>

We present the proof of the bisimulation equivalence for the three semantics: Sem<sub>T</sub>, Sem<sub>T/M</sub> and Sem<sub>M</sub>.

LTSs. We consider finite labeled transition systems (LTSs) as interpretation models, which are particularly suitable for action-based description formalisms such as $EB^3$. Formally, an LTS is a triple $(S, \{\to^a\}_{a \in Act}, I)$, where: (1) S is a set
of states, (2) $\xrightarrow{a} \subseteq S \times S$, for all $a \in Act$, (3) $I \subseteq S$ is a set of initial states.

**Bisimulation.** Bisimulation is a fundamental notion in the framework of concurrent processes and transition systems. A system is bisimilar to another system if the former can mimic the behaviour of the latter and vice-versa. In this sense, the associated systems are considered indistinguishable. Given two LTSs $TS_i = (S_i, \{\xrightarrow{a_i} a_i\}_{a_i \in Act}, I_i)$, where $i = 1, 2$ and a relation $R \subseteq S_1 \times S_2$, $R$ is said to be a bisimulation and $TS_i$ are said to be equivalent w.r.t. bisimulation iff

1. $\forall s_1 \in I_1 \exists s_2 \in I_2$ such that $(s_1, s_2) \in R$.

2. $\forall s_2 \in I_2 \exists s_1 \in I_1$ such that $(s_1, s_2) \in R$.

3. $\forall (s_1, s_2) \in R$:

(a) if $s_1 \xrightarrow{a_1} s'_1$ then $\exists s'_2 \in S_2$ such that $s_2 \xrightarrow{a_2} s'_2$ and $(s'_1, s'_2) \in R$;

(b) if $s_2 \xrightarrow{a_2} s'_2$ then $\exists s'_1 \in S_1$ such that $s_1 \xrightarrow{a_1} s'_1$ and $(s'_1, s'_2) \in R$.

**LTS Construction.** For a given $EB^3$ process $E$, we associate three LTSs w.r.t. $Sem_T$, $Sem_{T/M}$ and $Sem_M$ respectively. These correspond to the LTSs generated inductively by the rules given in Fig.4-6. The whole process mimicks the construction of a transition system associated with a transition system specification, as in [16]. For the rest, we denote $TS_T$, $TS_{T/M}$ and $TS_M$ for $TS_E$ w.r.t. $Sem_T$, $Sem_{T/M}$ and $Sem_M$ respectively.

**Theorem 1.** $TS_T$ and $TS_{T/M}$ are equivalent w.r.t. bisimulation.

*Proof.* Let $\xrightarrow{\to_1}$ be the transition relation for $TS_T$ and $\xrightarrow{\to_2}$ be the transition relation for $TS_{T/M}$. The relation, which will give the bisimulation between $TS_T$ and $TS_{T/M}$, is: $R = \{(\langle E, T, M \rangle, \langle E, T \rangle) | (E, T, M) \in S_{T/M} \wedge (E, T) \in S_T\}$. Note first that $\langle (E^0, []), M^0 \rangle, \langle (E^0, [] \rangle \in R$. We show that for any $\langle (E, T, M), (E, T) \rangle \in R$ and $(E, T, M) \xrightarrow{\rho_1} (E', T', M') \in \delta_{T/M}$, we obtain $(E, T) \xrightarrow{\rho_2} (E', T') \in \delta_T$ and vice-versa. We proceed with structural induction on $E$ and present the proof for some cases.

For $(T_{T/M}-1)$, suppose $(\rho, T, M) \xrightarrow{\rho_1} (\sqrt{T \cdot \rho}, next(M)(\rho)) \in \delta_{T/M}$. The rule $(R_T-1)$ allows us to conclude that also $(\rho, T) \xrightarrow{\rho_2} (\sqrt{T \cdot \rho}) \in \delta_T$. Conversely, suppose $(\rho, T) \xrightarrow{\rho_2} (\sqrt{T \cdot \rho}) \in \delta_T$. Note that each state $(E, T, M) \in S_{T/M}$ is of the form:

$$ (E, T, next'(T, M^0)), \text{ where} \\ next'(T, M) = \mathbf{match} \ T \ \mathbf{with} \ [\ ] \to M \mid T' \cdot \rho \to next'(T', next(M, \rho)) $$

Thus, there exists $(\rho, T, next'(T, M^0)) \xrightarrow{\rho_1} (\sqrt{T \cdot \rho}, next'(T \cdot \rho, M^0)) \in \delta_{T/M}$, which establishes rule $(T_{T/M}-1)$ by replacing $next'(T, M^0)$ with $M$ as well as $next'(T \cdot \rho, M^0)$ with $next(M)(\rho)$.

For $(T_{T/M}-2)$, suppose $(E_1.E_2, T, M) \xrightarrow{\rho_1} (E'_1.E_2, T', M') \in \delta_{T/M}$, which relies on the existence of a transition $(E_1, T, M) \xrightarrow{\rho_1} (E'_1, T', M') \in \delta_{T/M}$. By the induction hypothesis, $(E_1, T) \xrightarrow{\rho_2} (E'_1, T') \in Sem_T$ and by $(R_T-2)$, we get $(E_1.E_2, T) \xrightarrow{\rho_2} (E'_1.E_2, T') \in \delta_T$. Vice-versa, by virtue of $(R_T-2)$ a transition $(E_1.E_2, T) \xrightarrow{\rho_2} (E'_1.E_2, T') \in \delta_T$ necessitates $(E_1, T) \xrightarrow{\rho_2} (E'_1, T') \in \delta_T$. Using
the induction hypothesis, $(E_1, T, M) \xrightarrow{\rho_1} (E'_1, T', M')$. Finally, by $(T_{T/M}-2)$ we obtain $(E_1 \cdot E_2, T, M) \xrightarrow{\rho_1} (E'_1 \cdot E_2, T', M')$.

For $(T_{T/M}-10)$, we must prove that $\|C(T)\| = \|C[f_i \leftarrow M_i]\|$. Making use of the syntactic definition of $C(T)$ and the interpretation of $\| \cdot \|$, it suffices to prove that $f_i(T, \bar{x}) = M_i(\bar{x})$, $i \in 1..n$ for any parameter vector $\bar{x}$ and trace $T$. We prove this by induction on $T$.

For $T = []$, it is trivially $f_i(T, \bar{x}) = M_i^0(\bar{x}) = \|\exp_i^0(\bar{x})\|$, as $\exp_i^0(\bar{x})$ contains no calls to other attribute functions. If $f_i(tl(T), \bar{x}) = M_i(\bar{x})$, $i \in 1..n$, we need to prove that:

$$f_i(T, \bar{x}) = \text{next}(M_i)(hd(T))(\bar{x}), i \in 1..n. \qquad (1)$$

which we do again by induction on $i$.

Starting with $i = 1$, $\text{next}(M_i)(hd(T))(\bar{x})$, can be written as:

$$\| \exp_1^{j,k}(\bar{x})[f_l \leftarrow \text{if } l < 1 \text{ then } \text{next}(M_l)(hd(T)) \text{ else } M_l] \|,$$

where $k$ is specified by $hd(T)^5$ and all calls to $f_l$, $l \in 2..n$ are replaced by $M_l$. Thus, due to the inductive hypothesis, it will be:

$$\| \exp_1^{j,k}(\bar{x}) \| = \| \exp_1^{j,k}(\bar{x})[f_l \leftarrow M_l] \|$$

A similar result holds for $\text{cond}_1^{j,k}$.

For $i > 1$, we rely on $f_l = \text{next}(M_l)(\rho_j)$, $l < i$, which guarantees that the property 1 holds for all values $l < i$.

This completes the proof of the case $(T_{T/M}-10)$. $\square$

**Theorem 2.** $TS_{T/M}$ and $TS_M$ are equivalent w.r.t. bisimulation.

*Proof.* The proof is straightforward, because the effect of the trace on the attribute functions and the program execution is coded in memory $M$. Hence, intuitively the trace is redundant. $\square$

**Corollary 1.** $TS_T$ and $TS_M$ are equivalent w.r.t. bisimulation.

*Proof.* Combining the two Theorems and the transitivity of bisimulation. $\square$

# 4 Demonstration in LNT

The translation of $EB^3$ specifications is formalized in [18]. We show here how $Sem_M$ facilitates the translation of $EB^3$ specifications to LNT for verification with the toolbox CADP. To this end, we present the translation of the $EB^3$ specification of Fig.1 into LNT for $BID=\{b_1\}$ and $MID=\{m_1, m_2\}$ as was produced by the $EB^3$2LNT compiler [18].

**LNT.** LNT combines, in our opinion, features of imperative and functional programming languages and value-passing process algebras. It has a user-friendly syntax and formal operational semantics defined in terms of labeled transition

<footnote n="5">⁵ see Fig.5</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 7. Syntax of LNT</figcaption></figure>

systems (LTSs). LNT is supported by the LNT OPEN tool of CADP, which
allows the on-the-fly exploration of the LTS corresponding to an LNT specifi-
cation. We present the fragment of LNT that is useful for this translation. Its
syntax is given in Fig.7. LNT terms denoted by *B* are built from actions, choice
(select), conditional (if), sequential composition (:), breakable loop (loop and
break) and parallel composition (par). Communication is carried out by ren-
dezvous on gates *G* with bidirectional transmission of multiple values. Gates in
LNT (denoted with letter *G* with or without subscripts) correspond to the no-
tion of labels in *EB*³. Their parameters are called offers <fnref n="6" />. An offer *O* can be
either a send offer (!) or a receive offer (?). Synchronizations may also contain
optional guards (where) expressing boolean conditions on received values. The
special action δ is used for defining the semantics of sequential composition. The
internal action is denoted by the special gate *i*, which cannot be used for syn-
chronization. The parallel composition operator allows multiway rendezvous on
the same gate. Expressions *E* are built from variables, type constructors, func-
tion applications and constants. Labels *L* identify loops, which can be stopped
using “break *L*” from inside the loop body. The last syntactic construct defines
calls to process *P* that take gates *G*₁,..., *G*ₙ and variables *E*₁,..., *E*ₙ as actual
parameters. The semantics of LNT are formally defined in [5].

**Formalization.** The principal gain from *Sem*<sub>*M*</sub> lies in the use of *attribute variables*, the memory that keeps the values to all attribute functions. We need a mechanism that simulates this memory in LNT. The theoretical foundations of our approach are developed in [18]. In particular, we explicitly model in LNT a memory, which stores the *attribute variables* and is modified each time an action is executed. We model the memory as a process *Memory* placed in parallel with the rest of the system (a common approach in process algebra). To read the values of attribute variables, processes need to communicate with the memory *M*, and every action must have an immediate effect on the memory (so as to reflect the immediate effect on the execution trace). To achieve this, the memory process synchronizes with the rest of the system on every possible action of the system, and updates its attribute variables accordingly. Additional offers are used on each action, so that the current value of attribute variables can be read

<footnote n="6">⁶ Offers are not explicitely mentioned in the syntactic rules for **par** and for procedural calls</footnote>
```pascal
process Memory[ACQ, DIS, REG, UNREG, LEND, RET: ANY] is
  var mId: MEMBERID, bid: BOOKID, borrower: BOR, nbLoans: NB in
    (* attribute variables initialized *)
    mId := mBot; borrower := BOR(mBot); nbLoans := NB(0);
loop select
  ACQ(?bid)
  [] DIS(?bid, ?borrower)
  [] REG(?mid)
  [] UNREG(?mid)
  [] LEND(?bid, ?mid, !nbLoans, !borrower); borrower[ord(bid)] := mid;
    nbLoans[ord(mid)] := nbLoans[ord(mid)] + 1
  [] RET(?bid); mId := borrower[ord(bid)]; borrower[ord(bid)] := mBot;
    nbLoans[ord(mid)] := nbLoans[ord(mid)] - 1
end select end loop
end var end process
```

<caption>Fig. 8. Memory in LNT</caption>

by processes during communication, and used to evaluate guarded expressions wherever needed.

These ideas are implemented in a tool called EB³2LNT, presented in the companion paper [18]. We provide here the translation of the case study of library (with two members and two books) into LNT, obtained using EB³2LNT.

The process *Memory* is given in Fig.8. It runs an infinite loop, which “listens” to all possible actions of the system. We define two instances of the attribute variable *nbLoans* (one for each member) and one instance for *borrower* (one book). In the LNT expression *nbLoans[ord(mid)]*, *ord(mid)* denotes the ordinate of value *mid*, i.e., a unique number between 0 and the cardinal of *mid*'s type minus 1. *nbLoans[ord(mid)]* is incremented after a *Lend* and decremented after a *Return*<fnref n="7" />. The action *Lend(mId, bId)* takes, besides *mid* and *bid*, *nbLoans* and *borrower* as parameters, because the latter are used in the evaluation of the guarded expression preceding *Lend* (*where* statement in Fig.8). Note how upon synchronisation on *Lend*, *nbLoans* and *borrower* are offered (!) by the *Memory* and received (?) by *loan* (Fig.8).

The main program is given in Fig.9. All parallel quantification operations have been expanded as LNT is more structured and verbose than EB³. For most EB³ operators, there are equivalent LNT operators [18]. Making use of the expansion rule $E^* = E.E^*|\lambda$, the Kleene Closure (as in $member(mId)^*$ in Fig.1) can be written accordingly. The full LNT program is in the appendix.

## 5 Conclusion

In this paper, we presented an alternative, traceless semantics $Sem_M$ for EB³ that we proved equivalent to the standard semantics $Sem_T$. We showed how $Sem_M$ facilitates the translation of EB³ specifications to LNT for verification of

<footnote n="7">⁷ see the definition of *nbLoans* in Fig.1</footnote>
```pascal
process MAIN [ACQ, DIS, REG, UNREG, LEND, RET: ANY] () is
par ACQ, DIS, REG, UNREG, LEND, RET in
  par
    book[ACQ, DIS](b1)
  ||
  par
    loop L in select break L [] member[REG, UNREG, LEND, RET](m1)
      end select end loop
  ||
  loop L in select break L [] member[REG, UNREG, LEND, RET](m2)
    end select end loop
end par
end par
||
Memory[ACQ, DIS, REG, UNREG, LEND, RET]
end par
end process

process loan[LEND, RET : ANY](mid: MEMBERID, bid : BOOKID) is
var borrower: BOR, nbLoans: NB in (* NbLoans is set to 1 *)
  LEND(bid, mid, ?nbLoans, ?borrower) where
    ((borrower[ord(bid)] eq mBot) and (nbLoans[ord(mid)] eq 1));
  RET(bid)
end var
end process
```

<caption>**Fig. 9.** Main program and the process associated with the computation of the attribute function *Loan* in LNT</caption>

temporal properties with CADP, by means of a translation in which the memory
used to model attribute functions is implemented using an extra process that
computes at each step the effect of each action on the memory. We presented the
LNT translation of a case study involving a library with a predefined number
of books and members, translation obtained with the aid of a compiler called
EB³²LNT. The EB³²LNT tool is presented in detail in [18].

A formal proof of the correctness of the EB³²LNT compiler is under preparation. The proof strategy is by proving that the memory semantics of each EB³ specification and its LNT translation are bisimilar, and works by providing a match between the reduction rules of SemM and the corresponding LNT rules [5].

As future work, we plan to study abstraction techniques for the verification
of properties regardless of the number of components e.g. members, books that
participate in the IS (Parameterized Model Checking). We will observe how
the insertion of new functionalities to the ISs affects this issue. Finally, we will
formalize this in the context of EB³ specifications.
## References

1. J.-R. Abrial. *The B-Book - Assigning programs to meanings*. Cambridge University Press, 2005.

2. J.A. Bergstra, A. Ponse, S.A. Smolka. *Handbook of Process Algebra*. Elsevier, 2001.

3. J.A. Bergstra, J. W. Klop. Algebra of Communicating Processes with Abstraction. In *Journal of Theor. Comput. Sci.*, 37:77–121, 1985.

4. T. Bolognesi, E. Brinksma. Introduction to the ISO specification language LOTOS. *Computer Networks and ISDN Systems*, 14(1):25–59, 1987.

5. D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, V. Powazny, F. Lang, W. Serwe, G. Smeding. *Reference Manual of the LOTOS NT to LOTOS Translator – Version 5.4*. INRIA/VASY, 2011.

6. R. Chossart. *Evaluation d'outils de vérification pour les spécifications de systèmes d'information*. Master's thesis, Université de Sherbrooke, 2010.

7. ClearSy. *Atelier B*. http://www.atelierb.societe.com.

8. R. De Nicola, F. Vaandrager. Three logics for branching bisimulation (extended abstract). In *Proc. of LICS*, pages 118–129, 1990.

9. M. Frappier, B. Fraikin, R. Chossart, R. Chane-Yack-Fa, M. Ouenzar. Comparison of model checking tools for information systems. In *Proc. of ICFEM*, Springer, 2010.

10. M. Frappier, R. St.-Denis. $EB^3$: an entity-based black-box specification method for information systems. In *Proc. of Software and System Modeling*, 2003.

11. H. Garavel, F. Lang, R. Mateescu, W. Serwe. CADP 2010: A toolbox for the construction and analysis of distributed processes. In *Proc. of TACAS*, Springer, 2011.

12. F. Gervais. *Combinaison de spécifications formelles pour la modélisation des systèmes d'information*. PhD thesis, 2006.

13. D. Kozen. Results on the propositional mu-calculus. In *Journal of Theor. Comput. Sci.*, 27:333–354, 1983.

14. C. Löding, O. Serre. Propositional dynamic logic with recursive programs. In *Proc. of FOSSACS*, Springer, 2006.

15. R. Mateescu, D. Thivolle. A model checking language for concurrent value-passing systems. In *Proc. of FM*, Springer, 2008.

16. Mohammad Reza Mousavi, Michel A. Reniers. Congruence for Structural Congruences. In *Proc. of FoSSaCS 2005*, p.47-62, 2005.

17. V. Symons and W. Geoff. The Evaluation of Information Systems: A Critique. In *Journal of Applied Systems Analysis*, 15, 1988.

18. D. Vekris, F. Lang, C. Dima, R. Mateescu. Verification of $EB^3$ specifications using CADP. http://hal.inria.fr/hal-00768310.

## A LTS Construction

The construction is given by structural induction on $E$. In particular, we show how to construct:

$$TS_E = (S_E, \delta_E, I_E)$$

w.r.t. $Sem_M$ for several cases of $E$. We refer to the initial memory as $M^0 \in \mathcal{M}$ ($\mathcal{M}$ is the set of memory mappings in the IS) defined upon the fixed body of attribute function definitions. It is $I_E = \{(E, M^0)\}$. More precisely,
1. $S_{\rho} = \{(\rho, M^0)\} \cup \{(\sqrt{\cdot}, \text{next}(M^0))\}$, $\delta_{\rho} = \{(\rho, M^0) \xrightarrow{\rho} (\sqrt{\cdot}, \text{next}(M^0))\}$, where $\rho \neq \lambda$

2. $S_{\lambda} = \{(\lambda, M^0)\} \cup \{(\sqrt{\cdot}, M^0)\}$, $\delta_{\lambda} = \{(\lambda, M^0) \xrightarrow{\lambda} (\sqrt{\cdot}, M^0)\}$

3. $$ \begin{cases} S_{E_1 \cdot E_2} = \{(E'_1 \cdot E_2, M) \mid (E'_1, M) \in S_{E_1}\} \cup \{\bigcup_{(\sqrt{\cdot}, M_1) \in S_{E_1}} S_{E_2}^{M_1}\}, \\ \delta_{E_1 \cdot E_2} = \{(E'_1 \cdot E_2, M) \to (E''_1 \cdot E_2, M') \mid (E'_1, M) \to \rho(E''_1, M') \in \delta_{E_1}\} \cup \\ \quad \{\bigcup_{(\sqrt{\cdot}, M_1) \in S_{E_1}} \delta_{E_2}^{M_1}\} \end{cases} $$

4. $TS_{E^*} = lfp_F$, where $F(TS_{E_x}) = TS_E \cdot E_x \cup TS_{\lambda}$, $E^* \doteq E \cdot E^*|_{\lambda}$

5. $TS_{E_1}[[\Delta]|E_2}$, where $E_1[[\Delta]|E_2] \doteq \sum_{i=1}^{r} C(T)^i \Rightarrow \rho^i(\bar{a}^i) \cdot E^i$

6. $$ \begin{cases} S_C(T) \Rightarrow E = \begin{cases} \{(C(T) \to E, M^0)\} \cup S_E \setminus \{(E, M^0)\}, & \text{if } \|C[f_i \leftarrow M_i^0]\| \\ \{(C(T) \to E, M^0)\}, & \text{otherwise} \end{cases} \\ \delta_C(T) \Rightarrow E = \begin{cases} \delta_E[(E, M^0) \leftarrow (C(T) \Rightarrow E, M^0)], & \text{if } \|C[f_i \leftarrow M_i^0]\| \\ \emptyset, & \text{otherwise} \end{cases} \end{cases} $$

In 3, it is $(E'_1 \cdot E_2, M) \in S_{E_1 \cdot E_2}$ if $(E'_1, M) \in S_{E_1}$. For $(\sqrt{\cdot}, M_1) \in S_{E_1}$, we obtain $(E'_2, M) \in S_{E_2}^{M_1}$, where $S_{E_2}^{M_1}$ stands for state space $S_{E_2}$ with initial memory $M_1$. In 4, we need to compute the least fix point of function $F: TS \to TS$ w.r.t. the lattice $TS = (TS, \subseteq)$, where $TS$ is the possibly infinite set of LTSs simulating $EB^3$ specifications w.r.t. $Sem_{T/M}$ and $\subseteq$ denotes inclusion. In 5, $E_1[[\Delta]|E_2$ is written as a sum of $EB^3$ expressions. The first action of each summand would be $\rho^i(\bar{a}^i)$ for all possible execution paths picking this summand. This action would be taken under condition $C^i$ (=true in the absence of condition):

$$ E_1[[\Delta]|E_2 \doteq \sum_{i=1}^{r} C(T)^i \Rightarrow \rho^i(\bar{a}^i) \cdot E^i $$

This form is known as head normal form (HNF) in the literature. The construction of HNFs for process algebra expressions is discussed in [2]. It is a common practice developed principally in the context of the Algebra of Communicating Processes (ACP) [3] as a means to analyse the behaviour of recursive process algebra definitions. Note that the rules $(S_M - 8)$ and $(S_M - 9)$ for $Sem_M$ ensure the existence of this normal form. Finally, in 6, for $\|C[f_i \leftarrow M_i^0]\| = true$, we need to construct $S_E$ and replace $(E, M^0)$ with $(C(T) \Rightarrow E, M^0)$.

## B LNT code for the Library Management System

module library is
type MEMBERID is m1, m2, mBot with "eq", "ne", "ord" end type
type BOOKID is b1, bBot with "eq", "ne", "ord" end type
type ACQUIR is array [0..1] of BOOL end type
type NB is array [0..2] of NAT end type
type BOR is array [0..1] of MEMBERID end type

process memory[ACQ, DIS, REG, UNREG, LEND, RET: ANY] is
var mId: MEMBERID, bid: BOOKID, borrower: BOR, nbLoans: NB in
(* attribute variables initialized *)
mId := mBot; borrower := BOR(mBot); nbLoans := NB(0);
loop select
    ACQ(?bid) [] DIS(?bid, ?borrower) [] REG(?mid) [] UNREG(?mid)
[] LEND(?bid, ?mid, !nbLoans, !borrower); borrower[ord(bid)] := mid;
    nbLoans[ord(mid)] := nbLoans[ord(mid)] + 1
[] RET(?bid); mId := borrower[ord(bid)]; borrower[ord(bid)] := mBot;
    nbLoans[ord(mid)] := nbLoans[ord(mid)] - 1
end select end loop
end var end process

process loan[LEND, RET : ANY](mid: MEMBERID, bid : BOOKID) is
var borrower: BOR, nbLoans: NB in (* NbLoans is set to 1 *)
    LEND(bid, mid, ?nbLoans, ?borrower) where
        ((borrower[ord(bid)] eq mBot) and (nbLoans[ord(mid)] eq 1));
    RET(bid)
end var end process

process book[ACQ, DIS: ANY](bid: BOOKID) is
var borrower: BOR in
    ACQ(bid); DIS(bid, ?borrower) where (borrower[ord(bid)] eq mBot)
end var end process

process member[REG, UNREG, LEND, RET: ANY](mid: MEMBERID) is
    REG(mid);
loop L in select break L [] loan[LEND, RET](mid, b1)
    end select end loop; UNREG(mid)
end process

process MAIN [ACQ, DIS, REG, UNREG, LEND, RET: ANY] () is
par ACQ, DIS, REG, UNREG, LEND, RET in

par
    book[ACQ, DIS](b1)
||
    par
        loop L in select break L [] member[REG, UNREG, LEND, RET](m1)
            end select end loop
    ||
        loop L in select break L [] member[REG, UNREG, LEND, RET](m2)
            end select end loop
end par
end par
|| memory[ACQ, DIS, REG, UNREG, LEND, RET]
end par
end process
end module