Bengt Jonsson

Therese Aarts

Sofia Bohlin

Olga Cassel

Falk Grinchtein

Maik Howar

Bernhard Merten

Johan Steffen

Frits Vaandrager Uijen

Learning of Automata Models Extended with Data ⋆

One of the challenges in the Connect project is to develop techniques for learning models of networked components from exploratory interaction with the component, based on analyzing messages exchanged between the component and its environment. Many approaches to this problem employ regular inference (aka. automata learning) techniques which generate modest-size finite-state models. Most communication with real-life systems involves data values being relevant to the communication context and thus influencing the observable behavior of the communication endpoints. When applying methods from the realm of automata learning, it is desirable to handle such dataoccurrences. It is therefore important to extend inference techniques to handle message alphabets and state-spaces with structures containing data parameters, often with large domains. After very briefly mentioning several approaches to the problem, we give a longer account of an approach proposed by Aarts et al, which adapts ideas from of predicate abstraction, successfully used in formal verification. We illustrate the techniques by application to a simple running example, which models a simple booking service.

Introduction

Interoperability remains a fundamental challenge when connecting heterogeneous systems which encounter and spontaneously communicate with one another in pervasive computing environments. The Connect Integrated Project [START_REF] Issarny | Connect challenges: Towards emergent connectors for eternal networked systems[END_REF] aims at overcoming the interoperability barrier by synthesizing on the fly the Connectors via which networked systems communicate. Connectors are implemented through a comprehensive dynamic process based on (i) extracting knowledge from, (ii) learning about and (iii) reasoning about, the interaction ⋆ Supported in part by EC Proj. 231167 (CONNECT).

behavior of networked systems, together with (iv) synthesizing new interaction behaviors out of the ones exhibited by the systems to be made interoperable.

One of the challenges in the Connect project is to develop techniques for learning models of exploratory interaction with the component, based on analyzing messages exchanged between the component and its environment. Generation of models by exploratory interaction can be useful also in other contexts. A large source of application might be found in model-based verification and validation, including model checking and model-based testing [START_REF]Model-Based Testing of Reactive Systems[END_REF]. Such techniques have witnessed drastic advances in the last decades, and are being applied to verification and valiation of communication protocols, hardware systems, embedded controllers, etc., also in industrial settings (e.g., [START_REF] Huima | Implementing conformiq qtronic[END_REF]). They require models that specify the intended behavior of system components, which ideally should be developed during specification and design. However, the construction of models typically requires significant manual effort, implying that in practice often models are not available, or become outdated as the system evolves. Automated support for constructing models of the behavior of implemented components would therefore be useful also, e.g., for regression testing, for replacing manual testing by model based testing, for producing models of standardized protocols, for analyzing whether an existing system is vulnerable to attacks, etc.

The construction of models from observations of component behavior can be performed using automata learning (aka. regular inference) techniques [START_REF] Angluin | Learning regular sets from queries and counterexamples[END_REF][START_REF] Dupont | Incremental regular inference[END_REF][START_REF] Gold | Language identification in the limit[END_REF][START_REF] Kearns | An Introduction to Computational Learning Theory[END_REF][START_REF] Rivest | Inference of finite automata using homing sequences[END_REF][START_REF] Trakhtenbrot | Finite automata: behaviour and synthesis[END_REF]. This class of techniques is now receiving increasing attention in the testing and verification community, e.g., for regression testing of telecommunication systems [START_REF] Hagerer | Model generation by moderated regular extrapolation[END_REF][START_REF] Hungar | Domain-specific optimization in automata learning[END_REF], for integration testing [START_REF] Groz | Modular system verification by inference, testing and reachability analysis[END_REF][START_REF] Li | Integration testing of distributed components based on learning parameterized I/O models[END_REF], security protocol testing [START_REF] Shu | Testing security properties of protocol implementations -a machine learning based approach[END_REF], and for combining conformance testing and model checking [START_REF] Peled | Black box checking[END_REF][START_REF] Groce | Adaptive model checking[END_REF]. One of the most used algorithms for regular inference, L * , is thoroughly explained in the Chapter Introduction to Active Automata Learning from a Practical Perspective by Steffen, Howar, and Merten. This algorithm poses a sequence of membership queries, each of which observes the component's output in response to a certain input word, and produces a minimal deterministic finite-state machine which conforms to the observations. If the sequence of membership queries is sufficiently large, the produced machine will be a model of the observed component.

Since regular inference techniques are designed for finite-state models, most previous applications to model generation have been limited to generating control flow skeletons, suppressing data which appear, e.g., as parameters of messages. However, data parameters have a significant impact on control flow and behavior in typical networked components and protocol entities. they can be sequence numbers, configuration parameters, agent and session identifiers, etc.; a model of a networked service is considerabely less informative if information about exchanged data is suppressed. It is therefore important to extend inference techniques to handle message alphabets and state-spaces with structures containing data parameters with large domains.

In this chapter, we will consider the problem of extending learning to automata with data, by presenting a particular approach, introduced in the work by Aarts, Jonsson, Uijen, and Vaandrager [START_REF] Aarts | Generating models of infinite-state communication protocols using regular inference with abstraction[END_REF][START_REF] Aarts | Inference and abstraction of the biometric passport[END_REF]. We first define a model for symbolic representation of protocols. Thereafter, we present a technique for using the L * algorithm, designed for inference of finite-state Mealy machines, to infer also symbolically defined protocol models. The technique is inspired by predicate abstraction [START_REF] Loiseaux | Property preserving abstractions for the verification of concurrent systems[END_REF][START_REF] Clarke | Counterexampleguided abstraction refinement for symbolic model checking[END_REF], which has been successful for extending finite-state model checking to large and infinite state spaces. In contrast to that work, however, we are now in a black-box setting, where an abstraction cannot be defined based on the source code or model of a component, since it is not accessible. Instead, we must construct an externally supplied abstraction, which translates between a large message alphabet of the component to be modeled and a small finite alphabet of the regular inference algorithm. Via regular inference, a finitestate model of the abstracted interface is inferred. The abstraction can then be reversed to generate a faithful model of the component.

The presented approach was used to learn models of reduced versions of the SIP and TCP protocols, in [START_REF] Aarts | Generating models of infinite-state communication protocols using regular inference with abstraction[END_REF], and also to learn a model of the new generation of biometric passports in [START_REF] Aarts | Inference and abstraction of the biometric passport[END_REF]. A We will also describe how to construct a suitable abstraction, utilizing pre-existing knowledge about which operators are sufficient to express guards and operations on data in a faithful model of the component.

On Related Work Regular inference techniques have been used for several tasks in verification and test generation, e.g., to create models of environment constraints with respect to which a component should be verified [START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF], for regression testing to create a specification and test suite [START_REF] Hagerer | Model generation by moderated regular extrapolation[END_REF][START_REF] Hungar | Domain-specific optimization in automata learning[END_REF], to perform model checking without access to source code or formal models [START_REF] Groce | Adaptive model checking[END_REF][START_REF] Peled | Black box checking[END_REF], for program analysis [START_REF] Ammons | Mining specifications[END_REF], and for formal specification and verification [START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF].

In several approaches, the challenge of including data parameters of message have been addressed. In the work of Shu and Lee [START_REF] Shu | Testing security properties of protocol implementations -a machine learning based approach[END_REF], parameters are essentially suppressed in order to obtain a finite subset of input symbols when learning the behavior of security protocol implementations. This subset can be extended in response to new information obtained in counterexamples. Groz, Li, and Shahbaz [START_REF] Li | Integration testing of distributed components based on learning parameterized I/O models[END_REF][START_REF] Shahbaz | Learning and integration of parameterized components through testing[END_REF][START_REF] Groz | Modular system verification by inference, testing and reachability analysis[END_REF] extend regular inference to Mealy machines with data values, for use in integration testing. In their work, they select a finite set of representative data values to be supplied together with the input to ta component.

An influential approach to learning properties of data in programs is represented by the Daikon system [START_REF] Ernst | The daikon system for dynamic detection of likely invariants[END_REF]. Its basic technique is to observe executions of a component, and extract invariants over program variables that are observed to hold. The invariants can be chosen from a predefined collection. The Daikon system does not immediately consider to extract control structures of components. There are several approaches that combine regular inference for learning control structures, and the Daikon tool (or similar) for inferring constraints on data parameters. One of the questions to be solved in such a combination is how to correlate the two types of models.

Lorenzoli, Mariani, and Pezzé infer models of software components that consider both sequence of method invocations and their associated data parameters [START_REF] Lorenzoli | Automatic generation of software behavioral models[END_REF][START_REF] Mariani | Dynamic detection of COTS components incompatibility[END_REF]. They use a passive learning approach where a finite control structure that captures possible sequences of method invocations is infer by an extension of the k-tails algorithm (a passive learning algorithm), and using Daikon [START_REF] Brun | Finding latent code errors via machine learning over program executions[END_REF] to infer guards and relations on method parameters. This allows to infer constraints on data parameters that are exchanged after specific sequences of method invocations, but not to analyze the influence of data parameter on subsequent control behavior. The same basic combination is also employed by Lo and Maoz [START_REF] Lo | Scenario-based and value-based specification mining: better together[END_REF], which infer a more refined view on constraints over data parameters, in that different constraints are generated for different scenarios, if a need for this is detected.

In previous work, we have considered extensions of regular inference to handle data parameters. In [START_REF] Berg | Regular inference for state machines with parameters[END_REF], we show how guards on boolean parameters can be refined lazily. This technique for maintaining guards have inspired the more general notion of abstractions on input symbols presented in this chapter. We have also proposed techniques to handle infinite-state systems, in which parameters of messages and state variables are from an unbounded domain, e.g., for identifiers [START_REF] Berg | Regular inference for state machines using domains with equality tests[END_REF], and timers [START_REF] Grinchtein | Learning of event-recording automata[END_REF][START_REF] Grinchtein | Learning of Timed Systems[END_REF]. These extensions are specialized towards a particular data domain, and their worst-case complexities do not immediately suggest an efficient implementation.

Organization. In the next section, we first introduce a simple running example that will serve to illustrate the techniques presented in this tutorial. Thereafter, we introduce Mealy machines, and our symbolic extension of Mealy machines, that include data. The technique of using abstraction to adapt finite-state learning algorithms to symbolically defined Mealy machines is presented in Section 5. This techniques requires an abstraction which in general must be constructed manually. A technique for systematic construction of such abstractions is presented in 7. We illustrate the application of this technique to the running example in Section 6.

A Running Example

Let us introduce a small example to illustrate the techniques that will be introduced in later sections. Imagine a service for booking seats in a concert or similar event. A user of this service has to provide his credentials and can then browse through a list of seats. From the list of seats, a single seat can be booked, which will be confirmed in a corresponding receipt.

Imagine further that an a priori interface description of the service is provided, specifying a specific set of messages that are understood by the service, containing -openSession with two parameters, a user name and a password, supplies credentials, and if they are accepted the service provides a session identifier in response, -getSeats with a session identifier as parameter, asks for a list of avaible seats that can be booked, -getSeat with a session identifier and a seat as parameters, asks to book a specific seat, and if accepted, the service will confirm by a positive reply.

The exchange of interface primitives during a typical session can be informally depicted in sequence chart in Figure 1. In the following sections, we will con-

Mealy Machines

Throughout the presentation, we will use Mealy machines to model the behavior of communication protocol entities, networked services, etc.

Definition 1. A Mealy machine is a tuple M = Σ I , Σ O , Q, q 0 , δ, λ where
-Σ I is a nonempty set of input symbols, -Σ O is a nonempty set of output symbols, -Q is a nonempty set of states, -q 0 ∈ Q is the initial state, -δ : Q × Σ I → Q is the transition function, and -λ : Q × Σ I → Σ O is the output function. ⊓ ⊔
The sets of states and symbols can be finite or infinite: if they are both finite we say that the Mealy machine is finite-state. Elements of Σ * I are called input words, and elements of Σ * O are called output words.

Intuitively, a Mealy machine behaves as follows. At any point in time, the machine is in some state q ∈ Q. When supplied with an input symbol a ∈ Σ I , it responds by producing an output symbol λ(q, a) and transforms itself to a new state δ(q, a). We use the notation q a/b -→ q ′ to denote that δ(q, a) = q ′ and λ(q, a) = b; in this case q a/b -→ q ′ is called a transition of M. We can depict Mealy machines as directed edge-labeled graphs, where Q is the set of vertices. The outgoing edges from a state q ∈ S lead to δ(q, a) for all a ∈ Σ I , and they are labeled "a/b", where a is the input symbol and b is the output symbol λ(q, a). As an example, Figure 2 shows a Mealy machine that receives a sequence of symbols of form a or b. Whenever an a-symbol is received, it outputs the number of received a-symbols modulo 2, and whenever a b-symbol is received, it outputs the number of received a-symbols modulo 4. The initial state is q 0 . Applying a word a 1 a 2 • • • a k ∈ Σ * I of input symbols starting in a state q 0 results in the sequence of states q 0 , q 1 , . . . , q k with q j = δ(q j-1 , a j ) for j = 1, . . . , k. We extend the transition function to δ(q 0 , a

q 3 q 0 q 2 q 1 b/0 b/3 b/1 b/2 a/0 a/1 a/0 a/1
1 a 2 • • • a k ) def = q k and the output function to λ(q 0 , a 1 a 2 • • • a k ) def = λ(q 0 , a 1 )λ(q 1 , a 2 ) • • • λ(q k-1 , a k ), i.e.
, the concatenation of all outputs. We define λ M (u) = λ(q 0 , u) for u ∈ Σ * I . Two Mealy machines M and M ′ with the same set of input symbols are equivalent if λ M (u) = λ M ′ (u) for all input words u.

Mealy machines are completely specified, meaning that at every state there is a next state for every input (δ and λ are total). They are also deterministic, because only one next state is possible.

Finite-state Mealy machines, introduced in the previous section, cannot represent all aspects of the behavior of protocols and networked components, where the interplay between control and data is significant. Typical such models have an infinite number of states and infinite communication alphabets that span domains of data values that are very large or infinite. Typical examples of such data domains are integers to represent sequence numbers, session identifiers, etc., strings to represent exchanged data, etc.

In this section, we introduce Symbolic Mealy Machines. They can be seen as a symbolic representation of large or infinite-state Mealy machines, in that input and output symbols have parameters which are data values, e.g., to represent messages in a typical communication protocol. Often, data parameters are from rather large (in practice "infinite") domains, and on which rather simple operations and tests are applied, e.g., equality tests between elements of the same domain, or a check whether an element is a member of some set. It seems reasonable to be able to extend automata learning to such models, in analogy with the way automated verification techniques have been extended from finite-state models to extensions that cover, e.g., clocks as in timed automata.

Data Values

We first consider the data values that occur as parameters of input and output symbols and stored in state variables that are part of the representation of the internal state of a Mealy machine. We will use d, d 1 , d 2 , etc. to range over data values. To describe the data values that are relevant for a symbolic Mealy machine, we assume a finite set of domains, each of which is a (finite or infinite) set of data values. We also assume a finite set of functions and a finite set of predicates. Each function f has an arity, denoted

D 1 × • • • × D n → D,
where D 1 , . . . , D n and D are domains, meaning that the arguments to f must be an n-tuple of data values d 1 , . . . , d n , where d i ∈ D i for i = 1, . . . , n, and then

f (d 1 , . . . , d n ) is an element in D. We write f : D 1 × • • • × D n → D to denote that f has arity D 1 × • • •× D n → D. A predicate r has an arity, denoted D 1 × • • •× D n , meaning that it can be thought of as a function from D 1 × • • • × D n to boolean values.
Input and Output Symbols Input and output symbols will be represented using finite sets I and O of (input and output) ations. Each ation α has a certain arity, which is a tuple of domains D α,1 , . . . , D α,n (where n depends on α). Let Σ I be the set of input symbols of form α(d 1 , . . . , d n ), where d i ∈ D α,i is in the appropriate domain for each i with 1 ≤ i ≤ n. The set of output symbols Σ O is defined analogously.

Example For the service introduce in Section 2, we use the following domains to represent the data values that occur in input and output symbols.

-STRING contains data values for user names and passwords.

-SESSION contains identifiers of sessions: it could be, e.g., the set of natural numbers.

-SEAT contains the possible seats (e.g., represented by seat numbers) that are available in the event, and -SEATS contains sets of seats in SEAT.

We use the following predicates.

-∈: SEAT × SEATS is the test for membership, and has passwd : STRING × STRING tests for valid combinations of usernames and passwords.

In addition, we include the equality predicate = on the domains SESSION and SEAT.

The set of input ations with corresponding arities is described in the following table.q Input ation arity openSession : STRING, STRING, SESSION getSeats :

SESSION getSeat : SESSION, SEAT
To model the response from the service, we could use one output ation for each kind of response, e.g., an ation returnSession with arity SESSION for replies to input symbols of form openSession(u, p, s). To save space, we will simply just let the reply be modeled by a data element from the appropriate domain. ⊓ ⊔

Symbolic Mealy Machines

We can now define symbolic Mealy machines. We assume a set of domains, functions, and predicates, as described in the previous paragraphs, which will be used to form expressions denoting data values, and boolean expressions to denote tests on data values. We assume that expressions always follow the restrictions of the relevant arities. We assume a set of formal parameters, ranged over by p 1 , p 2 , . . ., to be used as placeholders for parameters of symbols in symbolic transitions. We also assume a set of state variables, each with a domain of possible values, and a unique initial value. Definition 2. A Symbolic Mealy machine (SMM for short) is a tuple SM = I, O, L, l 0 , X, -→ , where -I and O are disjoint finite sets of actions (input ations and output ations), -L is a finite set of locations, -l 0 ∈ L is the initial location, -X is a finite set of state variables; each state variable x has a domain D x of possible values, and a unique initial value, and

--→ is a finite set of symbolic transitions, each of form i l i l ′ - α(p 1 , . . . , p n ) when g / x 1 , . . . , x k := e 1 , . . . , e k ; β(e out 1 , . . . , e out m )
in which • l and l ′ are locations,

• α ∈ I and β ∈ O are input and output actions,

• p 1 , . . . , p n are distinct formal parameters,

• x 1 , . . . , x k are distinct state variables in X,

• g (the guard) is a boolean expression over the formal parameters p 1 , . . . , p n and the state variables in X, and • e 1 , . . . , e k and e out 1 , . . . , e out m are tuples of expressions over p 1 , . . . , p n and X. We assume that the arities of α and β and the domains of x 1 , . . . , x k are respected.

⊓ ⊔ Intuitively, a symbolic transition of the above form denotes steps of the Mealy machine in which some input symbol of form α(d 1 , . . . , d n ) is received, whereby the formal parameters p 1 , . . . , p n are bound to the received data values d 1 , . . . , d n ; in case the guard g is evaluated to true, the state variables among x 1 , . . . , x k are assigned new values by the assignment x 1 , . . . , x k := e 1 , . . . , e k , and an output symbol, obtained by evaluating β(e out 1 , . . . , e out m ), is generated. In case the guard g is evaluted to false, then the symbolic transition does not denote any step.

Semantics of SMM

We can give a precise meaning to an SMM by letting it denote a Mealy machine with possibly infinite sets of input and output symbols and states. Such a Mealy machine can be defined as follows. Assume an SMM SM defined as the tuple I, O, L, l 0 , X, -→ . A valuation is an assignment σ which maps each location variable x in X to a data value in D x . Valuations are extended to expressions in the natural way: for instance, if σ(x 3 ) = 8, then σ(2 * x 3 + 4) = 20. We let σ 0 denote the valuation which maps each variable to its initial value. In the following, we will use p for p 1 , . . . , p n and d for d 1 , . . . , d n . Definition 3. We define a SMM SM = I, O, L, l 0 , X, -→ as denoting a (typically infinite-state) Mealy machine M SM = Σ I , Σ O , Q, q 0 , δ, λ , where -Σ I is obtained from I as described when introducing actions, and similarly for Σ O , -Q is the set of pairs l, σ consisting of a location l ∈ L and a valuation σ, -q 0 is the pair l 0 , σ 0 , and δ and λ are such that for any symbolic transition in -→ of form i l i l ′ -α(p) when g / x 1 , . . . , x k := e 1 , . . . , e k ; β(e out 1 , . . . , e out m )

for any valuation σ and data values d such that σ(g[d/p]) is true (i.e., under the valuation σ, the guard g is evaluated to true when the formal parameters p are replaced by the received data values d), it holds that

• δ( l, σ , α(d)) = l ′ , σ ′ , where σ ′ is the valuation such that * σ ′ (x i ) = σ(e i [d/p]) for 1 ≤ i ≤ k, and * σ ′ (x) = σ(x) if x is not among x 1 , . . . , x k , • λ( l, σ , α(d)) = β(σ ′ (e out 1 [d/p]), . . . , σ ′ (e out m [d/p])). ⊓ ⊔
Here the four last lines say that the state is updated to a new pair l ′ , σ ′ , where l ′ is the target location of the symbolic transition and σ ′ is obtained by performing the multiple assignment x 1 , . . . , x k := e 1 , . . . , e k simultaneously to all variables that are among x 1 , . . . , x k , and that an output symbol, obtained by evaluating the expression β(e out 1 , . . . , e out m ) in σ, is generated. Having defined the meaning of an SMM through translation to an ordinary Mealy machine, we can inherit some definitions. We use λ SM to denote λ MSM , and say that SM and SM ′ are equivalent if λ SM (u) = λ SM ′ (u) for all input words u. We can similarly say that an SMM is equivalent to a Mealy machine.

Symbolic Mealy machines are required to be deterministic, just like ordinary Mealy machines. We say that SM is deterministic if M SM is deterministic: a sufficient condition under which M SM , is deterministic is that for each input action α ∈ I, each location l ∈ L, and each valuation σ, the set -→ contains exactly one symbolic transition such that σ(g[d/p]) is true.

Example 1. Model a simple booking system

Inference Using Abstraction

Let us consider the problem of extending finite-state automata learning (as realized. e.g., by th L * alglorithm) to the learning of infinite state automata, as represented by Symbolic Mealy machines. More precisely, given a SUT, whose behavior can be modeled as an SMM SM, we should describe how a component, called the Learner, which communicates with the SUT, can infer an SMM equivalent to SM by query learning. In this setup, the Learner initially knows the static interface of SM, i.e., the sets I and O of input and output actions together with their arities. It may then ask a sequence of membership queries; each one supplying a chosen input word u ∈ (Σ I ) * and observing the response λ SM (u). After a "sufficient" number of membership membership queries the Learner can build a "stable" hypothesis H from the obtained information. The hypothesis H should of course agree with SM on the performed membership queries (i.e., λ SM (u) = λ H (u) whenever u was supplied in a membership query), but must make suitable generalizations for other input words.

The L * algorithm is designed for finite-state Mealy machines and cannot construct infinite-state models. In order to use it for inferring models of large or infinite-state SMMs, we must somehow transform the behavior of an SMM so that it becomes the behavior of some finite-state Mealy machine. In this section, we present an approach, which has been elaborated in the work by Aarts, Jonsson, Uijen, and Vaandrager [START_REF] Aarts | Generating models of infinite-state communication protocols using regular inference with abstraction[END_REF][START_REF] Aarts | Inference and abstraction of the biometric passport[END_REF]. The approach adapts ideas from predicate abstraction [START_REF] Loiseaux | Property preserving abstractions for the verification of concurrent systems[END_REF][START_REF] Clarke | Counterexampleguided abstraction refinement for symbolic model checking[END_REF], which has been successful for extending finite-state model checking to large and infinite state spaces.

In order to introduce our ideas, consider an SMM SM = I, O, L, l 0 , X, -→ for which the sets Σ I and Σ O of input and output symbols, and the set of valuations of X may be large or even infinite. To apply regular inference to SM, we here propose to define an abstraction from Σ I and Σ O to (small) finite sets of abstract input and output symbols. The overall idea can be schematically depicted as in Figure 3. The abstraction A interacts with the SUT using the alphabets Σ I and Σ O ; it interacts with the Learner using finite alphabets of If A is suitable defined, it can also the (possibly) infinite-state behavior of SUT into a behavior which can be represented by a finite-state Mealy machine. The Learner can then use standard techniques to learn this Mealy machine. Having done this, we can finally "reverse" the effect of the abstraction A to obtain an SMM which is equivalent to the original SUT.

As a concrete example, in the SMM in our running example, symbols of form getSeats(s) in which the parameter s belongs to the large domain of session identifiers, can be abstracted to symbols of form getSeats(S), where S is a value from a small domain. A natural choice for such a small domain could be the set {CUR, BAD}, where the value CUR denotes that s is the "current" session identifier (supplied in the relevant openSession interaction), and the value BAD denotes that s has some other value. Thus, the abstraction of a symbol, such as getSeats(s), in general depends on the previous history of symbols. In model checking using abstraction [START_REF] Loiseaux | Property preserving abstractions for the verification of concurrent systems[END_REF][START_REF] Clarke | Counterexampleguided abstraction refinement for symbolic model checking[END_REF], this dependency is taken into account by letting the abstraction depend on internal state variables. For instance, the SUT may have a state variable to remember the "current" session identifier; a predicate abstraction will then only represent whether this internal state variable is equal to the session identifier that is received in the input symbol that is being processed. However, automata learning is performed in a black-box setting where the state variables of the SMM are not accessible. Therefore, these state variables must be recreated in the the abstraction, and be updated to record relevant history information. In our example, the recreated state variables can be cur session and cur seats, where cur session is assigned the session identifier supplied to the SUT in the relevant openSession interaction, and cur seats is returned by the SUT in response to the relevant getSeats interaction. Typically, these additional state variables must be defined by a user who has some insight into the functioning of the SUT. In general, this is a nontrivial task, but in Section 7 we discuss approaches for systematically constructing abstractions for situations where the operation on data is not overly complex.

We can define an abstraction formally as follows. Intuitively, an abstraction A maps input and output symbols of the SUT to abstract input and output symbols, and updates its local state immediately after the occurrence of each symbol. Let us, as was done for Mealy machines, extend the definitions of the abstraction functions to sequences of input and output symbols. We will use u to range over sequences of input symbols, v to range over sequences of output symbols, and w to range over sequences of pairs (of form a/b) of input and output symbols. Since a Mealy machine interacts with both an input symbol and an output symbol at each transition, we extend the definitions of δ R , abstr I , and abstr O by defining:

δ R (r, a/b) = δ R (δ R (r, a), b) abstr(r, a/b) = abstr I (r, a)/abstr O (δ R (r, a), b)
where a/b is a pair of input and output symbol, and abstr maps pairs of input and output symbols to corresponding abstract ones. In the last formula, the abstraction of the input symbol a is performed in the local state r, and the abstraction of the output symbol b is performed wrp. to the local state δ R (r, a) reached after having processed the input symbol a.

We thereafter extend δ R to sequences of pairs of input and output symbols, by δ R (r, ε) = r δ R (r, w a/b) = δ R (δ R (r, w), a/b)

We can similarly extend the mapping abstr from pairs of input and output symbols to sequences of such pairs. abstr(r, ε) = ε abstr(r, w a/b) = abstr(r, w) abstr(δ R (r, w), a/b) ,

In particular, abstr(r 0 , w) is the abstraction of an arbitrary sequence w of inputoutput pairs.

In a concrete setup for learning a model of the SUT, we envisage that the abstraction is performed by introducing a Mapper module between the Learner and the SUT, which carries out the transformations of the abstraction. The Learner can then interact with the combination of the Mapper and the SUT, using the finite sets Σ A I and Σ A O , whereas the Mapper and the SUT interact using the alphabets Σ I and Σ O . The Mapper maintains the local state r of the abstraction. Note that the Mapper must transform between original and abstract symbols in two different directions, depending on whether the symbol is an input or output symbol. Each abstract input symbol a A supplied by the Learner is translated by the Mapper to a concrete input symbol a such that a A = abstr I (r, a), and sent to the SUT, while also updating the local state r to δ R (r, a). The corresponding reply b by SUT is translated to the abstract symbol abstr O (δ R (r, a), b) and sent back to the Learner. Finally the local state r is updated to δ R (r, a/b).

An example of a possible round of exchanged symbols is depicted in Figure 4. In this round, the abstract symbol openSession(USR, OK) is received by the Mapper. Here the combination USR, OK represents a valid combination of user and password. The Mapper chooses appropriate concrete data values as parameters, including to choose a session identifier to create an input symbol for the SUT. It also stores the chosen session identifier into a local variable. The SUT recognizes the input symbol as a valid start of a session, and so acknowledges this by returning the provided session identifier. The Mapper compares the session identifier returned with its stored local variable containing the session identifier in the preceding input symbol, finds out that they are equal, and therefore transforms 42 into the abstract symbol CUR, representing "current session identifier". Example Let us suggest an abstraction that could be applied in order to learn a model of the seat booking service. In Section 4, we already described the domains and predicates for modeling data parameters. Let us first suggest a representation of the local state of the abstraction. This can be represented by two state variables:

cur session which stores the value of the "current" session, and and cur seats which stores the set of seats that has been proposed by the service.

The initial values of both variables is ⊥ (undefined). Thus, a state of the abstraction is a valuation ρ which maps cur session and cur seats to values. Initially, ρ maps these variables to the undefined value. Let us then define the set of abstract input symbols and the state-dependent mapping abstr I from input symbols of the service to abstract input symbols. The abstraction of an input symbol depends on whether certain guards, that may be evaluated when such an input symbol is received, hold. For each combination of input symbol and applicable guard, we create a suitable abstract input symbol. In Table 1, we show the different combinations of input symbols and guards, and the corresponding abstract input symbols. For instance, if Let us next define the set of abstract output symbols and the mapping abstr O . As described in Section 4, the set of output symbols correspond to data values in domains SESSION, SEATS, and SEAT. In addition, there is an output symbol error which is returned on input that does not make the current session progress. These output symbols are mapped to abstract output symbols as follows.

-Data values in SESSION are mapped to CUR or BAD, depending on whether they are equal to cur session or not. -Data values in SEATS are mapped to OFFERED or NOT OFFERED, depending on whether they are equal to the set of seats offered by the service. Here, we have performed a modeling trick in order to be able to model the service as a (deterministic) Mealy machine, in spite of the fact that the set of seats it may return cannot be predicted from the past sequence of input and output symbol. In order not to have to model the return of a set of seats using nondeterminism, we invent a constant, named offered (say), which represents the set of seats offered by the service in the session considered. -Data values in SEAT are mapped to SEAT or NO SEAT, depending on whether the seat is a member of the set cur seats or not. -The output symbol error is left unchanged by the abstraction.

Let us finally consider how the state of the abstraction is updated on the occurrence of an input or output symbol. This state is unchanged, except for the following cases.

-When an input symbol of form openSession(u, p, s) is received, such that has passwd(u, p) and when cur session is previously undefined, then cur session is assigned the value s received in the input symbol.

-When an output symbol in domain SEATS is produced in a situation where cur seats is previously undefined, then cur seats is assigned the value of the output symbol.

⊓ ⊔

In order to better understand what behavior is obtained by wrapping the SUT with the Mapper, and which is observed by the Learner, let us model the behavior of the combination of the Mapper and SUT, which we denote by A SM . Unfortunately, A SM cannot in general be modeled as a (deterministic) Mealy machine. The reason is that each (abstract) input symbol a A can be translated by the Mapper (in state r) to any input symbol a with a A = abstr I (r, a): different choices of a will, in general, cause the SUT to move to different states and subsequently cause different (abstract) output symbols to be generated. In addition, the Mapper should have a defined reaction for the case that there is no input symbol a with a A = abstr I (r, a). We therefore need to introduce a generalization of Mealy machines that allows nondeterminism, and represent the behavior of A SM as a nondeterministic Mealy machine. A nondeterministic Mealy machine differs from a Mealy machine as defined in Definition 1 in that the reception of an input symbol can result in several possible combinations of output symbols and next states. For this situation, it is more suitable to use only the notation q a/b -→ q ′ to denote that when the machine is in state q and receives input symbol a, a possible reaction is to emit output symbol b and move to state

q ′ . Let M SM = Σ I , Σ O , Q, q 0 , δ, λ denote the Mealy machine model of SM, let (Σ A O ) ⊤ = Σ A O ∪ {⊤} and R ⊤ = R ∪ {r ⊤ },
where ⊤ is an output symbol denoting that the provided abstract input symbol cannot be translated by the Mapper. Then the behavior of A SM can be modeled as a nondeterministic Mealy machine in which -Σ A I and (Σ A O ) ⊤ are the sets of input and output symbols, -Q × R ⊤ is the set of states, -q 0 , r 0 is the initial state, and whenever A SM is in state q, r and receives an abstract input symbol a A , then for any concrete input symbol a such that a A = abstr I (r, a)

• the state q, r can be updated to δ(q, a), δ R (r, a/b) , where b = λ(q, a) is the output symbol returned by SM, and • the abstract output symbol abstr O (δ R (r, a), b) can be produced. We denote this possible symbol exchnage by q, r abstrI (r,a)/abstrO(δ R (r,a),λ(q,a)) -→ δ(q, a), δ R (r, a/λ(q, a)) .

For the case where there is no concrete input symbol a such that a A = abstr I (r, a), the output symbol ⊤ is produced and the state q, r is updated to r ⊤ , where it remains, i.e.,

• q, r a A /⊤ -→ q, r ⊤ , and

• q, r ⊤ a A /⊤ -→ q, r ⊤ for any a A ∈ Σ A I .
Although the behavior of A SM must, in general, be modeled as a Mealy machine, which is internally nondeterministic, it is still possible that its external behavior will appear to the Learner as being deterministic. The Learner can only observe the sequences of abstract output symbols that are produced in response to provided input sequences. So, for a sequence

a A 1 • • • a A n of abstract input sym- bols, define λ A SM ( q, r , a A 1 • • • a A n ) as the set of sequences of output symbols of form b A 1 • • • b A n such that for some sequence of states q 1 , r 1 • • • q n , r n we have q, r a A 1 /b A 1 -→ q 1 , r 1 a A 2 /b A 2 -→ • • • a A n co/b A n -→ q n , r n Intuitively, λ A SM ( q, r , a A 1 • • • a A n )
is the set of abstract output sequences that may be generated by A SM in response to a A 1 • • • a A n , starting from state q, r . In particular, λ A SM ( q 0 , r 0 , u) is the set of sequences that may result from the input sequence u.

If tha input-output behavior of A SM is equivalent to that of a deterministic Mealy machine, and if this (deterministic) Mealy machine is finite-state, it will be possible to use L * for learning a model of its external behavior. Indeed, a well-designed abstraction will preserve the determinism of the SUT so that the input-output behavior of A SM behaves deterministically, i.e., each sequence of supplied (abstract) input symbols uniquely determines the subsequently produced (abstract) output symbol.

We make a formal definition of the condition under which the abstraction will present a deterministic view to the Learner. Definition 5. Let SM = I, O, L, l 0 , X, -→ be an SMM, and let A = Σ A I , Σ A O , R, r 0 , abstr I , abstr O , δ R be an I, O -abstraction. Then A is adequate for SM if for any sequence u ∈ (Σ A I ) * of abstract input symbols, the set λ A SM ( q 0 , r 0 , u) of correspondingly generated output sequences has at most one element.

⊓ ⊔

Intuitively, adequacy means that A SM exhibits a deterministic mapping from sequences of abstract input symbols received by the Mapper to sequences of abstract output symbols produced by the Mapper after abstracting the output of the SUT. If A is adequate for SM, then the Learner will perceive that A SM is equivalent to a (deterministic) Mealy machine (which may or may not be finitestate). For any deterministic mapping from sequences of abstract input symbols to sequences of abstract output symbols, there is a minimal Mealy machine which generates it. This Mealy machine can be defined by a Nerode-like quotient construction, as follows. Let Q SM,A denote the set of states of A SM that are reachable. More precisely, Q SM,A is the smallest subset of Q × R which includes q 0 , r 0 and such that q, r ∈ Q SM,A implies δ(q, a), δ R (r, a/λ(q, a) ∈ Q SM,A for all a ∈ Σ I ). Note that we have excluded states where the Mapper has reached r ⊤ .

Define the equivalence ≃ on Q SM,A by q, r ≃ q ′ , r ′ if λ A SM ( q, r , u) = λ A SM ( q ′ , r ′ , u) for any sequence of abstract input symbols u ∈ (Σ A I ) * . Intuitively, two elements of Q SM,A are equivalent if they cannot be distinguished by the Learner, i.e., any two subsequent sequences of input symbols that are identified by abstr I trigger two subsequent output words that are identified by abstr O .

If A is adequate for SM, then the input-output behavior of A SM is equal to that of a deterministic Mealy machine M A (in the sense that λ A SM ( q 0 , r 0 , u) = {λ M A (u)} for any sequence u ∈ (Σ A I ) * of abstract input symbols), which is defined by

M A = Σ A I , Σ A O , Q A , q A 0 , δ A , λ A , where -Q A = Q SM,A / ≃ ∪{q ⊤ }, i.e.
, the set of states is the set of equivalence classes under ≃ plus an extra state q ⊤ denoting that an abstract input symbol with no corresponding concrete input symbol has been received, -q A 0 = [ q 0 , r 0 ] ≃ is the equivalence class of the initial state of A SM , -δ A and λ A are defined as follows:

for any a ∈ Σ I with abstr I (r, a) = a A we have • δ A ([ q, r ] ≃ , a A ) = [ δ(q, a), δ R (r, a/λ(q, a)) ] ≃ , and

• λ A ([ q, r ] ≃ , a A ) = abstr O (δ R (r, a), λ(q, for any a A ∈ Σ A I s.t.
there is no a ∈ Σ I with abstr I (r, a) = a A we have

• λ A ([ q, r ] ≃ , a A ) = ⊤, and • δ A ([ q, r ] ≃ , a A ) = q ⊤ .
To complete the definition, we define δ A (q ⊤ , a A ) = q ⊤ for any a A ∈ Σ A I .

The definition of ≃ can be used to show that M A is well-defined.

The Mealy machine M A may be finite-or infinite-state. If a finite-state Mealy machine

M A = Σ A I , Σ A O , Q A , q A 0 , δ A , λ
A is produced by the Learner, then we must finally "reverse" the effect of the abstraction A to obtain the original SMM SM, such that A SM is equivalent to M A . In general, there can of course be many SMMs with this property. In order that the SMMs be determined uniquely up to equivalence (which is anyway the best we can hope for), it is necessary that each abstract output symbol correspond to a uniquely determined concrete output symbol generated by the SMM. We formulate this as follows. ⊓ ⊔

Intuitively, this means that we can deduce which output symbol is produced by SM by seeing only its abstraction. If A is unambiguous, and

M A = Σ A I , Σ A O , Q A , q A 0 , δ A , λ
A is a finite-state mealy machine, define A -1 M A as be the Mealy machine Σ I , Σ O , Q A × R, q A 0 , r 0 , δ, λ , where δ and λ are defined by λ( q A , r , a) = b, where b the unique output symbol such that λ A (q A , abstr I (r, a)) = abstr O (δ R (r, a), b), and δ( q A , r , a) = δ A (q A , abstr I (r, a)), δ R (r, a/b) .

We can now prove that under the conditions we have introduced, the SUT can be inferred from M A , of course up to equivalence. Proposition 1. If A is unambiguous and adequate for SM, and if A SM is equivalent to M A (i.e., λ A SM ( q 0 , r 0

, u) = {λ M A (u)} for any u ∈ (Σ A I ) * ), then SM is equivalent to A -1 M A . ⊓ ⊔
The proposition can be proven by establishing that A -1 M A satisfies the conditions of the propsition, i.e., that A A -1 M A is equivalent to M A , and by establishing (e.g., by induction on the length of u) that the ouput generated in response to an input sequence u, by any SM such that A SM is equivalent to M A , is uniquely determined.

Illustrating Example

In this section, we sketch how a model of the booking service could be obtained by combining automata learning, and the abstraction that was developed in the course of the two previous sections.

Having supplied the abstraction described in the previous section, we can now employ the L * algorithm to learn a finite-state Mealy machine, which interacts using the sets Σ A I and Σ A O of symbols. Assume that the result is as described by the finite-state Mealy machine in Figure 5. In this figure, we have omitted all transitions that return error, and concentrate on those that make the session progress. Starting from the finite-state Mealy machine in Figure 5, we can apply the construction described at the end of the preceding section to generate a possible SMM that models the service. It is shown in Figure 6. ? l0 X X X X X X X X X X X X X X X X X X X X X X X z openSession(u, p, s) when has passwd(u, p)/ cur session := s; s l1 9 getSeats(s) when s = cur session/ seatsvar := offered; offered l2 X X X X X X X X X X X X X X X X X X X X X X X z getSeat(s, seat) when s = cur session ∧ seat ∈ cur seats/seat l3 Fig. 6. Constructed Symbolic Mealy machine (self-loops suppressed)

?

l0 X X X X X X X X X X X X X X X X X X X X X X X z openSession(USR, OK)/CUR l1 9 getSeats(CUR)/OFFERED l2 X X X X X X X X X X X X X X X X X X X X X X X z getSeat(CUR, SEAT)/SEAT l3

Systematic Construction of Abstractions

The construction of a suitable abstraction is crucial for successful inference of an SMM SM. In this subsection, we discuss how a successful abstraction can be constructued more systematically. A necessary prerequisite for constructing an abstraction is obviously that the sets I and O of input and output actions of SM, together with their arities, are known a priori.

Furthermore, it appears necessary to have some a priori knowledge about how SM stores and manipulates data that it receives and emits. On the other hand, the control aspects of SM can be inferred by the Learner using automata learning, provided that the abstraction is "good enough". In the following, we give some sufficient criteria for "good enough" abstractions, under which learning and SM, according to the technique described in Section 5 can be successful. At the end of this section, we discuss how such knowledge can sometimes be obtained by testing and experimentation on SM.

In the running example in the previous subsection, we see that the abstraction mapping for input symbols uses expressions that become guards in the resulting SMM, and that the abstraction mapping for output symbols uses expressions that occur in output expressions of the SMM. When SM is only available as a black box, such an abstraction can be produced if the following information is available.

-An "overestimate" of the information that is stored in state variables of SM.

More precisely, such an overestimate can be represented by a set R of states of the abstraction and an update function δ R such that after any sequence of pairs of input and output symbols, the information in the "data state", represented by the current valuation σ of state variables, of SM can be obtained from the current state r of the abstraction. One way to formalize is by finding a mapping h from the set of valuations of the state variables X to the set r of states of the Mapper, which has the properties that • h(σ 0 ) = r 0 , and ). This can be achieved by letting each possible guard correspond to a different abstract input symbol. For the case that the abstraction is not fine enough to distinguish between symbolic transitions that cause different output, a technique for refining the abstraction on-the-fly, during the learning process, has been developed by Howar, Steffen, and Merten [START_REF] Howar | Automata learning with automated alphabet abstraction refinement[END_REF]. -The abstraction should be unambiguous. This can be achieved if different output expressions are mapped to different abstract output symbols. For instance, one could let abstract output symbols "be" the output expressions that can occur in symbolic transitions, assuming that an output expression is uniquely obtainable from the actual output symbol produced.

•
Under the above assumptions, we can construct an abstraction which maps combinations of parameterized input actions and guards in a possibe SMM to abstract input symbols, and maps combinations of expressions in output symbols of a possible SMM to abstract output symbols, as in the running example. The updates to state variables will simply consist in assigning some input parameters to state variables: the problem here is to decide which input parameters will influence the future behavior of SM, and must be remembered in state variables. In our experiments, we have made this decision based on observing the response of SM to selected input strings, i.e., by posing membership queries, and saving those parameter values that are used to produce future output. For parameter values on which the only performed operation is a test for equality, such as the id parameter of the running example, we have made these ideas more precise in our earlier work [START_REF] Berg | Regular inference for state machines using domains with equality tests[END_REF], as follows:

Consider an input string u, which contains a parameter value d. We observe the output of M in response to u and to selected continuations of u, and decide to store d in a state variable if there is some continuation v of u such that d is used to produce the response to v. More precisely, this happens if there is a fresh (i.e., previously unused) data value d ′ such that the response λ(δ(q 0 , u), v) to v and the response λ(δ(q 0 , u), v[d ′ /d]) to v[d ′ /d] (i.e., v where all occurrences of d have been replaced by d ′ ) satisfy λ(δ(q 0 , u), v)[d ′ /d] = λ(δ(q 0 , u), v[d ′ /d]), i.e., SM does not treat d in the same way as a fresh (previously unused) value d ′ . This happens, e.g., if λ(δ(q 0 , u), v[d ′ /d]) contains the data value d implying that d must have been remembered before seeing the subsequent input v[d ′ /d], and that d should be stored in a state variable.

Conclusions and Future Work

We have considered the problem of extending automata learning to incorporate data parameters, including their influence on control behavior. We concentrated on presenting an approach that adapts ideas using abstraction that have been successfully applied in formal verification. This approach has been used on some nontrivial examples [START_REF] Aarts | Generating models of infinite-state communication protocols using regular inference with abstraction[END_REF][START_REF] Aarts | Inference and abstraction of the biometric passport[END_REF], and techniques for revising abstractions by need have been developed [START_REF] Howar | Automata learning with automated alphabet abstraction refinement[END_REF]. However, it is clear that much work remains in order to make automata learning with data easily applicable to a wide class of systems. Issues that need to be addressed include to remove (some of) the need for manual construction of abstractions: this could be addressed by developing more canonical models for automata with data. Another issue is that the determinism of the Mealy machine model is limiting the modeling power: ways should be found to effectively learn nondeterministic models.

Fig. 2 .

 2 Fig.2. A Mealy machine ΣI, ΣO, Q, q0, δ, λ with states Q = {q1, q2, q3, q4}, input alphabet ΣI = {a, b}, and output alphabet ΣO = {0, 1, 2, 3}. For instance, applying a starting in q0 produces output λ(q0, a) = 1 and moves to next state δ(q0, a) = q1.

Fig. 3 .

 3 Fig. 3. Introducing an abstraction A between the SUT and the Learner

Definition 4 .

 4 Let I and O be disjoint finite sets of (input and output) actions. An I, O -abstraction is a tuple A = Σ A I , Σ A O , R, r 0 , abstr I , abstr O , δ R , where -Σ A I and Σ A O are finite sets of abstract input and output symbols, -R is a (possibly infinite) set of local states, -r 0 ∈ R is an initial local state, -abstr I : R × Σ I → Σ A I maps input symbols of the SUT to abstract input symbols, -abstr O : R × Σ O → Σ A O maps output symbols of the SUT to abstract output symbols, and δ R : R × (Σ I ∪ Σ O ) → R updates the local state when a new input or output symbol occurs. ⊓ ⊔

Fig. 4 .

 4 Fig. 4. Introduction of Mapper module

Definition 6 .

 6 An I, O -abstraction A = Σ A I , Σ A O , R, r 0 , abstr I , abstr O , δ R is unambiguous if for all abstract output symbols b A and all r ∈ R there is at most one output symbol b such that b A = abstr O (δ R (r, a), b) for some input symbol a ∈ Σ I .

Fig. 5 .

 5 Fig. 5. Learned Abstract Mealy machine (self-loops suppressed)

  for any symbolic transition in -→ of form i l i l ′ -α(p) when g / x 1 , . . . , x k := e 1 , . . . , e k ; β(e out 1 , . . . , e out m )and valuation σ and data values d such that σ(g[d/p]) evaluates to true, then if h(σ) = r, then it holds that for σ ′ defined by* σ ′ (x i ) = σ(e i [d/p]) for 1 ≤ i ≤ k, and * σ ′ (x) = σ(x) if x is not among x 1 , . . . , x k , we have h(σ ′ ) = δ R (r, α(d)/β(σ ′ (e out 1 [d/p]), . . . , σ ′ (e out m [d/p]))).-The abstraction should distinguish between the different symbolic transitions from a location. More precisely, this means that if from a location and from some state l, σ with h(σ) = r, there are two different symbolic transitions taken for input α(d) and α ′ (d ′ ), then abstr I (r, α(d)) = abstr I (r, α ′ (d ′ )

Table 1 .

 1 Mapping from combinations of input symbols and guards to abstract input symbols

	input	guard	abstract symbol
	openSession(u, p, s) has passwd(u, p)	openSession(USR, OK)
		¬has passwd(u, p)	openSession(USR, NOK)
	getSeats(s)	s = cur session	getSeats(CUR)
		s = cur session	getSeats(BAD)
	getSeat(s, seat)

s = cur session ∧ seat ∈ cur seats getSeat(CUR, SEAT) s = cur session ∧ seat ∈ cur seats getSeat(CUR, NO SEAT) s = cur session ∧ seat ∈ cur seats getSeat(BAD, SEAT) s = cur session ∧ seat ∈ cur seats getSeat(BAD, NO SEAT) ρ(cur session) = 42, and ρ(cur seats) = {C, D, G}, then abstr I (ρ, getSeat(42, F )) is getSeat(CUR, NO SEAT).


Yuxin Deng

Stéphane Grumbach

Jean-François Monin

A Framework for Verifying Data-Centric Protocols

Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They simplify greatly the code, which is orders of magnitude shorter, much more declarative, while still admitting efficient distributed execution. We show that they also provide a promising approach to the verification of distributed protocols, thanks to their data centric orientation, which allows to explicitly handle global structures, such as the topology of the network, routing tables, trees, etc, as well as their properties. We consider a framework using an original formalization in the Coq proof assistant of a distributed computation model based on message passing with either synchronous or asynchronous behavior. The declarative rules of the Netlog language for specifying distributed protocols, as well as the virtual machines for evaluating these rules, are encoded in Coq as well. We consider as a case study tree protocols, and show how this framework enables us to formally verify them in both the asynchronous and synchronous setting.

Introduction

Up to now, most efforts to formalize protocols or distributed algorithms and automate their verification relied on control-oriented paradigms. It is the case for instance of the "Formal Description Techniques" developed by telecom labs at the beginning of the 1980s in order to specify and verify protocols to be standardized at ITU and ISO. Two of the languages developed, Estelle and SDL, are based on asynchronous communicating automata, while LOTOS is a process algebra based on CCS and CSP extended with algebraic data types [START_REF] Turner | Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL[END_REF]. Several verification tools, ranging from simulation to model checking, have been developed and applied to different case studies [START_REF] Wu | Translation from LOTOS and Estelle Specifications to Extended Transition System and its Verification[END_REF][START_REF] Kirkwood | Experiences with specification and verification in LOTOS: a report on two case studies[END_REF][START_REF] Törö | SDL specification and verification of universal personal computing: with Object GEODE[END_REF][START_REF] Zhang | Applying SDL Specifications and Tools to the Verification of Procedures[END_REF][START_REF] Regensburger | Formal Verification of SDL Systems at the Siemens Mobile Phone Department[END_REF][START_REF] Shahrier | SDL Specification and Verification of a Distributed Access Generic opticalNetwork Interface for SMDS Networks[END_REF][START_REF] Jard | Development of Veda, a Prototyping Tool for Distributed Algorithms[END_REF][START_REF] Fernandez | A toolbox for the verification of LOTOS programs[END_REF][START_REF] Gotzhein | Formal Description Techniques IX: Theory, application and tools[END_REF].

For the verification of communication protocols based on process algebras, the idea has been to model both the implementation and the specification of a protocol as processes in a process algebra, and then to use automatic tools to check whether the former is a refinement of the latter or if they are behaviorally equivalent [START_REF] Cleaveland | The Concurrency Workbench: A semantics-based tool for the verification of concurrency systems[END_REF][START_REF] Roscoe | Model-checking CSP[END_REF]. Examples include the Concurrency Workbench [START_REF] Cleaveland | The Concurrency Workbench: A semantics-based tool for the verification of concurrency systems[END_REF], which is a verification tool based on CCS, FDR [START_REF] Roscoe | Model-checking CSP[END_REF] which is based on CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], ProVerif [START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF] which is based on the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Other approaches include input/output automata [START_REF] Lynch | An introduction to input/output automata[END_REF], or Unity and TLA, which combine temporal logic and transition-based specification [START_REF] Chandy | Parallel program design: a foundation[END_REF][START_REF] Lamport | The temporal logic of actions[END_REF], and may rely as well on proof assistant technology [START_REF] Paulson | Mechanizing UNITY in Isabelle[END_REF][START_REF] Heyd | A Modular Coding of UNITY in COQ[END_REF][START_REF] Chetali | Formal Verification of Concurrent Programs Using the Larch Prover[END_REF][START_REF] Långbacka | A HOL Formalisation of the Temporal Logic of Actions[END_REF].

The common feature of all these approaches is their focus on control, in particular on how to deal with behaviors in a distributed framework. Typical issues include non-determinism, deadlock freedom, stuttering, fairness, distributed consensus and, more recently, mobility. Data is generally considered as an abstract object not really related to the behavior. If this is relevant for many low-level protocols, such as transport protocols, it does not suit the needs of applications which aim at building up distributed global information, such as topological information on the network (in a physical or a virtual sense), e.g. routing tables. Such protocols are qualified as data-centric in the sequel. Correctness proofs of data-centric protocols are even more complex than those for control-centric protocols.

Data-centric rule-based languages have been recently proposed to program network protocols and distributed applications [START_REF] Loo | Declarative routing: extensible routing with declarative queries[END_REF][START_REF] Loo | Declarative networking: language, execution and optimization[END_REF][START_REF] Liu | A declarative perspective on adaptive manet routing[END_REF]. This approach benefits from reasonably efficient implementations, by using methods developed in the field of databases for recursive languages à la Datalog. Programs are expressed at a very high level, typically two orders of magnitude shorter than code written in usual imperative languages.

Our claim is that this framework is promising not only for the design of distributed algorithms, but for their verification as well. Up to now, only a few partial results have been demonstrated. In [START_REF] Wang | Declarative Network Verification[END_REF], a declarative network verifier (DNV) was presented. Specifications written in the Network Datalog query language are mapped into logical axioms, which can be used in theorem provers like PVS to validate protocol correctness. The reasoning based on DNV is for Datalog specifications of (eventually distributed) algorithms, but not for distributed versions of Datalog such as the one proposed in this paper. In other words, only the highly abstract centralized behaviour of a network is considered. Therefore, deep subtleties on message passing, derivation of local facts and their relationship with the intended global behaviour are absent in [START_REF] Wang | Declarative Network Verification[END_REF].

In the present paper, we go one essential step further. We show that it is indeed feasible to reason about the distributed behaviour of individual nodes which together yield some expected global behaviour of the whole network. We consider the Netlog language [START_REF] Grumbach | Netlog, a Rule-Based Language for Distributed Programming[END_REF], which relies on deductive rules of the form head ← body, which are installed on each node of the distributed system. The rules allow to derive new facts of the form "head", if their body is satisfied locally on the node. The facts derived might then be stored locally on the node or sent to other nodes in the network depending upon the rule.

Netlog admits a fixpoint semantics which interleaves local computation on the nodes and communication between neighboring nodes. On each node, a local round consists of a computation phase followed by a communication phase. During the computation phase, the program updates the local data and produces messages to be sent. During the communication phase, messages are transmitted and become available to the destination node.

Our objective is to develop a framework to formally verify properties of Netlog programs. As to formal verification, there are roughly two kinds of approaches: model checking and theorem proving. Model checking explores the state space of a system model exhaustively to see if a desirable property is satisfied. It is largely automated and generates a counterexample if the property does not hold. The state explosion problem limits the potential of model checkers for large systems. The basic idea of theorem proving is to translate a system's specification into a mathematical theory and then construct a proof of a theorem by generating the intermediate proof steps. Theorem proving can deal with large or even infinite state spaces by using proof principles such as induction and co-induction.

We use the proof assistant, Coq, which is an interactive theorem prover, in which high level proof search commands construct formal proofs behind the scene, which are then mechanically verified. Coq has been successfully applied to ensure reliability of hardware and software systems in various fields, such as multiplier circuits [START_REF] Paulin-Mohring | Circuits as Streams in Coq: Verification of a Sequential Multiplier[END_REF], concurrent communication protocols [START_REF] Giménez | A Calculus of Infinite Constructions and its application to the verification of communicating systems[END_REF], self-stabilizing population protocols [START_REF] Deng | Verifying Self-stabilizing Population Protocols with Coq[END_REF], devices for broadband protocols [START_REF] Monin | Proving a real time algorithm for ATM in Coq[END_REF], and compilers [START_REF] Leroy | Formal certification of a compiler back-end or: programming a compiler with a proof assistant[END_REF], to name a few.

We develop a Coq library necessary for our purposes, including (i) the formalization of the distributed system; (ii) the modeling of the embedded machine evaluating the Netlog programs; (iii) the translation of the Netlog programs; as well as (iv) a formalization of graphs and trees suitable to our needs.

As a proof of concept, we experimented the proposed framework on concrete protocols for constructing spanning trees over connected graphs. Such protocols have been shown to be correct on theoretical models. This is the case for instance of the well-known distributed algorithm for computing a minimum-weight spanning tree due to Gallager, Humblet and Spira [START_REF] Gallager | A Distributed Algorithm for Minimum-Weight Spanning Trees[END_REF]. The rigorous proofs made between 1987 and 2006 [START_REF] Welch | A lattice-structured proof of a minimum spanning[END_REF][START_REF] Hesselink | The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract[END_REF][START_REF] Moses | A New Proof of the GHS Minimum Spanning Tree Algorithm[END_REF] are all intricate and very long (100 to 170 pages). Only [START_REF] Hesselink | The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract[END_REF] has been mechanically proof-checked.

Our objective is to carry on proofs for protocols written in a programming language (Netlog) which is implemented and runs on real distributed systems, and not only in theoretical models, and to concentrate on a data-centric approach. The protocols proceed in rounds, where one node (in the asynchronous model) or all nodes (in the synchronous model) perform some local computation, update their local data and then exchange data with their neighbors before entering the next round.

We have proven an initial simple protocol for defining spanning trees. Furthermore, in the synchronous message passing model, we show that we obtain a distributed version of the classical breadth-first search (BFS) algorithm. To show its correctness, the crucial ingredient is to formally prove the validity of the invariant that states the relationship between the centralized and the distributed version of the protocol, as well as the propagation of information on the distributed version. This is non trivial and requires modeling how distributed tasks cooperate together to form the invariant. We claim that the proposed techniques establish foundations for proving more complex tree protocols such as GHS [START_REF] Gallager | A Distributed Algorithm for Minimum-Weight Spanning Trees[END_REF].

The paper is organized as follows. In Section 2, the distributed computation as formalized in Coq is presented. Section 3 is devoted to the presentation of the Netlog language. Section 4 contains the sketches of the proofs of the correctness of the tree protocol (a complete Coq script is available in [START_REF] Deng | Coq script for Netlog protocols[END_REF]).

Distributed Computation Model of Netlog

In this section we introduce a distributed computation model based on the message passing mechanism, which is suitable both for synchronous and asynchronous execution. Corresponding formal definitions in Coq can be found in [START_REF] Deng | Coq script for Netlog protocols[END_REF][START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF]. The distributed computation model described below does not depend on Netlog. In our formalization, we just assume that the states at nodes have a type local data which can evolve using simple set-theoretic operations such as union.

A distributed system relies on a communication network whose topology is given by a directed connected graph G = (V G , G), where V G is the set of nodes, and G denotes the set of communication links between nodes. For many applications, we can also assume that the graph is symmetric, that is

G(α, β) ⇔ G(β, α).
Each node has a unique identifier, Id, taken from 1, 2, • • • , n, where n is the number of nodes, and distinct local ports for distinct links incident to it. The control is fully distributed in the network, and there is no shared memory. In this high-level computation model, we abstract away detailed factors like node failures and lossy channels; if we were to formalize a more precise model, most of the data structures defined below would have to be refined.

All the nodes have the same architecture and the same behavior. Each node consists of three main components: (i) a router, handling the communication with the network; (ii) an engine, executing the local programs; and (iii) a local data store to maintain the information (data and programs) local to the node. It contains in particular the fragment of G, which relates a node to its neighbors. The router queues the incoming messages on the reception queue and the message to push produced by the engine on the emission queue.

We distinguish between computation events, performed in a node, and communication events, performed by nodes which cast their messages to their neighbors. On one node, a computation phase followed by a communication phase is called a local round of the distributed computation.

An execution is a sequence of alternating global configurations and rounds occurring on one node, in the case of an asynchronous system, or a sequence of alternating global configurations and rounds occurring simultaneously on each node, in the case of a synchronous system. In the latter case, the computation phase runs in parallel on all nodes, immediately followed by a parallel execution on all nodes of the corresponding communication phase.

The contents of node loc (the database of facts stored at loc) for a configuration cnf is denoted by |loc| cnf , or just |loc| when the configuration is clear from the context. Similarly, the set of messages arriving a node y from node x is denoted by |x→y| cnf or |x→y|. A local round at node loc relates an actual configuration pre to a new configuration mid and a list out of messages emitted from loc. Furthermore, incoming edges are cleared -intuitively, this represents the consumption of messages, once their contents has been used to elaborate mid and out. The new data d to be stored on loc is defined by a relation new stores given as a parameter, and we assume that d depends only on the data available at loc in pre, that is, |loc| pre and all the |x→loc| pre such that there is an edge from x to loc. Intuitively, the relation new stores expresses that d consists of new facts derived from facts available at loc. Similarly, out is defined by a relation new push and satisfies similar requirements. Formally, a local round is defined by the following conjunction.

local round (loc, pre, mid , out) def = =    ∃d, new stores(pre, loc, d) ∧ |loc| mid = |loc| pre ∪ d new push(pre, loc, out) ∀ x ∈ neighbors(loc), |x→loc| mid = ∅
For modeling asynchronous behaviors, we also need the notion of a trivial local round at loc, where the local data does not change and moreover incoming edges are not cleared either.

no change at(loc, pre, mid A synchronous round between two configurations pre and post is given by an intermediate configuration mid such that for all node Id loc, there exists a list of messages out such that there is a local round relating pre, mid and out on loc and a communication relating mid and out to post on loc. Now, given an arbitrary trans relation, which can be of the form sync round , or async round , or even of some alternative form, we can co-inductively define a run starting from a configuration. We have two cases: either there is a transition from configuration pre to configuration post, then any run from post yields a run from pre; or, in the opposite case, we have an empty run from pre. Altogether, a run from pre is either a finite sequence of transitions ended up with a configuration where no transition is available, or an infinite sequence of transitions, where consecutive configurations are related using trans. In order to prove properties on run, we define some temporal logic operators. In the examples considered below we need a very simple version of always, which is parametrized by a property P of configurations. In a more general setting, the parameter would be a property of runs. It is well known that a property which holds initially and is invariant is always satisfied on a run. This fact is easily proved in the very general setting provided by Coq.

) def = = |loc| mid = |loc| pre ∀ x ∈ neighbors(loc), |x→loc| mid = |x→loc|

Data Centric Protocols

In this section, we introduce the Netlog language through examples of simple protocols for defining trees. Only the main constructs of the language are presented. A more thorough presentation can be found in [START_REF] Grumbach | Netlog, a Rule-Based Language for Distributed Programming[END_REF]. Netlog relies on Datalog-like recursive rules, of the form head ← body, which allow to derive the fact "head" whenever the "body" is satisfied.

We first recall classical Datalog, whose programs run in a centralized setting over relational structures, and which allow to define invariants that will be used as well in the proofs in the distributed setting. We assume that the language contains negation as well as aggregation functions, which can be used in the head of rules to aggregate over all values satisfying the body of the rule. For instance, the function min will be used in the next example.

Let us start with the program, BFS-seq, which computes BFS trees. It runs on an instance of a graph represented by a binary relation E, and a unique node satisfying root(x). The derived relations onST , and ST , are such that onST (α) holds for a node α already on the tree, and ST (α, β) holds for an edge (α, β) already in the BFS tree.

BFS-seq in Datalog

onST (x) ← Root(x).

(1)

ST (min(x), y) onST (y) ← E(x, y); onST (x); ¬onST (y).

(

) 2
The evaluation of the program is iterated in a inflationary manner, by accumulating the results till a fixpoint, which defines its semantics, is reached. At the first step, the root node is included in the relation onST using the first rule. At the n th step, nodes at distance n -1 from the root are added in onST , and an arc of the tree is added in ST for each of them, by choosing the parent with minimal Id. The fixpoint is reached when all nodes are on the tree.

Minimum spanning trees can be defined in Datalog with arithmetic. Let us consider first the definition corresponding to Prim's algorithm [START_REF] Lynch | Distributed Algorithms[END_REF]. We assume weighted graphs, G = (V, E, ω), where the weight ω : E → R + , satisfies ω(u, v) = ω(v, u) for every edge (u, v) ∈ E. As usual, to simplify the algorithm, we assume that ω is a 1-1 mapping, so the weights of any pair of edges are distinct. Prim's algorithm starts from a (root) node, and construct successive fragments of the MST, by adding the minimal outgoing edge to the fragment at each step.

The sequential Datalog program can be written with three rules as follows. The symbol "!" denotes the consumption of the fact used in the body of the rule, which is deleted after the application of the rule.

MST-Prim-seq in Datalog

M W OE(min(m)) ← onST (x); ¬onST (y); E(x, y, m); ¬M W OE(m).

The evaluation of this program alternates two phases, (i) computation of the minimal outgoing edge's weight, MWOE, and when it is obtained, (ii) addition of the corresponding unique edge.

Let us consider now, Netlog programs, which are installed on each node, where they run concurrently. The rules of a program are applied in parallel, and the results are computed by iterating the rules over the local instance of the node, using facts either stored on the node or pushed by a neighbor. In contrast with other approaches to concurrency, the focus is not primarily on monitoring events, but data (i.e. Datalog facts) contained in nodes.

The facts deduced from rules can be stored on the node, on which the rules run, or sent to other nodes. The symbol in the head of the rules means that the result has to be either stored on the local data store (↓), sent to neighbor nodes (↑), or both ( ). The facts received on a node are used to trigger the rules, but do not get stored on that node.

The evaluation of the body of a rule is always performed on a given node. A fact is then considered to hold if and only if it occurs on this node. The negation of a fact holds if the fact does not occur on the node where the computation is performed.

The following program, which constructs a spanning tree over a distributed system, relies as above on three relation symbols: E, onST , and ST ; E represents the edge relation; and at any stage of the computation, onST (α) (respectively ST (α, β)) hold iff the node α (respectively the edge (α, β)) is already on the intended tree.

Spanning Tree Protocol in Netlog

onST (x) ← @x = 0. ( 6
)
onST (y) ↓ ST (min(x), y) ← E(x, @y); onST (x); ¬onST (y). ( 7)

Rule ( 6) runs on the unique (rrot) node, say ρ, which satisfies the relation ρ = 0. It derives a fact onST (ρ), which is stored on ρ and sent to its neighbors. Rule [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF] runs on the nodes (@y) at the border of the already computed tree. It chooses one parent (the one with minimal Id) to join the tree. Two facts are derived, which are both locally stored. The fact onST (y) is pushed to all neighbors. Each fact E(x, y) is assumed to be initially stored on node y. As no new fact E(x, y) can be derived from Rules ( 6) and ( 7), the consistency of E with the physical edge relation holds forever. This algorithm aims at constructing suitable distributed relations onST and ST . In Section 4, we will prove that they actually define a tree; moreover, in the synchronous setting they define a BFS tree. The translation of the sequential Datalog program defining a spanning tree, to a distributed program is almost trivial. It suffices to add communication instructions since the program runs locally. The translation to a distributed program is more complex for the Minimal Spanning tree protocol. Indeed, rules (4) and ( 5) are not local, and require communication between remote nodes. In a network, the root can orchestrate the distributed computation, by alternating phases of (i) computation of the MWOE by a convergecast into the current spanning tree, and (ii) addition of the new edge with minimal weight to the tree.

The next program (together with two simple rule modules for the convergecast and the edge addition) defines the minimal spanning tree in Netlog. The facts AddEdge(x, m) and GetM W OE(x) are triggering rule modules (of half a dozen rules) that perform respectively a traversal of the tree to add the edge with minimal outgoing weight, and a convergecast to obtain the new minimal outgoing weight. These rule modules (omitted for space reason) can be used in other protocols requiring non local actions. We have tested them in particular in a concurrent version of the Minimal Spanning Tree, the GHS, where there is no initial root and all nodes concurrently start building MST fragments.

Minimum Spanning Tree Protocol in Netlog

onST (x) U pM W OE(x, min(m)) GetM W OE(x) ← Root(x); E(x, y, m). (8)
↓ AddEdge(x, m) ← Root(x); !GetM W OE(x); !U pM W OE(x, m). ( 9)

↓ GetM W OE(x) ← Root(x); !AddEdge(x, m); !U pEdge(x, m). ( 10
)

Verifying Tree Protocols

We conduct the verification in two settings. In the asynchronous case, we prove that the previous protocol for spanning tree eventually constructs a spanning tree, while in the synchronous case, we prove that this protocol constructs actually a spanning tree by doing a breadth-first search in the network. We briefly sketch the first case study and then give a more detailed discussion for the second one which involves a much more difficult proof.

In both cases we expect to show that the relation ST determines a spanning tree. However, this relation is distributed on the nodes and the Netlog protocol reacts only to a locally visible part of relations ST , onST and E. The expected property is then stated in terms of the union of all ST facts available on the network.

Spanning Tree in the Asynchronous Case

We have to check that when adding a new fact ST (x, y) at some node loc then x is already on the tree while y is not yet. This is basically entailed by the body of the last rule, but additional properties are needed in order to ensure this rigorously. We use the following ones:

1. The E relation corresponds exactly to the edges.

2. An onST (z) fact arriving at a node y is already stored on the sender x. 3. If an onST (x) fact is stored on a node loc, then x = loc. 4. The onST relation grows consistently with ST (onST is actually the engine of the algorithm), and these two relations define a tree.

The first three properties are separately proved to be invariant. The last property is included in a predicate is tree(o, s), which intuitively means that the union of all onST facts o and the union of all ST facts s are consistent and they define a tree. We prove that if at the beginning of a round the first three properties together with is tree(o, s) hold, then at the end of the round is tree(o, s) still holds. The conjunction of all the four properties then constitutes an invariant of the protocol.

We check that the initial configuration generates a tree, then we have that in all configurations of any asynchronous run starting from the initial configuration, ST has the shape of a tree. This safety property is formalized in Coq (the script is available online [START_REF] Deng | Coq script for Netlog protocols[END_REF]).

Liveness, i.e. each node is eventually a member of onST , can be easily proved, provided the graph is finite and connected, and a fairness property is assumed in order to discard uninteresting runs where an inactive node is continuously chosen for each local round, instead of another node having an enabled rule. The proof is by induction on the finite cardinality of the set onST of nodes which do not satisfy onST . If at some point of a run this set is non-empty, then at least one of its members is a neighbor of the current tree due to connectivity. By fairness, this node eventually performs a local round and is no longer in onST . Formalizing such arguments involving liveness and fairness properties of infinite behaviors of distributed systems has already been done in Coq [START_REF] Deng | Verifying Self-stabilizing Population Protocols with Coq[END_REF]. The issue of termination is simpler in the synchronous setting, since fairness is no more needed to remove fake stuttering steps.

BFS in the Synchronous Case

For our second case study, the correctness proof of the BFS protocol, we prove that in the synchronous setting, the union of ST facts is the same as the one which would be computed by a centralized algorithm O (the oracle) running rules ( 1) and ( 2) on a reference version of the global relations onST and ST . This is subtler than one may expect at first sight, because decisions taken on a given node do not depend on the global relations onST and ST , but only on the visible part, which is made of the locally stored facts and of the arriving messages. Moreover, the information contained in an arriving onST (x) fact is ephemeral: this fact is not itself stored locally (only its consequences onST (y) and ST (m, y) are stored) and it will never be sent again. Indeed this information is available exactly at the right time. We therefore make a precise reasoning on the consistency of stored and transmitted facts with the computation that would be performed by the oracle O.

We denote by C the database of facts managed by O. Our main theorem states that a synchronous round in the distributed synchronous version corresponds to a step of computation performed by O on C. The proof relies necessarily on a suitable characterization of the body of rule [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF], which depends on the presence and the absence of facts onST . Therefore we need first to prove that facts onST , as computed by distributed rules ( 6) and [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF], are the ones computed by O and conversely -this is respectively called correctness and completeness of onST (definitions 3 and 6).

The first direction is not very hard (proposition 5). Completeness requires more attention. The issue is to ensure that, given an edge from x to y, such that onST (x) ∈ C but onST (y) ∈ C, the body of rule [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF] holds at y in order to ensure that rule [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF] will derive onST (y) as expected by rule (2) at the next step. If we just assume correctness and completeness of onST , we get onST (x) only on x, while we need it on y. Therefore a stronger invariant is needed. The key is the introduction of the notion of a good edge (definition 7) which says that if onST (x) is stored at x, then onST (y) is stored at y or onST (x) is arriving at y (both things can happen simultaneously as well). Here are the main steps. Additional properties, such as the establishment of the invariant in the initial configuration (actually: after one synchronous round) are available in [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF][START_REF] Deng | Coq script for Netlog protocols[END_REF].

Notation Let ϕ be a fact; here ϕ can have the shape E(x, y) or onST Proposition 2 After a transition, a configuration always satisfies received-onST-already-stored.

Proof. By inspection of store and push rules ( 6) and [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF]. Proof. By inspection of the consequences of rule (7) and using proposition 2.

Correctness of onST

Completeness of onST The notion of completeness needed is much more precise than the converse of correct-onST: the location where onST (z) is stored has to be known. This is especially clear in the proof of lemma 10. The following proposition is about non-extended configurations, i.e. it is purely about the distributed aspect of the BFS algorithm.

Proposition 8 received-onST-already-stored, all-good sr ---→ all-good

The main use of goodness is the completeness of the evaluation of the body of rule [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF].

Definition 9

We say that an extended configuration cnf , C is ready if and only if (i) it satisfies correct-onST, complete-onST-node and (ii) cnf satisfies all-good. Finally, we observe that invar is established after one synchronous round from the initial configuration, and that same-ST holds in the initial configuration. As a consequence, same-ST holds forever, as expected.

Besides this global property, one may wonder whether ST (x, y) facts are located on relevant nodes, i.e. child nodes y in our case, so that this information could be used by a higher layer protocol for transmitting data towards the root. This is actually a simple consequence of Rules ( 6) and [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF], since they ensure that ST (x, y) can only be stored on y. This is formally proved in our framework.

We developed a framework for verifying data-centric protocols expressed in a rule-based language. We have shown that both the synchronous and the asynchronous models of communication can be formalized in very similar ways from common building blocks, that can be easily adapted to other communication models.

Our framework has been implemented as a Coq library, which includes the formalization of the distributed computation environment with the communication network, as well as the embedded machine which evaluates the Netlog programs on each node. The Netlog programs are translated into straightforward Coq definitions. The proofs, sketched in the paper have been fully formalized in Coq [START_REF] Deng | Verifying Declarative Netlog Protocols with Coq: a First Experiment[END_REF]. As a preliminary result we proved a topological property of a distributed data structure -a tree -constructed by a simple but subtle program.

Figures on the size of our current Coq development are given in Table 1. The detail of justifications such as "by inspection of rules ( 6) and ( 7)" requires in general many bureaucratic proofs steps. From previous experience with Coq, we know that most of them can be automated using dedicated tactics, so that the user can focus entirely on the interesting part of the proof. The representation of Netlog rules was obtained in a systematical way and could be automated as well, using a deep embedding.

The distributed algorithm considered here as a case study was not as trivial as it may appear at first sight, though it can be expressed in a few lines of Netlog. It was sufficient to cover essential issues of a data-centric distributed algorithm, in particular the relationship between local transformations and global properties. Such properties are difficult to handle and even to state in event-centric approaches to the verification of distributed programs.

The advantage of the techniques we have developed is that they constitute a natural and promising open framework to handle other distributed data-centric algorithms. We are currently working on proofs for minimum spanning trees, and plan to further verify protocols for routing, election, naming, and other fundamental distributed problems. 2)) 360 Proofs on (asynchronous) ST (Rules ( 6) and ( 7)) 1100 Proofs on (synchronous) BFS (Rules ( 6) and ( 7)) 1300

Table 1. Size of coq scripts (in number of lines)

  pre A communication event at node loc specifies that the local data at loc does not change and that facts from out are appended on edges according to their destinations. communication(loc, mid , post, out) def = = |loc| post = |loc| mid ∀ y ∈ neighbors(loc), |loc →y| post = find (y, out) ∪ |loc →y| mid The function find returns the fact in out whose destination is y. Note that none of the previous three definitions specifies completely the next configuration in function of the previous one. They rather constrain a relation between two consecutive configurations by specifying what should happen at a given location. Combining these definitions in various ways allows us to define a complete transition relation between two configurations, with either a synchronous or an asynchronous behavior. async round (pre, post) def = round (loc, pre, mid , out) ∀ loc , loc = loc ⇒ no change at(loc , pre, mid ) communication(loc, mid , post, out) ∀ loc , loc = loc ⇒ communication(loc , mid , post, ∅) An asynchronous round between two configurations pre and post is given by a node Id loc, an intermediate configuration mid and a list of messages out such that there is a local round relating pre, mid and out on loc while no change occurs on loc different from loc, and a communication relates mid and out to post on loc while nothing is communicated on loc different from loc. sync round (pre, post) def = = ∃ mid , ∀ loc, ∃ out local round (loc, pre, mid , out) communication(loc, mid , post, out)

3 )

 3 onST (x) M W OE(min(m)) ← Root(x); E(x, y, m). (ST (x, y) onST (y) ← onST (x); ¬onST (y); E(x, y, m); !M W OE(m).

  (x) or ST (x, y). The presence of a fact ϕ in a database d is denoted by ϕ ∈ d. The set of facts ST (x, y) in d is denoted by d ST , and use a similar convention for onST end E. The database of facts stored at node loc is denoted by |loc|. Similarly, the database of facts arriving a node y from node x is denoted by |x→y|. Statements such as onST (z) ∈ |loc| are about a given configuration cnf or even an extended configuration cnf , C , and should be written cnf , C onST (z) ∈ |loc|. In general cnf is clear from the context and we just write P instead of cnf , C P . When we consider a synchronous round, i.e., a transition between two consecutive configurations pre and post, we write P sr ---→ Q for pre P ⇒ post Q. Similarly, for oracle transitions and transitions between extended configurations, we write respectively P o --→ Q for C P ⇒ C Q and P sro ---→ Q for pre, C P ⇒ post, C Q. Definition 1 A configuration satisfies received-onST-already-stored if and only if for all edges x→y, if onST (z) ∈ |x→y|, then z = x and onST (z) ∈ |x|.

Definition 3

 3 An extended configuration cnf , C satisfies correct-onST if and only if for all location loc of cnf , if some fact onST (z) is visible at loc, then onST (z) ∈ C. Proposition 4 onST (0) ∈ C o ---→ onST (0) ∈ C. Proof. By inspection of oracle rules (1) and (2). Proposition 5 onST (0) ∈ C, correct-onST sro ---→ correct-onST.

Lemma 10

 10 Given an extended configuration satisfying ready, and an edge x→y such that onST (x) ∈ C but onST (y) ∈ C, the body of rule (7) holds at y. The propagation of the completeness of onST follows. Proposition 11 ready sro ---→ complete-onST-node. Correctness and completeness of ST Definition 12 Let cnf be a given configuration. We say that cnf , C satisfies same-ST if and only if the union of all ST facts contained in some node of cnf is the same as set of facts ST in C. Proposition 13 ready, same-ST sro ---→ same-ST. Main theorem Our invariant is the following conjunction. Definition 14 An extended configuration cnf , C satisfies invar if and only if it satisfies onST (0) ∈ C, received-onST-already-stored, ready and same-ST. Theorem 15 invar sro ---→ invar. Proof. Immediate use of propositions 2, 4, 5, 11 and 13.

  ST algorithm (Rules (1) and (

  Definition 6 An extended configuration cnf , C satisfies complete-onST-node if and only if for all x, if onST (x) ∈ C, then onST (x) is stored at x. Definition 7 An edge x → y is good in a given configuration if and only if, if onST (x) ∈ |x|, then onST (y) ∈ |y| or onST (x) ∈ |x→y|. A configuration satisfies all-good if and only if all its edges are good.

Supported by the Natural Science Foundation of China under grant No. 61033002.