Elvira Albert

Puri Arenas

Miguel Gómez-Zamalloa

Actor-and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing

Testing concurrent systems requires exploring all possible non-deterministic interleavings that the concurrent execution may have. This is because any of the interleavings may reveal the erroneous behaviour. In testing of actor systems, we can distinguish two sources of non-determinism: (1) actor-selection, the order in which actors are explored and (2) task-selection, the order in which the tasks within each actor are explored. This paper provides new strategies and heuristics for pruning redundant state-exploration when testing actor systems by reducing the amount of unnecessary non-determinism. First, we propose a method and heuristics for actor-selection based on tracking the amount and the type of interactions among actors. Second, we can avoid further redundant interleavings in task-selection by taking into account the access to the shared-memory that the tasks make.

Introduction

Concurrent programs are becoming increasingly important as multicore and networked computing systems are omnipresent. Writing correct concurrent programs is harder than writing sequential ones, because with concurrency come additional hazards not present in sequential programs such as race conditions, data races, deadlocks, and livelocks. Therefore, software validation techniques urge especially in the context of concurrent programming. Testing is the most widelyused methodology for software validation. However, due to the non-deterministic interleavings of processes, traditional testing for concurrent programs is not as effective as for sequential programs. Systematic and exhaustive exploration of all interleavings is typically too time-consuming and often computationally intractable (see, e.g., [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] and its references).

We consider actor systems [START_REF] Agha | Actors: A Model of Concurrent Computation in Distributed Systems[END_REF][START_REF] Haller | Scala actors: Unifying Thread-Based and Event-Based Programming[END_REF], a model of concurrent programming that has been gaining popularity and that it is being used in many systems (such as ActorFoundry, Asynchronous Agents, Charm++, E, ABS, Erlang, and Scala). Actor programs consist of computing entities called actors, each with its own local state and thread of control, that communicate by exchanging messages asynchronously. An actor configuration consists of the local state of the actors and a set of pending tasks. In response to receiving a message, an actor can update its local state, send messages, or create new actors. At each step in the computation of an actor system, firstly an actor and secondly a process of its pending tasks are scheduled. As actors do not share their states, in testing one can assume [START_REF] Sen | Automated Systematic Testing of Open Distributed Programs[END_REF] that the evaluation of all statements of a task takes place serially (without interleaving with any other task) until it releases the processor (gets to a return instruction). At this point, we must consider two levels of non-determinism: [START_REF] Agha | Actors: A Model of Concurrent Computation in Distributed Systems[END_REF] actor-selection, the selection of which actor executes, and (2) task-selection, the selection of the task within the selected actor. Such nondeterminism might result in different configurations, and they all need to be explored as only some specific interleavings/configurations may reveal the bugs.

A naïve exploration of the search space to reach all possible system configurations does not scale. The challenge is in avoiding the exploration of redundant states which lead to the same configuration. Partial-order reduction (POR) [START_REF] Esparza | Model checking using net unfoldings[END_REF][START_REF] Godefroid | Using Partial Orders to Improve Automatic Verification Methods[END_REF] is a general theory that helps mitigate the state-space explosion problem by exploring the subset of all possible interleavings which lead to a different configuration. A concrete algorithm (called DPOR) was proposed by Flanagan and Godefroid [START_REF] Flanagan | Dynamic Partial-Order Reduction for Model Checking Software[END_REF] which maintains for each configuration a backtrack set, which is updated during the execution of the program when it realises that a nondeterministic choice must be tried. Recently, TransDPOR [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] extends DPOR to take advantage of the transitive dependency relations in actor systems to explore fewer configurations than DPOR. As noticed in [START_REF] Lauterburg | Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques[END_REF][START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF], their effectiveness highly depend on the actor selection order. Our work enhances these approaches with novel strategies and heuristics to further prune redundant state exploration, and that can be easily integrated within the aforementioned algorithms. Our main contributions can be summarized as follows:

1. We introduce a strategy for actor-selection which is based on the number and on the type of interactions among actors. Our strategy tries to find a stable actor, i.e., an actor to which no other actor will post tasks. 2. When temporal stability of any actor cannot be proven, we propose to use heuristics that assign a weight to the tasks according to the error that the actor-selection strategy may make when proving stability w.r.t. them. 3. We introduce a task-selection function which selects tasks based on the access to the shared memory that they make. When tasks access disjoint parts of the shared memory, we avoid non-determinism reordering among tasks. 4. We have implemented our actor-selection and task-selection strategies in aPET [START_REF] Albert | aPET: A Test Case Generation Tool for Concurrent Objects[END_REF], a Test Case Generation tool for concurrent objects. Our experiments demonstrate the impact and effectiveness of our strategies.

The rest of the paper is organized as follows. Section 2 presents the syntax and semantics of the actor language we use to develop our technique. In Sec. 3, we present a state-of-the-art algorithm for testing actor systems which captures the essence of the algorithm in [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] but adapted to our setting. Section 4 introduces our proposal to establish the order in which actors are selected. In Sec. 5, we present our approach to reduce redundant state exploration in the task selection strategy. Our implementation and experimental evaluation is presented in Sec. 6. Finally, Section 7 overviews related work and concludes.

The Actor Model

We consider a distributed message-passing programming model in which each actor represents a processor which is equipped with a procedure stack and an unordered buffer of pending tasks. Initially all actors are idle. When an idle actor's task buffer is non-empty, some task is removed, and the task is executed to completion. Each task besides accessing its own actor's global storage, can post tasks to the buffers of any actor, including its own. When a task does complete, its processor becomes idle, chooses a next pending task to remove, and so on.

Syntax and Semantics

Actors are materialized in the language syntax by means of objects. An actor sends a message to another actor x by means of an asynchronous method call, written x ! m(z), being z parameters of the message or call. In response to a received message, an actor then spawns the corresponding method with the received parameters z. The number of actors does not have to be known a priori, thus in the language actors can be dynamically created using the instruction new.

Tasks from different actors execute in parallel. The grammar below describes the syntax of our programs.

M ::= void m( T x){s; } s ::= s ; s | x = e | x = this.f | this.f = y | if b then s else s | while b do s | x = new C | x ! m(z) | return
where x, y, z denote variables names, f a field name and s an instruction. For any entity A, the notation Ā is used as a shorthand for A 1 , ..., A n . We use the special actor identifier this to denote the current actor. For the sake of generality, the syntax of expressions e, boolean conditions b and types T is not specified. As in the object-oriented paradigm, a class denotes a type of actors including their behavior, and it is defined as a set of fields and methods. In the following, given an actor a, we denote by class(a) the class to which the actor belongs. Fields(C) stands for the set of fields defined in class C. We assume that there are no fields with the same name and different type. As usual in the actor model [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF], we assume that methods do not return values, but rather that their computation modify the actor state. The language is deliberately simple to explain the contributions of the paper in a clearer way and in the same setting as [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF]. However, both our techniques and our implementation also work in an extended language with tasks synchronization using future variables [START_REF] De Boer | A Complete Guide to the Future[END_REF].

An actor is a term act(a, t, h, Q) where a is the actor identifier, t is the identifier of the active task that holds the actor's lock or ⊥ if the actor's lock is free, h is its local heap and Q is the set of tasks in the actor. A task is a term tsk(t, m, l, s) where t is a unique task identifier, m is the method name executing in the task, l is a mapping from local variables to their values, and s is the sequence of instructions to be executed or if the task has terminated. A state or

(mstep) selectActor (S) = act(a, ⊥, h, Q), Q = ∅, selectTask (a) = t, S a•t ; * S S a•t -→ S (setfield) t = tsk(t, m, l, this.f = y; s) act(a, t, h, Q ∪ {t}) ; act(a, t, h[f → l(y)], Q ∪ {tsk(t, m, l, s)}) (getfield) t = tsk(t, m, l, x = this.f ; s) act(a, t, h, Q ∪ {t}) ; act(a, t, h, Q ∪ {tsk(t, m, l[x → h(f )], s)}) (newactor) t = tsk(t, m, l, x = new D; s), fresh(a ), h = newheap(D), l = l[x → a ] act(a, t, h, Q ∪ {t}) ; act(a, t, h, Q ∪ {tsk(t, m, l , s)}) • act(a , ⊥, h , {}) (async) t = tsk(t, m, l, x ! m1(z); s), l(x) = a1, fresh(t1), l1 = buildLocals(z, m1, l) act(a, t, h, Q ∪ {t}) • act(a1, , , Q ) ; act(a, t, h, Q ∪ {tsk(t, m, l, s)}) • act(a1, , , Q ∪ {tsk(t1, m1, l1, body(m1))}) (return) t = tsk(t, m, l, return; s) act(a, t, h, Q ∪ {t}) ; act(a, ⊥, h, Q)
0 •a 1 •• • ••a n , where a i ≡ act(a i , t i , h i , Q i ).
The execution of a program from a method m starts from an initial state S 0 = {act(0, 0, ⊥, {tsk(0, m, l, body(m))}. Here, l maps parameters to their initial values (null in case of reference variables), body(m) is the sequence of instructions in method m, and ⊥ stands for the empty heap.

Fig. 1 presents the semantics of the actor model. As actors do not share their states, the semantics can be presented as a macro-step semantics [START_REF] Sen | Automated Systematic Testing of Open Distributed Programs[END_REF] (defined by means of the transition "-→") in which the evaluation of all statements of a task takes place serially (without interleaving with any other task) until it gets to a return instruction. In this case, we apply rule mstep to select an available task from an actor, namely we apply the function selectActor (S) to select nondeterministically one active actor in the state (i.e., an actor with a non-empty queue) and selectTask (a) to select non-deterministically one task of a's queue. The transition ; defines the evaluation within a given actor. We sometimes label transitions with a • t, the name of the actor a and task t selected (in rule mstep) or evaluated in the step (in the transition ;). The rules getfield and setfield read and write resp. an actor's field. The notation h[f → l(y)] (resp. l[x → h(f )]) stands for the result of storing l(y) in the field f (resp. h(f ) in variable x). The remaining sequential instructions are standard and thus omitted. In newactor, an active task t in actor a creates an actor a of class D which is introduced to the state with a free lock. Here h = newheap(D) stands for a default initialization on the fields of class D. async spawns a new task (the initial state is created by buildLocals) with a fresh task identifier t 1 . We assume a = a 1 , but the case a = a 1 is analogous, the new task

t 1 is added to Q of a.
In what follows, a derivation or execution E ≡ S 0 -→ • • • -→ S n is a sequence of macro-steps (applications of rule mstep). The derivation is complete if S 0 is the initial state and all actors in S n are of the form act(a, ⊥, h, {}). Since the execution is non-deterministic, multiple derivations are possible from a state. Given a state S, exec(S) denotes the set of all possible derivations starting at S. Explore(E • next(S, a • t));

Fig. 2. A state-of-the-art algorithm for testing

This section presents a state-of-the-art algorithm for testing actor systems -which captures the essence of the algorithm DPOR in [START_REF] Flanagan | Dynamic Partial-Order Reduction for Model Checking Software[END_REF] and its extension TransDPOR [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF]-but it is recasted to our setting. The main difference with [START_REF] Flanagan | Dynamic Partial-Order Reduction for Model Checking Software[END_REF][START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] is that we use functions selectActor and selectTask that will be redefined later with concrete strategies to reduce redundant state exploration. To define the notion of redundancy, we rely in the standard definition of partial order adapted to our macro-step semantics. An execution

E = S 0 a1•t1 -→ • • • an•tn -→ S n
defines a partial order [START_REF] Flanagan | Dynamic Partial-Order Reduction for Model Checking Software[END_REF] between the tasks of an actor. We write t i < t j , if t i , t j belong to the same actor a and t i is selected before t j in E. Given S, we say that E 1 , E 2 ∈ exec(S) are equivalent if they have the same partial order for all actors.

Definition 1 (redundant state exploration). Two complete executions are redundant if they have the same partial order.

The algorithm DPOR [START_REF] Flanagan | Dynamic Partial-Order Reduction for Model Checking Software[END_REF], and its extension TransDPOR [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF], achieve an enormous reduction of the search space. Function Explore in Fig. 2 illustrates the construction of the search tree that these algorithms make. It receives as parameter a derivation E, which starts from the initial state. We use last(E) to denote the last state in the derivation, next(S, a • t) to denote the step S

a•t -→ S and E • next(S, a • t) to denote the new derivation E a•t
-→ S . Intuitively, each node (i.e., state) in the search tree is evaluated with a backtracking set back , which is used to store those actors that must be explored from this node. The backtracking set back in the initial state is empty. The crux of the algorithm is that, instead of considering all actors, the back set is dynamically updated by means of function updateBackSets(E , S ) with the actors that need to be explored. In particular, an actor is added to back only if during the execution the algorithm realizes that it was needed. Intuitively, it is needed when, during the execution, a new task t of an actor a previously explored, occurs. Therefore, we must try different reorderings between the tasks since according to Def. 1 they might not be redundant. In this case, the back set of the last state S in which a was used to give a derivation step might need to be updated. As a simple example, consider a state S in which an actor a with a unique task t 1 is selected. Now, assume that when the execution proceeds, a new task t 2 of a is spawned by the execution of a task t of an actor a and that t was in S. This means that it is required to consider also first the execution of t 2 and, next the execution of t 1 , since it represents a different partial order between the tasks of a. This is accomplished by adding a to the back set of S, which allows exploring the execution in which a is selected before a at S, and thus considering the partial order t 2 < t 1 . The formal definition of updateBackSets (and its optimization with freeze flags to avoid further redundancy) can be found at [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF]. Function selectActor at line 4 selects non-deterministically an active actor in S (or returns if there is none). The back set is initialized with the selected actor. The while loop at line 8 picks up an actor in the back set that has not been evaluated before (checked in done set) and explores all its tasks (lines 10-11).

Example 1. Consider the program in Fig. 3 borrowed from [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] and extended with field accesses to later explain the concepts in Sec. 5. It consists of 3 classes, one registry Reg and two workers Worker 1 and Worker 2 , together with a main block from which the execution starts. In Fig. 4 we show the search tree built by executing Explore(E 0 ), where E 0 = S ini main -→ S 0 , and S ini is the initial state from the main block. The branches in the tree show the macro-steps performed labeled with the task selected at the step (the object identifier is omitted). We distinguish three types of edges: dotted edges are introduced by the for loop at line 10 in Fig. 4, dashed edges are eliminated by the improvement of [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF], and normal edges are introduced by the while loop at line 8. After executing the main block, there are three actors S 0 ={rg, wk1, wk2} in node 0 and their queues of pending tasks are

Q rg ={p()}, Q wk1 ={q(rg)} and Q wk2 ={h(rg)} resp. Let us focus on the execution E 2 = S 0 p -→ S 1 q -→ S 2 .
The recursive call Explore(E 2 ) updates the back set of S 0 because a new task m() of rg (previously explored) occurs. Since this task has been produced by the execution of wk1 ! q(rg) and task q(rg) is in S 0 , then back (S 0 ) = {rg, wk1}. The derivation continues and task wk2 ! h(rg) is selected. The execution of E 3 =E 2 h -→ S 3 introduces t() in the queue of rg. The recursive call Explore(E 3 ) updates the back set of node 0 by introducing wk2 in back (S 0 ) since it is the responsible of introducing t() on rg (dashed line in node 0). This branch, which generates 14 more (redundant) executions, can be avoided by introducing a "freeze" flag as done in [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF], an optimization that we adopt but which is no relevant to explain our contributions. In S 3 , the unique active actor rg is selected, and its tasks explored. The execution continues in a similar way and other nodes are added to the back sets. For instance, the back set of node 8 is updated with wk2 from node 10.

Actor-Selection based on Stability Criteria

This section introduces our method to establish the order in which actors are selected based on their stability levels. In Sec. 4.1 we first motivate the problem. Afterwards, Sec. 4.2 introduces the notion of temporarily stable actor and sufficient conditions to ensure it dynamically during testing. Finally, Section 4.3 presents heuristics based on the stability level of actors.

Motivation

In Algorithm 2, function selectActor selects non-deterministically an active actor in the state. As noticed in [START_REF] Lauterburg | Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques[END_REF], the pruning that can be achieved using the testing algorithm in Sec. 3 is highly dependent on the order in which tasks are considered for processing. Consider the execution tree in Fig. 4. By inspecting the branches associated to the terminal nodes, we can see that the induced partial order p<m<t occurs in the executions ending in 5, 12, 18, p<t<m in those ending in 7, 14, 20, m<p<t ending in 23, m<t<p ending in node 25, t<p<m ending in 28, and t < m < p ending in 30. Hence, it is enough to consider the coloured subtree since the remaining executions (ending in 5, 7, 12, 14) have the same partial order than some other execution in the coloured tree. Our work is motivated by the observation that if selectActor first selects an actor to which no other actors will post tasks, then we can avoid redundant computations. In particular, if selectActor selects wk1, the exploration will lead to the coloured search tree, which does not make any redundant state-exploration.

The Notion of Temporal Stability

The notion of temporal stability will allow us to guide the selection of actors so that the search space can be pruned further and redundant computations avoided. An actor is stable if there is no other actor different from it that introduces tasks in its queue. Basically, this means that the actor is autonomous since its execution does not depend on any other actor. In general, it is quite unlikely that an actor is stable in a whole execution. However, if we consider the tasks that have been spawned in a given state, it is often the case that we can find an actor that is temporarily stable w.r.t. the actors in that state.

Definition 2 (temporarily stable actor). act(a, t, h, Q) is temporarily stable in S iff, for any E starting from S and for any subtrace S * -→ S ∈ E in which the actor a is not selected, we have act(a, t, h, Q) ∈ S .

The intuition of the definition is that an actor's queue cannot be modified by the execution of other actors (which are different from itself). E.g., actor rg in Ex. 1 is not temporarily stable in S 0 because the derivation S 0 p -→S 1 q -→S 2 introduces the task m() in the queue of rg.

Lemma 1. Let a be a temporarily stable actor in a state S. For any execution E generated by Explore(S) such that selectActor (S)=a, we have back (S)={a}.

The intuition of the lemma is that if selectActor returns a temporarily stable actor a, it is ensured that, from that state, there will be only a branch in the search tree (that corresponds to the selection of a), i.e., no other actors will be added to back during its exploration using the testing algorithm Explore.

Our goal is to come up with sufficient conditions that ensure actors stability and that can be computed during dynamic execution. To this end, given a method m 1 of class A 1 , we define Ch(A 1 ::m 1 ) as the set of all chains of method calls of the form A 1 ::m 1 →A 2 ::m 2 → • • • →A k ::m k , with k≥2, such that A i ::m i = A j ::m j , 2≤i≤k-1, i = j and there exists a call within body(A i ::m i ) to method A i+1 ::m i+1 , 1≤i<k. This captures all paths A 2 ::m 2 → A k-1 ::m k-1 , without cycles, that go from A 1 ::m 1 to A k ::m k . The set Ch(A 1 ::m 1 ) can be computed statically for all methods.

Theorem 1 (sufficient conditions for temporal stability). We say that act(a, t, h, Q) ∈ S, class(a)=A n is temporarily stable in S, if for every act(a , t , h , Q ) ∈ S, a = a , class(a )=A 1 , and for every tsk( , m 1 , l, s) ∈ Q , one of the following conditions holds:

1. There is no chain A 1 ::m 1 → • • • → A n ::m n ∈ Ch(A 1 ::m 1 ); or 2. For all chains A 1 ::m 1 → • • • → A n ::m n ∈Ch(A 1 ::m 1 ), l(x) =a holds, for all x∈dom(l), h (f ) =a for all f ∈Fields(A 1 ), and for all act(a , , h , )∈S with class(a )=A i , 2≤i≤n-1, then h (f ) =a, for all f ∈Fields(A i ).

Intuitively, the theorem above ensures that a cannot modify the queue of a. This is because (1) there is no transitive call from m 1 to any method of class A n to which object a belongs, or (2) there are transitive calls from m 1 to some method of class A n , but no reference to actor a can be found along the chain of objects that will lead to the potential call (that will post a task on actor a).

In order to be sound, we check the second condition on all objects in the state whose type matches that of the methods considered in the chain of calls. The following example illustrates why seeking the reference in intermediate objects is required in condition (2).

Example 2. Consider S=act(a 1 , , h 1 , Q 1 ) • act(a 2 , , h 2 , ∅) • act(a 3 , , h 3 , Q 3 ), of classes A, B and C resp., with Q 3 ={tsk(t 3 , m, l 3 , {y!p(); return; })}, l 3 (y) = a 2 , body(B :: p) = {x = this.f ; x!q(); return; }, and h 2 (f ) = a 1 . Then, even if a 3 does not have a reference to a 1 , it is able to introduce the call q() to Q 1 . This is because from m there is a call to p() and from there to f !q() with h 2 (f ) = a 1 . Thus actor a 1 is not temporarily stable.

Th. 1 allows us to define selectActor in Fig. 2 such that it returns an actor a in S which is temporarily stable. If such actor does not exist, then it returns randomly an active object in S.

Example 3. Consider Ex. 1. At node 0 the actor rg is not temporarily stable because in the queue of wk1 there is a call q(rg) (i.e., actor rg can be reachable from q), and in the body of method q there is also a call to method m() of class Reg (i.e., rg can possibly be modified by wk1). However, actors wk1 and wk2 are temporarily stable at node 0. Thus we can select any of these actors to start the exploration. In Fig. 4, actor wk1 has been selected, resulting in the coloured subtree. Similarly, in node 8, rg is not temporarily stable but wk2 it is.

Heuristics based on Stability Level

When we are not able to prove that there is a stable actor, then we can use heuristics to determine which actor must be explored first. In particular, we refine the definition of function selectActor so that it computes stability levels for the actors and selects the actor with highest stability level. Our heuristics tries to weight the loss of precision of the sufficient conditions in Th. 1 in the following way: (1) k a : this is the value assigned by the heuristics to the case in which an object is not stable due to a direct call from another object that has a reference to it, ( 2) k b : it corresponds to the case in which stability is lost by a transitive (indirect) call from another object that has a reference to it, (3) k c : this is the case in which the object that breaks its stability does not have a reference to it (instead some intermediate object will have it). It is clear that the heuristics must assign values such that k a > k b > k c . This is because the most likely scenario in which the sufficient conditions detect an unfeasible nonstability is (3) since the loss of precision can be large when we seek references to the object within all other objects of the intermediate types in the call chain.

The first scenario ( 1) is more likely to happen since we have both the reference and the direct call. Scenario ( 2) is somewhere in the middle. Thus, we define the stability level of a∈class(A n ) w.r.t. a tsk(t, m 1 , l, ) of an actor act(a , , h , )∈S breaking its stability (a = a , class(a )=A 1 ) and a chain Ch = A 1 ::m 1 → * A n ::m n , denoted as st(a, t, Ch, S), as follows:

(a) If l(x)=a, for some x ∈ dom(l) or h (f )=a, for some f ∈ Fields(A 1 ) and n=2, then st(a, t, Ch, S)=k a . (b) If l(x)=a, for some x ∈ dom(l) or h (f )=a, for some f ∈ Fields(A 1 ) and n > 2, then st(a, t, Ch, S)=k b . (c) Otherwise, i.e., l(x) = a, for all x ∈ dom(l) and h (f ) = a, for all f ∈ Fields(A 1 ), then st(a, t, Ch, S)=k c .

The stability level of an actor a ∈ S, class(a)=A n , w.r.t. a task tsk(t, m 1 , l, ) from act(a , , h , ) ∈ S, class(a )=A 1 , denoted as st(a, t, S), is defined as st(a, t, Ch, S) such that Ch = A 1 ::m 1 → * A n ::m n ∈ Ch(A 1 ::m 1 ).

Definition 3 (stability level of an actor). Let a be a non temporarily stable actor in a state S. The stability level of a in S, denoted as st(a, S), is defined as st(a, t, S)

such that t ∈ Q , act(a , t, h , Q ) ∈ S, a = a .
Given a state S = a 1 •. . .•a n , the above definition allows us to define the function selectActor (S) in Fig. 2 such that, in case of finding an active actor, it returns a temporarily stable actor a if it exists, and otherwise it returns a i , where a i satisfies st(a i , S) ≥ st(a j , S), for all 1 ≤ i, j ≤ n, i = j.

Example 4. Let us consider the program in Fig. 5, borrowed from [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF], which computes the nth element in the Fibonacci sequence in a distributed fashion. The computation starts with the execution of a task fib(3) on actor a 1 , which in turn generates two actors a 2 and a 3 with Q a2 = {fib(2)} and Q a3 = {fib(1)}.

the "depth" of the calls according to the number of conditions that need to be checked to perform the call. In the absence of a stable object, it is also sensible to select the object that is breaking most stabilities, since once it is explored, those objects whose stability it was breaking might become stable.

Task Selection based on Shared-Memory Access

In the section, we present our approach to reduce redundant state exploration within task selection. In Sec. 5.1, we first motivate the problem and characterize the notion of task independence. In Sec. 5.2 we provide sufficient conditions to ensure it. Finally, Sec. 5.3 presents our task selection function.

Motivation

Let us observe that there can executions with different partial-orders which lead to the same state, which according to a stronger notion of redundancy could be considered as redundant executions. Consider node 15 in the search tree of Fig. 4. At this point, only tasks of actor rg are available. The derivations ending in nodes 18, 23, 25 result in the same state (namely fields of object rg are f=2, g=3) and the derivations to nodes 20, 28 and 30 also result in the same state (f=2, g=4). The reason for this redundancy is that the execution of p is independent from the executions of m and t because they access disjoint areas of the shared memory. However tasks m and t are not independent and the order in which they are executed affects the final result.

Definition 4. Tasks t 1 and t 2 are independent, written indep(t 1 , t 2 ), if for any complete execution S 0 -→ • • • -→ S n with t 1 < t 2 , there exists another execution

S 0 -→ • • • -→ S n with t 2 < t 1 .
Observe that according to Def. 1, the above two derivations are not redundant (as they have a different partial order). However, they are redundant because they lead to the same state, which is a stronger notion of redundancy.

The Notion of Task Independence

The notion of independence between tasks is well-known in concurrent programming [START_REF] Andrews | Concurrent Programming: Principles and Practice[END_REF]. Basically, tasks t and t are independent if t does not write in the shared locations that t accesses, and viceversa. The following definition provides a syntactic way of ensuring task independence by checking the fields that are read and written. Let act(a, , , Q)∈S and tsk(t, m, , s)∈Q. We define the set W (t) as {f | this.f =y ∈ s}. Similarly, the set R(t) is defined as {f | x=this.f ∈ s}. The following theorem is an immediate consequence of the definition of independent task above. We denote by indep(t 1 , t 2 ) that t 1 and t 2 are independent.

Theorem 2 (sufficient condition for tasks independence). Given a state S, an actor act(a, , , Q) ∈ S and two tasks t

1 , t 2 ∈ Q. If R(t 1 ) ∩ W (t 2 ) = ∅, R(t 2 )∩ W (t 1 ) = ∅ and W (t 1 ) ∩ W (t 2 ) = ∅, then indep(t 1 , t 2 ) holds.

9:

for all t ∈ selectTask (a) do 10: unmark (a); mark (t, a); 11:

Explore(E • next(S, a • t))

Fig. 6. Refining Algorithm 2 with Task Selection

Note that since the actor state is local, i.e., fields cannot be accessed from other actors. Thus, all accesses to the heap are on the actor this.

A Task-Selection Function based on Task-Independence

We now introduce in Alg. 2 a task selection function which avoids unnecessary reorderings among independent tasks. To this end, we introduce marks in the tasks such that the elements in the queues have the form t, flag , where t is a task and mark is a boolean flag which indicates if the task can be selected. Furthermore, we treat queues as lists and assume that its elements appear in the order in which they were added to the queue during execution. In order to implement task independence in Alg. 2, we replace lines 10 and 11 of Alg. 2 by those in Fig. 6 where we have that: (1) function selectTask (a) returns the list of unmarked tasks in the queue Q of a, i.e, those tasks of the form t, false ; (2) procedure unmark (a) traverses Q and changes the flag mark to false; and (3) procedure mark (t, a) sets the flag mark to true for all tasks which are independent with t and occur in Q after t. Intuitively the task selection process works as follows. Given act(a, , , Q)∈S, Q contains a list [t 1 , . . . , t n ] of tasks. These tasks are selected one by one traversing Q (line 10 of Alg, 2). This means that if t i is selected by selectTask (a) and t i is independent from t j , then i < j, i.e., the task t i is selected before t j . Furthermore, procedure mark (t i , a) puts the flag mark of t j to true. Thus, in the following step in which actor a is selected, task t j cannot be chosen, i.e., the direct order t i < t j is pruned. By direct order, we mean that t j is selected immediately after t i . However, when t j is selected from S, as it occurs after t i , then t i will not be marked. This branch will capture the direct order t j < t i . Since both orders generate equivalent states, no solution is missed.

Example 5. Consider the execution tree in Fig. 4, and the subtree from node 15 in Fig. 7, where t denotes that the flag mark of t is true. At this point, all tasks in rg have the flag mark set to false. Thus selectTask (rg) returns the list [p, m, t]. Procedure unmark does nothing. The execution of mark (p, rg) then sets the flag mark of m and t to true since indep(p, m) and indep(p, t). This branch is therefore cut at node 16 (selectTask (rg) returns the empty list). Afterwards, the selection of m from node 15 does not mark any task. However, when selecting p from node 21, procedure mark (p, rg) sets the flag of t to true since we have the independence relation indep(p, t). Hence at node 22 the branch is cut (selectActor (rg) returns the empty list). Similarly, at node 27 the branch is cut

Implementation and Experimental Evaluation

We have implemented and integrated all the techniques presented in the paper within the tool aPET [START_REF] Albert | aPET: A Test Case Generation Tool for Concurrent Objects[END_REF], a test case generator for ABS programs which is available at http://costa.ls.fi.upm.es/apet. ABS [START_REF] Johnsen | ABS: A Core Language for Abstract Behavioral Specification[END_REF] is a concurrent, object-oriented, language based on the concurrent objects model, an extension of the actors model which includes future variables and synchronization operations. Handling those features within our techniques does not pose any technical complication. This section reports on experimental results which aim at demonstrating the applicability, effectiveness and impact of the proposed techniques during testing. The experiments have been performed using as benchmarks: (i) a set of classical actor programs borrowed from [START_REF] Lauterburg | Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques[END_REF][START_REF] Sen | Automated Systematic Testing of Open Distributed Programs[END_REF][START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] and rewritten in ABS from ActorFoundry, and, (ii) some ABS models of typical concurrent systems. Specifically, QSort is a distributed version of the Quicksort algorithm, Fib is an extension of the example at Fig. 5, PI, computes an approximation of π distributively, PSort is a modified version of the sorting algorithm used in the dCUTE study [START_REF] Sen | Automated Systematic Testing of Open Distributed Programs[END_REF], RegSim is a server registration simulation, DHT is a distributed hash A relevant point to note, which is not shown in the table, is that no backtracking due to actor selection is performed at any state of any test. The number of executions is therefore induced by the non-determinism at task selection. In most states, overall in 99.9% of them, our sufficient condition for temporal stability is able to determine a stable actor (compare column H against States). Interestingly, at all states where no stable actor can be found, the heuristics for temporal stability guides the execution towards selections of actors which are indeed temporarily stable. This demonstrates that, even though our sufficient condition for stability and heuristics are syntactic, they are very effective in practice since they are computed dynamically on every state. Another important point to observe is the huge pruning of redundant executions which our task selection function is able to achieve for most benchmarks. Last two columns show the gain of the task selection function in number of executions and time. In most benchmarks, the speedup ranges from one to two orders of magnitude (the more complex the programs the bigger the speedup). There is however no reduction in the first three benchmarks. This is because they only generate actors of the same type, and at most two kinds of tasks, usually recursive, which are dependent. This is also the main reason of the loss of precision of our sufficient condition for temporal stability for these benchmarks (namely, cond. 2 of Th. 1 needs to consider all actors in the state).

There are two more benchmarks, Chameneos and Shortpath, also borrowed from [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF], that have been used in our evaluation. We do not provide concrete data for them in the table since they cannot be handled yet by our current implementation. In Chameneos the heuristics needs to be used at many states in order to select an actor. The heuristics of Sec. 4.3 enriched to take into account calls affected by conditional instructions (as described at the end of Sec. 4) would always be able to select actors which are indeed temporarily stable. The ShortPath benchmark poses new challenges. It builds a cyclic graph of actors, all of the same type, which interact through a recursive task. An intelligent actor selection heuristics able to prune redundant executions in this case would require detecting tasks which execute their base case. This could be done by computing constrained call-chains, and checking dynamically that the constraints hold in order to sum-up the effect of the call-chain when computing the non-stability factor.

Related Work and Conclusions

We have proposed novel techniques to further reduce state-exploration in testing actor systems which have been proven experimentally to be both efficient and effective. Whereas in [START_REF] Lauterburg | Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques[END_REF][START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] the optimal redundancy reduction can only be accomplished by trying out different selection strategies, our heuristics is able to generate the most intelligent strategy on the fly. Additionally, our task selection reduction has been shown to be able to reduce the exploration in up to two orders of magnitude. Our techniques can be used in combination with the testing algorithms proposed in [START_REF] Flanagan | Dynamic Partial-Order Reduction for Model Checking Software[END_REF][START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF]. In particular, the method in [START_REF] Tasharofi | TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs[END_REF] makes a blind selection on the actor which is chosen for execution first. While in some cases, such selection is irrelevant, it is known that the pruning that can be achieved is highly dependent on the order in which tasks are considered for processing (see [START_REF] Lauterburg | Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques[END_REF]). Sleep sets, as defined in [START_REF] Godefroid | Using Partial Orders to Improve Automatic Verification Methods[END_REF], can be used as well to guide actor-selection by relying on different criteria than ours (in particular, they use a notion of independence different from ours). However, we have not found practical ways of computing them, while we can syntactically detect stable actors by some inspections in the state. Also, we define actor selection strategies based on the stability level of actors. The accuracy of such strategies can be improved by means of static analysis. In particular, points-to analysis [START_REF] Steensgaard | Points-to Analysis in almost Linear Time[END_REF] can be useful in Th. 2 to detect more accurately if there is a reference to an object from another one and also to know from which object a method is invoked. Another novelty of our approach to reduce useless state-exploration is to consider the access to the shared memory that tasks make. This allows us to avoid non-deterministic task-selection among independent tasks. A strong aspect of our work is that it can be used in symbolic execution [START_REF] Clarke | A System to Generate Test Data and Symbolically Execute Programs[END_REF][START_REF] King | Symbolic Execution and Program Testing[END_REF] directly. In symbolic execution, it is even more crucial to reduce state-exploration, since we already have nondeterministic choices due to branching in the program and due to aliasing of reference variables. In aPET, we use our method to prune the state-exploration of useless interleavings in the context of symbolic execution of actor programs.

Recently, the project Setak [START_REF] Setak | A Framework for Stepwise Deterministic Testing of Akka Actors[END_REF] has developed a new testing framework for actor programs. Differently to us, where everything is automatic, part of the testing is doing manually, and programmers may specify the order of tasks during the execution of a test.

Fig. 1 .

 1 Fig. 1. Summarized Semantics for Distributed and Concurrent Execution

Fig. 4 .

 4 Fig. 4. Execution Tree

  Pruning due to task-selection because of indep(p, m). The only derivations are those ending in nodes 25 and 30 which correspond to the order of tasks m < t < p and t < m < p, resp.

	{p,m,t}	15
	p			t
	{p,t} m	{p,m}
	16		21		26
	{m, t}	p		t	p	m
	{t}	22		24	27	29
	n1=2, n2=8, n3=8	25 p	{m}	30	p
					n1=2, n2=8, n3=7
	independent tasks
	node 15: indep(p,m) indep(p,t)
	node 21: indep(p,t) node 26: indep(p,m)
	Fig. 7.

table ,

 , Mail is an email client-server simulation, and BB is a classical producerconsumer. All sources are available at the above website. For each benchmark, we consider two different tests with different input parameters. Table1shows the results obtained for each test. After the name, the first (resp. second) set of columns show the result with (resp. without) our task selection function. For each run, we measure: the number of finished executions (column Execs); the total time taken and number of states generated by the whole exploration (columns Time and States); and the number of states at which no stable actor

Table 1 .

 1 Experimental evaluation is found and the heuristics is used for actor selection (column H ).

	Times are in

Acknowledgements This work was funded partially by the EU project FP7-ICT-610582 ENVISAGE: Engineering Virtualized Services (http://www.envisageproject.eu) and by the Spanish projects TIN2008-05624 and TIN2012-38137.

Both a 2 and a 3 are clearly temporarily stable since there is no reference pointing to them. Let us select a 2 and therefore execute its task fib(2). This generates two more actors a 4 and a 5 with Q a4 = {fib(1)} and Q a5 = {fib(0)}. Again a 4 and a 5 are clearly temporarily stable. After selecting successively a 3 , a 4 and a 5 we reach a state S, where a 3 , a 4 and a 5 have an empty queue, Q a1 = {res(1)}, and Q a2 = {res(1), res(0)}. At this point, our sufficient condition for temporal stability is not able to determine a stable actor. Namely, a 1 is clearly non-stable since the execution of task res on a 2 can, and will, eventually launch a task res on it. However, a 2 is stable, but we cannot determine it syntactically since there is a call chain Fib::res → Fib::res → Fib::res (i.e. we can reach from F ib::res to F ib::res through F ib::res), which forces us to look for a reference to a 2 within all actors of type Fib (cond. 2 of Th. 1). That includes a 4 and a 5 whose parent field points to a 2 . Interestingly, our heuristics assigns a much lower non-stability factor to a 2 than to a 1 , making it being selected first. Specifically, st(a 2 , S) = k c whereas st(a 1 , S) = 2 * k a + 2 * k c . The latter is because we find 4 tasks that break the stability, 2 of them fulfill condition (a) and the two others condition (c). A wrong selection of a 1 would cause a backtracking at S which produces the exploration of redundant executions. In this concrete example, 8 executions would be explored, whereas with our right selection we explore 4.

We have defined a heuristics which according to our experiments works very well in practice. However, there are other factors to be taken into account to define other heuristics. For instance, it is relevant to consider if the calls appear within conditional instructions (and thus they may finally not hold). This can be easily detected from the control flow graph of the program, where we can define


Carlos Gregorio-Rodríguez

Luis Llana
email: llana@ucm.es

Rafael Martínez-Torres

Effectiveness for input output conformance simulation iocos

Keywords: Model Based Testing, Online Testing, Simulation Algorithm, Input Output Conformance Simulation, Model Checking Minimisation, Verification, Generalised Coarsest Partition Problem, Formal Methods

In this paper we continue the study of the input-output conformance simulation (iocos). In particular, we focus on implementation aspects to show that iocos is indeed an interesting semantic relation for formal methods. We address two complementary issues: a) In the context of model based testing (MBT) we present an online, also called on-the-fly, testing algorithm that checks whether an implementation conforms a given specification. Online testing combines test generation and execution and avoids the generation of the complete test suite for the specification. We prove both soundness and completeness of the online algorithm with respect to the iocos relation. b) In the context of formal verification and model checking minimisation a key issue is to efficiently compute the considered semantic relations; we show how the coinductive flavour of our conformance relation iocos makes it appropriate to be cast into an instance of the Generalised Coarsest Partition Problem (GCPP) and thus it can be efficiently computed.

Introduction

In a recent paper [START_REF] Gregorio-Rodríguez | Input-output conformance simulation (iocos) for model based testing[END_REF] we introduced the input-output conformance simulation relation (iocos) that refines the classic Tretman's ioco. The work by Tretmans [START_REF] Tretmans | Model based testing with labelled transition systems[END_REF] has settled a solid and widespread framework in the Model Based Testing (MBT) community: it offers both offline and online [START_REF] René | On-the-fly conformance testing using spin[END_REF] testing algorithms; and there are several model-based test generation tools (e.g. [START_REF] Tretmans | Torx: Automated model-based testing[END_REF][START_REF] Belinfante | Jtorx: A tool for on-line model-driven test derivation and execution[END_REF]) that implement the iocotesting theory.

From a theoretical point of view, some interesting particularities of the iocoframework are: behaviours are modelled as labelled transition systems (LTS); quiescent states (see [START_REF] Stokkink | Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation[END_REF]) are considered; implementations should be inputenabled; and the ioco relation is a trace-based semantics, and thus a linear semantics [START_REF] Van Glabbeek | Handbook of Process Algebra, chapter The Linear Time -Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes[END_REF].

Our iocos approach shares LTS as models, quiescence, and much of the conformance philosophy, while considering a wider behaviour domain not imposing, but allowing, implementations to be input enabled. The substantial difference is that the conformance relation is an input-output simulation (iocos) -a branching semantics [START_REF] Van Glabbeek | Handbook of Process Algebra, chapter The Linear Time -Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes[END_REF]-with greater discriminatory power than ioco (see Theorem 1 below). In [START_REF] Gregorio-Rodríguez | Input-output conformance simulation (iocos) for model based testing[END_REF] we presented an offline algorithm that starting from a formal model of the specification produced a test suite to be checked against the possible implementations. We proved the resulting test suite to be sound and exhaustive for the given specification with respect to iocos.

In this paper we present an alternative approach to offline testing that avoids the generation of the whole test suite. When time or space requirements are considered, a more suitable testing approach is the so called online testing. Online testing considers a concrete implementation to be checked against the specification. It combines test generation from the specification model and test execution against the implementation. In this approach only a single step of a test is generated from the model and executed in the implementation; the results of this execution are taken into account to generate the next step in the test, that is again checked against the implementation. In order to show the applicability of our conformance relation, in this paper we define an online testing algorithm for iocos that we prove to be sound and complete.

An essential point of our conformance relation is that it is simulation-based. Simulation is an important notion pervading many fields in computer science (model checking, concurrency theory, formal verification. . . ). It is an active area of research both theoretical (e.g. [START_REF] Aceto | Axiomatizing weak simulation semantics over BCCSP[END_REF][START_REF] De Frutos-Escrig | Unifying the linear time-branching time spectrum of process semantics[END_REF][START_REF] Lüttgen | Ready simulation for concurrency: It's logical! Information and Computation[END_REF][START_REF] Fábregas | Logics for contravariant simulations[END_REF]) and practical (e.g. [START_REF] Bulychev | Efficient on-the-fly algorithm for checking alternating timed simulation[END_REF][START_REF] Ranzato | A more efficient simulation algorithm on kripke structures[END_REF]). Regarding practical implementation applications for iocos, it is particularly interesting its use in model checking minimisation ([6,14]) as a technique to overcome the state explosion problem.

The quest for efficient algorithms1 to compute this relation has been an area of active research in the last years (e.g. [START_REF] Gentilini | From bisimulation to simulation: Coarsest partition problems[END_REF][START_REF] Bulychev | Efficient on-the-fly algorithm for checking alternating timed simulation[END_REF][START_REF] Ranzato | A more efficient simulation algorithm on kripke structures[END_REF]). In [START_REF] Ranzato | A more efficient simulation algorithm on kripke structures[END_REF] you can find an excellent review of the state of the art for simulation algorithms. One of the most outstanding algorithms is the one presented in [START_REF] Gentilini | From bisimulation to simulation: Coarsest partition problems[END_REF], and subsequently corrected in [START_REF] Van Glabbeek | Correcting a space-efficient simulation algorithm[END_REF]. It is one of the fastest algorithms and quasi-optimal in space. This algorithm exploits the representation of the simulation problem as a Generalised Coarsest Partition Problem (GCPP). We show in this paper how the conformance relation iocos can be cast into an instance of the GCPP. Therefore it can be efficiently computed using the algorithm in [START_REF] Van Glabbeek | Correcting a space-efficient simulation algorithm[END_REF].

The paper is organised as follows: in Section 2 we present the essential notation, definitions and results of the iocos-theory used in the rest of the paper. In Section 3, definition and behaviour of our online testing algorithm are explained and we discuss other related online testing algorithms in the literature. Section 4 is devoted to prove that iocos is indeed a relation that can be effi-ciently computed. We use the technique of system transformation to adequate iocos to the problem definition in [START_REF] Gentilini | From bisimulation to simulation: Coarsest partition problems[END_REF]. Then we prove that this transformation holds all requirements to be computed as a GCPP. Finally in Section 5 we make a summary and advance some future research lines. In order to meet the space requirements, there is an appendix containing the more technical proofs of the paper. This appendix will be available on-line in case of acceptance of the paper.

Preliminaries

This section presents the notation used in the paper and reviews the formal framework of the iocos theory introduced in [START_REF] Gregorio-Rodríguez | Input-output conformance simulation (iocos) for model based testing[END_REF][START_REF] Llana | Ioco as a simulation[END_REF].

We consider two disjoint finite sets of actions: inputs I, initiated by the environment and annotated with a question mark, a?, b?, c? ∈ I; and outputs O, initiated by the system, and annotated with an exclamation mark, o!, u!, t! ∈ O. In many cases we want to name actions in a general sense, inputs and outputs indistinctly. We will consider the set L = I ∪ O and we will omit the exclamation or question marks when naming generic actions, x, y, z ∈ L.

A state with no output actions cannot autonomously proceed, such a state is called quiescent. Quiescence is an essential component of the ioco theory. For the sake of simplicity and without lost of generality (see for instance [START_REF] Tretmans | Model based testing with labelled transition systems[END_REF][START_REF] Stokkink | Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation[END_REF]), we directly introduce the event of quiescence as a special action denoted by δ! ∈ O into the definition of our models. Definition 1. A labelled transition system with inputs and outputs is a 4-tuple (S, I, O, -→ ) such that -S is a set of states or behaviours.

-I and O are disjoint sets of input and output actions respectively. Output action include the quiescence symbol δ! ∈ O. We define

L = I ∪ O. -- → ⊆ S × L × S.
As usual we write p x --→ q instead of (p, x, q) ∈ -→ and p x --→, for x ∈ L, if there exists q ∈ S such that p x --→ q. Analogously, we will write p x --→, for x ∈ L, if there is no q such that p x --→ q. In order to allow only coherent quiescent systems the set of transitions -→ should also satisfy:

• if p δ! --→ p then p = p . A quiescent transition is always reflexive.

• if p o! ----→ for any o! ∈ O\{δ!}, then p δ! --→ p.
A state with no (regular) outputs is quiescent.

• if there is o! ∈ O\{δ!} such that p o! --→, then p δ!
----→ . A quiescent state performs no other output action.

-A system is input-enabled if at any s ∈ S for every a? ∈ I we have s a? --→.

We denote the set of labelled transition systems with inputs and outputs just as LTS . In general we use p, q, p , q . . . for states or behaviours, but also i, i , s and s when we want to emphasise the concrete role of a behaviours as implementation or specification. We consider implementations and specifications, or, more generally, behaviours under study, as states of the same LTS .

A trace is a finite sequence of symbols of L. We will normally use the symbol σ to denote traces, that is, σ ∈ L * . The empty trace is denoted by and we juxtapose, σ 1 σ 2 , to indicate concatenation of traces. The transition relation of labelled transition systems can naturally be extended using traces instead of single actions, p σ --→ q. Next we introduce some definitions and notation frequently used in the paper. --→ }, the set of inputs of a state p.

A behaviour is deterministic when for any x ∈ L, if p x --→ p 1 and p x --→ p 2 then p 1 = p 2 ; or equivalently the set p after σ is always empty or a singleton. While some models prevent non determinism we assume and allow all kinds of non-deterministic behaviour both in specifications and implementations.

Next we recall the simulation-based formal definition of iocos.

Definition 3. Let (S, I, O, -→ ) ∈ LTS , we say that a relation R ⊆ S × S is a iocos-relation if and only if for any (p, q) ∈ R the following conditions hold:

1. ins(q) ⊆ ins(p) 2. ∀a? ∈ ins(q) if p a? --→ p then ∃q ∈ S such that q a? --→ q ∧ (p , q ) ∈ R.

∀o! ∈ outs(p) if p o!

--→ p then ∃q ∈ S such that q o! --→ q ∧ (p , q ) ∈ R.

We define the input-output conformance simulation (iocos) as the union of all iocos-relations (the biggest iocos-relation).

Additional details on iocos rationale and examples appear in [START_REF] Gregorio-Rodríguez | Input-output conformance simulation (iocos) for model based testing[END_REF], where it is also proved that iocos is a strictly finer relation than ioco. Theorem 1. [START_REF] Gregorio-Rodríguez | Input-output conformance simulation (iocos) for model based testing[END_REF] Let (S, I, O, -→ ) ∈ LTS ; then iocos ⊆ ioco. That is, for any p, q ∈ S, whenever we have p iocos q it is also true that p ioco q.

An online testing algorithm for iocos

The main goal of this section is to prove iocos as a suitable conformance relation to be used in online testing. As usual, the online testing algorithm merges test generation and execution into a single interactive process. In order to understand the notation and some ideas and key concepts behind Algorithm 1, next we recall the iocos theory of testing: test definition and test execution. Definition 4. A test is a syntactical term defined by the following BNF:

T = % | ! | T 1 ⊕ T 2 | T 1 + T 2 | x; T where x ∈ L
We denote the set of tests as T .

As usual in MBT, the environments we want to model should be able to respond at any moment to any possible output of the implementation under test. That is, tests like a?; T a? will not be accepted as valid tests, but should be completed into tests like a?; T a? + o!∈O o!; T o! . For the sake of simplicity we use i∈{1,...,n} T i as a shortcut for

T 1 + • • • + T n .
Particularly interesting is that we consider two kind of choices in the tests: the one corresponding to the + operator, with conjunctive semantics, and the ⊕ operator with a disjunctive meaning. To define how tests interacts with behaviours and what is the result of the execution of that experiment, we follow Abramsky's ideas in [START_REF] Abramsky | Observational equivalence as a testing equivalence[END_REF] and use a predicate to define the outcomes of the interaction between a test and the behaviour or implementation being tested.

s pass % = f alse s pass ! = true s pass o!; T o! = true if o! ∈ outs(s) {s pass T o! |s o! --→ s } otherwise s pass a?; T a? = f alse if a? ∈ ins(s) {s pass T a? |s a? --→ s } otherwise s pass T 1 + T 2 = s pass T 1 ∧ s pass T 2 s pass T 1 ⊕ T 2 = s pass T 1 ∨ s pass T 2
For the sake of convenience the pass predicate is inductively defined over the whole set of tests, with a simpler structural formulation, while at the end we will only be interested in valid tests.

In [START_REF] Gregorio-Rodríguez | Input-output conformance simulation (iocos) for model based testing[END_REF] we defined an algorithm (Definition 6 below) that starting from a given specification s produced a test suite T (s) of valid tests that characterised the specification with respect to the iocos conformance relation as stated in Theorem 2 below. Definition 6. Let (S, I, O, -→) ∈ LTS and p ∈ S. We denote with T (p) the set of valid tests from p by applying a finite number of recursive applications of one of the following non-deterministic choices:

1. T = ! ∈ T (p). 2. If a? ∈ ins(p), then T ∈ T (p) where T = a?; {T p a? | p a? --→ p a? } + o!∈outs(p) o!; {T p o! | p o! --→ p o! } + o!∈O o! ∈outs(p) o!; % 3. If ins(p) = ∅ then T ∈ T (p) where T = o!∈outs(p) o!; {T p o! | p o! --→ p o! } + o!∈O o! ∈outs(p) o!; %
In all cases the tests T p are chosen non-deterministically from the set T (p),

T δ (p) = ! if p δ! --→, and T δ! (p) = % otherwise.
Theorem 2.

[12](Completeness) Let (S, I, O, -→) ∈ LTS and p, q ∈ S, T ∈ T (p) : q pass T iff q iocos p.

Online Algorithm Offline generation of test leads to a massive test suite. 2 This is not surprising given that the test suite should be able to prove and disprove the conformance with any possible implementation. Online testing, on the contrary, considers a concrete implementation under test (IUT) and, therefore, the testing process can be guided by the mutual interaction.

The online testing algorithm for iocos is defined in Algorithm 1. This algorithm somehow merges the test generation and execution (Definition 5 and 6), and it considers only the necessary continuations by taking into account the current state of the specification and the last response from the implementation.

Algorithm 1 starts with a specification, an IUT, and a desired number of iterations (parameters s, IUT and maxIter in function TE). The testing process will continue until a % verdict is found, indicating IUT does not conform s, or until the number of iterations has been reached without a faulty behaviour found in IUT.

According to Definition 5 the testing process will yield a % verdict on these cases: a mandatory input is rejected by IUT or an unexpected output by IUT is registered by the tester. In Algorithm 1, the first situation is solved in the first conditional inside the first case statements in function TE REC (lines 16 and 17). Let us note that to check the enabled actions in IUT (line 16), is equivalent to check condition 1 in Definition 3 (iocos).

Otherwise, if the action that the test chooses to offer is actually enabled in the IUT, the stimulus is sent to the implementation (line 18) and then condition Algorithm 1 Online Testing Algorithm for iocos There are in the literature of MBT two essential works we can relate Algorithm 1 with. In [START_REF] René | On-the-fly conformance testing using spin[END_REF] de Vries and Tretmans presented an online algorithm for ioco that is non-deterministic and even termination is one of the non-deterministic choices. In [START_REF] Kim Guldstrand Larsen | Online testing of real-time systems using UPPAAL[END_REF] Larsen et al. describe an online algorithm for an ioco-based conformance relation extended with real time and considering a concrete environment, namely rtioco e . Algorithm 1 is more similar in form to that on [START_REF] Kim Guldstrand Larsen | Online testing of real-time systems using UPPAAL[END_REF] and share with it the reset clause and the explicit use of the number of iterations. We do not consider explicit environments but the most general possible environment. 3As in [START_REF] René | On-the-fly conformance testing using spin[END_REF][START_REF] Kim Guldstrand Larsen | Online testing of real-time systems using UPPAAL[END_REF], quiescence detection can be implemented with a timeout.

In [START_REF] Veanes | Online testing with model programs[END_REF] you can find a practical online testing algorithm that is implemented in the MBT tool developed at Microsoft Research called Spec Explorer. The framework and the approach are somehow different: they use interface automaton as the specification model and assume the implementation to be in the domain of the specifications. In this work soundness and completeness are not even mentioned.

Soundness and Completeness

The rest of this section is devoted to prove that Algorithm 1 is indeed sound and complete.

In [START_REF] René | On-the-fly conformance testing using spin[END_REF] correctness of the online algorithm for ioco is stated under fairness assumptions (weather conditions [START_REF] Milner | A Calculus of Communicating Systems[END_REF]) in the non-deterministic choices. In [START_REF] Kim Guldstrand Larsen | Online testing of real-time systems using UPPAAL[END_REF] online algorithm for rtioco e is proved to be sound and complete assuming the classic test hypothesis,4 fairness in the randomisation of algorithm choices, and deterministic IUT.

In our model, we allow both implementations and specifications to behave non-deterministically and, as usual, we assume fairness in the non-deterministic choices and the test hypothesis ( [START_REF] René | On-the-fly conformance testing using spin[END_REF][START_REF] Kim Guldstrand Larsen | Online testing of real-time systems using UPPAAL[END_REF]). Test hypothesis assumes that any IUT can be modelled in the domain of LTS . Proof. The proof proceed by induction on the parameter n of TE(s, i, n), following the ideas commented in the algorithm explanation.

Asserting completeness implies that, for any faulty implementation of a given specification s, the online testing process in Algorithm 1 should eventually yield a % result, that is, the algorithm should drive the computation through a test passed by the specification and failed by the implementation. Let us note that a key point to prove the completeness is to assure that all states in the specification and implementation should be inspected. This is where the fairness requirement is needed: every infinitely often eligible action is eventually executed. To ensure this possibility one of the choices of the algorithm is to reset the IUT and to restart the algorithm (lines 37 and 38). Moreover, assuming the fairness hypothesis also implies that the number of times required to ensure that all states have been checked is not known a priori. So the number of iterations appearing in Proposition 1 and Theorem 1 cannot be determined at the beginning of the execution.

Proposition 1. Let (S, I, O, -→ ) be a LTS , let i, s ∈ S, and let T ∈ T (s) be a test such that s pass T and i / pass T . Then there exist n, n ∈ N such that TE REC (s, i, n) returns % , n .

Proof. We make the proof by induction on the depth of T . The case base is when T = ! that is trivial since i pass T . According to Definition 6, there are two cases. We are going to consider the test

T = a?; {T s a? | s a? --→ s a? } + o!∈outs(s) o!; {T s o! | s o! --→ s o! } + o!∈O o! ∈outs(s) o!; %
The other case is simpler than this one. Since i / passT , there are three possibilities to make the test fail:

1. i / pass a?; {T s a? | s a? --→ s a? }. Since we are assuming the fairness hypothesis, by choosing an arbitrary high n the choice in line 15 of the algorithm will eventually choose the action a?. If a? is not enabled in i, then the algorithm returns % in line 17. Otherwise the algorithm sends a? to the implementation. Again, by the fairness hypothesis the implementation, eventually will go to a state i such that i / pass {T s a? | s a? --→ s a? }. Let us name n i the number of iterations needed to reach this state. On the other hand, since s pass T , s pass {T s a? | s a? --→ s a? } for any s ∈ s after a?. So by induction hypothesis for any s ∈ s after a? there exist n s ∈ N such that TE REC (s , i, n s ) returns % . So by choosing n 0 ≥= n i + s ∈saftera? n s , there exists n such that the TE REC (s, i, n 0 ) returns % , n . o!; % . In this case there is o! ∈ O such that i produces output o!. By the fairness hypothesis the implementation will produce this output an the algorithm will return % in line 29.

i

Since the main function of the algorithm just makes calls to the recursive algorithm as a corollary we get the following result:

iocos as a Generalised Coarsest Partition Problem

Milner in [START_REF] Milner | An algebraic definition of simulation between programs[END_REF] introduced the preorder relation called simulation. Simulation equivalence strongly preserves ACTL * , and also strongly preserves LTL and ACTL as sublogics of ACTL * [START_REF] Bustan | Simulation-based minimization[END_REF]. Both ACTL and LTL are widely used for model checking in practice.

Simulation is a close relative of the well known bisimulation equivalence [START_REF] Milner | Communication and Concurrency[END_REF]. Bisimulation equivalence can be fast computed by reducing it to the problem of determining the coarsest partition of a set stable with respect to a given relation [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF]. An equivalent result for computing simulation as a generalised coarsest partition problem (GCPP) was given in [START_REF] Gentilini | From bisimulation to simulation: Coarsest partition problems[END_REF] and corrected in [START_REF] Van Glabbeek | Correcting a space-efficient simulation algorithm[END_REF]. This algorithm keeps a very good time complexity while its space complexity can be considered minimal.

Although iocos definition is simulation-like, it has particularities inherited from the classic requirements for the conformance relations when dealing with inputs and outputs, and even the use of input-output actions is not symmetric in the definition. Therefore, the applicability of simulation algorithms to compute iocosis not straightforward.

We will show in this section that fortunately we can compute iocos by using any algorithm that solves the GCPP. To achieve this goal, first we will show how to transform the LTS into graphs and partitions as defined in [START_REF] Gentilini | From bisimulation to simulation: Coarsest partition problems[END_REF][START_REF] Van Glabbeek | Correcting a space-efficient simulation algorithm[END_REF]. Then we will define the relation g-iocos (graph-iocos) in the transformed LTS that will be equivalent to iocos. Finally, we will formally prove that the transformed LTS holds the conditions of the GCPP.

Transforming an LTS into a graph

The GCPP in [START_REF] Gentilini | From bisimulation to simulation: Coarsest partition problems[END_REF] is defined in terms of graphs. These graphs have no labels in the edges. The objective is to transform an LTS into a graph without actions and without loosing information. The idea to achieve this is to encode the action associated to a transition into the states of the graph. So the states of the associated graph of an LTS will be pairs: the first component of the pair refers to a state of the LTS whereas the second component is the action needed to reach this state.

One of the details that we have to deal with to transform iocos into a simulation is that in Definition 3 (iocos) the implementation is allowed to introduce unspecified behaviour. We do not need to take into account those states reached by implementation when input actions are not present in the specification. To overcome this situation, in the transformed system, we need to represent these states by adding a sort of new magic state, that we denote by the symbol * . Such a state has the next property: every possible implementation will fulfil it. Moreover, in the transformation we will embed the transition action symbol into the state itself. Exceptionally, and just for the sake of uniformity, a new action symbol (•) is used for states with no incoming transitions. Definition 7. Let L = (S, I, O, -→) be a labelled transition system. We define its transformed graph as T(L) = (N, = ⇒ ) where N = (S ∪ { * }) × (L ∪ {•}) and = ⇒ is defined by the following rules.

s y --→ s (s, x) = ⇒ (s , y) , s a? ----→ (s, x) = ⇒ ( * , a?) , ( * , x) = ⇒ ( * , y) , s, s ∈ S x, y ∈ L ∪ {•}, a? ∈ I
The nodes of N will be denoted by the letters n, n 1 , n 2 , etc. Since these nodes come from states of the original labelled transition system, we annotate the arcs of the graph with the action of the target node for readability In this way will write n 1

x == ⇒ n 2 whenever n 1 = ⇒ n 2 and there is s 2 ∈ S such that n 2 = (s 2 , x).

Following the same rationale we adapt the definition of the function ins: ins( * , x) = ∅ and ins(s, x) = ins(s) if s ∈ S. Definition 8. Let (N, ⇒) be the transformed graph of an L ∈ LTS , a relation R ⊆ N ×N is g-iocos simulation iff for any n 1 , n 2 ∈ N, (n 1 , n 2 ) ∈ R the following conditions hold:

1. n 1 = (s 1 , x), n 2 = (s 2 , y) and x = y. 2. ins(n 2 ) ⊆ ins(n 1 ) 3. for all a ∈ L, if n 1 a == ⇒ n 1 then exists n 2 such that n 2 a = = ⇒ n 2 and n 1 Rn 2 .
For n 1 , n 2 ∈ N , we say that n 1 g-iocos n 2 if there exists a g-iocos simulation R such that (n 1 , n 2 ) ∈ R.

At a first glance, g-iocos is defined as a kind of ready simulation preorder [START_REF] Bloom | Bisimulation can't be traced[END_REF]. Next, we show that computing g-iocos over graphs is equivalent to compute iocos on LTS. Proposition 2 describes how to transform a concrete iocos-simulation into a g-iocos-simulation, while Proposition 3 presents the reciprocal transformation. Finally, Theorem 5 is a corollary of the previous results showing iocos and g-iocos to be two different formulations for the same semantics in two different domains.

Proposition 2. Let L = (S, I, O, - → ), let T(L) = (N, = ⇒ ) be its transformed graph, let R be iocos relation R ⊆ S × S, and let R ⊆ N × N defined as R = ((i, a), (s, a)|(i, s) ∈ R, ∀a ∈ L∪{•} ∪ (i, a)( * , a)| a ∈ L∪{•}, i ∈ S ∪{ * } Then R is a g-iocos simulation.
Proof. Let us take (n 1 , n 2 ) ∈ R and check that R holds the statements of Definition 8. --→ i and n 1 = (i , x). Since R is a iocos simulation, then there exists s such that s a --→ s and (s, s ) ∈ R. Again, by the construction of the transitions n 2 = (s, a)

x = = ⇒ (s , x) = n 2 and (n 1 , n 2 ) ∈ R by definition of R . If x ∈ I
there are two possibilities: either x ∈ ins(i) or x ∈ ins(i). In the first case we have (i, a) x --→ ( * , a) = n 1 by the way transitions are defined. Since R is an iocos simulation ins(s) ⊆ ins(i) and therefore x ∈ ins(s). Then n 2 = (s, a)

x == ⇒ ( * , x) = n 2 and (n 1 , n 2 ) ∈ R . In the second case there exists i such that i x --→ i . If x ∈ ins(s), since R is an iocos simulation there exists s such that s x --→ s and and (s, s ) ∈ R. By the construction of the transitions n 2 = (s, a) = = ⇒ n 2 . Since b? ∈ ins(s), s = * , so s ∈ S. Finally, by definition of, R we obtain (i , s ) ∈ R.

x == ⇒ (s , x) = n 2 and (n 1 , n 2 ) ∈ R by definition of R . If x ∈ ins(s), then (s, a) x --→ ( * , x) = n 2 . Then (n 1 , n 2 ) ∈ R by definition of R Proposition 3. Let L = (S, I, O, - → ) be a labelled transition system, let T(L) = (N, = ⇒ ) be its transformed graph, let R ⊆ N × N be a g-iocos relation, and let R ⊆ S × S defined as R = {(i, s)|∃a ∈ L ∪ {•}. ((i, a), (s, a)) ∈ R ∧ i, s ∈ S}. Then R is a iocos simulation.
-The case when o! ∈ outs(i) and i o! --→ i is similar to the previous one, but in this case s = * because o! ∈ I.

Finally, we obtain the theorem that relates iocos and g-iocos. This theorem is a corollary of the previous Proposition 2 and 3.

Theorem 5. Let L = (S, I, O, -→ ) be a labelled transition system and T(L) = (N, = ⇒ ) its transformed graph. Then, for any s 1 , s 2 ∈ S, we have (s 1 , s 2 ) ∈ iocos if and only if ((s 1 , x), (s 2 , x)) ∈ g-iocos ∀x ∈ L.

g-iocos as a GCPP problem

To conclude this section we will show that g-iocos can be seen as an instance of the GCPP. In order to make the paper self-contained, we are going to reproduce in condensed form definitions from [START_REF] Gentilini | From bisimulation to simulation: Coarsest partition problems[END_REF]. We write α = ⇒ ∀ β iff ∀a ∈ α we have a = ⇒ b for some b ∈ β. 4. We say that S, is stable with respect to = ⇒ iff

∀α, β, γ ∈ S if (α, β) ∈ ∧α = ⇒ ∃ γ then ∃ ∈ S : (γ, ) ∈ ∧β = ⇒ ∀ 5.
Let S 1 , 1 and S 2 , 2 be partition pairs. We say that S 1 , 1 is a refinement of S 2 , 2 , written S 1 , 1 S 2 , 2 , if S 1 is finer than S 2 , i.e., (∀α ∈ S 1 ∃α ∈ S 2 : α ⊆ α ) and 1 ⊆ 2 (S 1 ) where 2 (S 1 ) is the induced relation on S 1 by 2 : (α, β) ∈ 2 (S 1 ) iff there exist α , β ∈ S 2 such that α ⊆ α , β ⊆ β and (α , β ) ∈ 2 . 6. Let us consider a pair S, , the Generalised Coarsest Partition Problem (GCPP) for S, consists in finding a partition pair S 0 , 0 such that: a) S 0 , 0 S , b) S 0 , 0 is stable respect to = ⇒ , and c) S 0 , 0 is maximal fitting a) and b). Now we are ready to set up our key concepts in order to embed iocos computation into GCPP problem via a g-iocos reduction.

Definition 10. Let L = (S, I, O, -→ ) be a labelled transition system and T(L) = (N, = ⇒ ) its transformed graph. We write ≡ g-iocos for the kernel of g-iocos, that is (a, b) ∈≡ g-iocos iff (a, b) ∈ g-iocos and (b, a) ∈ g-iocos.

Since ≡ g-iocos is an equivalence relation, it induces the partition N/ ≡ g-iocos . In this partition we can define g-iocos as the natural relation induced by g-iocos in N/ ≡ g-iocos , namely, for

n 1 , n 2 ∈ N , ([n 1 ] g-iocos , [n 2 ] g-iocos ) ∈ g-iocos iff (n 1 , n 2 ) ∈ g-iocos.
Let us note, that g-iocos is reflexive and acyclic in N/ ≡ g-iocos , so N/ ≡ g-iocos , g-iocos is a partition pair. So, the rest of this section is devoted to prove that the partition N/ ≡ g-iocos , g-iocos can be solved with any algorithm that solves the GCPP. In order to do it we need to define an initial partition pair Ω, such that N/ ≡ g-iocos , g-iocos Ω, .

Definition 11. Let L = (S, I, O, -→ ) be a labelled transition system and T(L) = (N, = ⇒ ) its transformed graph.

-We define the partition Ω = {α 1 , α 2 , . . . α n } ⊆ P(N ) as follows: (n 1 , n 2 ) ∈ α i if and only if n 1 = (s 1 , x), n 2 = (s 2 , y), ins(s 2 ) = ins(s 1 ) and x = y. -We define the relation

⊆ Ω × Ω as [n 1 ] Ω [n 2 ] Ω iff n 1 = (s 1 , x)
, n 2 = (s 2 , y), ins(s 2 ) ⊆ ins(s 1 ) and x = y. Lemma 1. Let L = (S, I, O, -→ ) be a labelled transition system and its transformed graph T(L) = (N, = ⇒ ). Then N/ ≡ g-iocos , g-iocos Ω, .

Proof. This lemma is immediate because of the definition of g-iocos-simulation, kernel ≡ g-iocos and the induced partition pair N/ ≡ g-iocos , g-iocos .

Lemma 2. Let L = (S, I, O, -→ ) be a labelled transition system and its transformed graph, T(L) = (N, = ⇒ ), then the partition pair N/ ≡ g-iocos , g-iocos is stable with respect to = ⇒ .

Proof. Let us consider equivalence classes [n

1 ] g-iocos , [n 2 ] g-iocos , γ ∈ N/ ≡ g-iocos such that ([n 1 ] g-iocos , [n 2 ] g-iocos ) ∈ g-iocos and [n 1 ] g-iocos = ⇒ ∃ γ. Then there exists n 1 ∈ γ and x ∈ L such that n 1 x = = ⇒ n 1 . As (n 1 , n 2 ) ∈ g-iocos there exists n 2 such that n 2 x == ⇒ n 2 and ([n 1 ] g-iocos , [n 2 ] g-iocos ) ∈ g-iocos .
Let us consider n 2 a maximal element with respect to g-iocos, i.e, for any n i such that (n 1 , n i ) ∈ g-iocos we have (n i , n 2 ) ∈ g-iocos .

Next we will prove that

[n 2 ] = ⇒ ∀ [n 2 ]. Let us consider n 3 ∈ [n 2 ]
. Since they belong to the same ≡ g-iocos class, the equivalence kernel makes true (n 2 , n 3 ) ∈ g-iocos . Therefore there exists n 3 such that n 3 x = = ⇒ n 3 and (n 2 , n 3 ) ∈ g-iocos. Again, (n 3 , n 2 ) ∈ g-iocos, there exists n 2 such that n 2 x = = ⇒ n 2 and (n 3 , n 2 ) ∈ g-iocos. Since g-iocos is transitive we obtain (n 2 , n 2 ) ∈ g-iocos. Since n 2 was a maximal element then n 2 = n 2 and then n

3 ∈ [n 2 ].
We also need to show that N/ ≡ g-iocos , g-iocos is maximal with respect to the points a) and b) of the GCPP. In order to do it, first let us note that any partition pair S, induces a natural relation in N that we will denote by (N ). Definition 12. Let L = (S, I, O, -→ ) be a labelled transition system and T(L) = (N, = ⇒ ) its transformed graph, and let S, be a partition pair. We define the relation

(N ) ⊆ N × N as (n 1 , n 2 ) ∈ (N ) iff ([n 1 ] S , [n 2 ] S ) ∈ . Second, if S,
satisfies the points a) and b) of the GCPP for the partition pair Ω, , then the following lemma states that (N ) is a g-iocos-simulation. Lemma 3. Let L = (S, I, O, -→) be a labelled transition system and T(L) = (N, = ⇒ ) its transformed graph, and let S, be a refinement of Ω, such that is stable with respect to = ⇒ . Then (N ) is a g-iocos-simulation.

Proof. Let us consider (n 1 , n 2 ) ∈ N ( ). Since S, is a refinement of Ω, , we obtain ([n 1 ] Ω , [n 2 ] Ω ) ∈ .
Then n 1 has the form (s 1 , x), and n 2 has the form (s 2 , y) with x = y and ins(n 2 ) ⊆ ins(n 1 ), hence fulfilling 1 of Definition 8. Now let us consider x ∈ L and n 1 ∈ N such that n 1 x = = ⇒ n 1 . By rewriting all those elements at coarse level in S we obtain (

[n 1 ] S , [n 2 ] S ) ∈ and [n 1 ] S = ⇒ ∃ [n 1 ] S . Since S, is stable there exists δ ∈ S such that [n 2 ] S = ⇒ ∀ δ and ([n 1 ] S , δ) ∈ . At discrete level that means there exists n 2 ∈ δ such that n 2 = ⇒ n 2 . Since S, is a refinement of Ω, , we obtain ([n 1 ] Ω , [n 2 ] Ω ) ∈ . Since n 1 x == ⇒ n 1 ,
then n 1 has the form (s 1 , x) (see transformation rules in Definition 7). By the definition of Ω (Definition 11), then n 2 has also the form (s 2 , x). Therefore n 2 x == ⇒ n 2 . Now Since g-iocos is the maximal g-iocos-simulation, we obtain that (N ) ⊆ g-iocos. From this fact is easy to prove the following lemma. Finally, we obtain the main theorem of this section. Theorem 6. Let L = (S, I, O, -→ ) be a labelled transition system and T(L) = (N, = ⇒ ) its transformed graph, then N ≡ g-iocos , g-iocos is the solution of the GCPP for the partition pair Ω, .

Proof. The points a) and b) of the GCPP follows from Lemmas 1, and 2. The maximality follows from Lemmas 3 and 4.

Conclusions and Future Work

In this paper we have defined an online algorithm that allows to check if a certain implementation iocos-conforms a given specification by interacting with it and without computing any a priori set of tests. Under fairly standard hypothesis -even weaker than in other models-we prove the algorithm to be sound and complete.

We plan to introduce test selection criteria and coverage in the iocos-theory. This technique is mainly used in offline testing but we think that implementations of the online algorithm we have presented can also benefit from them to further restrict the search tree.

Since iocos is a branching semantics, it is essential in the online algorithm to make use of the copy clause (see for instance [START_REF] Abramsky | Observational equivalence as a testing equivalence[END_REF] for a more elaborated discussion). While this copy capability will exclude some systems to being tested with iocos -essentially unique systems that cannot be replicated-for a vast number of applications, for instance to check software products, it could definitely be a feasible operation. The implementation of our online algorithm is currently under development using cluster computing techniques.

In this paper we have also proved that the conformance relation iocos, in spite of its particularities and asymmetry with input and output actions, can be solved with the GCPP. Actually, we are adapting the mCRL2 toolset [START_REF] Sjoerd Cranen | An overview of the mcrl2 toolset and its recent advances[END_REF], that implements one of the best solution to the GCPP [START_REF] Van Glabbeek | Correcting a space-efficient simulation algorithm[END_REF], to compute iocos and the minimised LTS for a give specification. This technique, frequently used in model checking, allows to reduce the size of the models and therefore the state explosion in any further testing process. Moreover, we plan to investigate the logic preservation properties of iocos that would allow to perform model checking of the intended model specifications and integrate MBT and model checking in the same theory.

Finally, once the ground model has proved to be useful, we plan to improve the expressiveness introducing a syntax language and integrating internal τ actions.

Definition 2 .

 2 Let (S, I, O, -→ ) ∈ LTS , and p ∈ S, we define: 1. p after σ = {p | p ∈ S, p σ --→ p }, the set of states after the trace σ. 2. outs(p) = {o! | o! ∈ O, p o! --→ }, the outputs of a state p (it may include δ!). 3. ins(p) = {a? | a? ∈ I, p a?

Definition 5 .

 5 Let (S, I, O, -→ ) ∈ LTS , s ∈ S, a? ∈ I, and o! ∈ O, we inductively define the predicate pass ⊆ S × T as follows:

Theorem 3 .

 3 Let (S, I, O, -→ ) be a LTS , let i, s ∈ S, and n ∈ N. If the function call TE(s, i, n) in Algorithm 1 returns a % , then i / iocos s.

Theorem 4 .

 4 Let (S, I, O, -→) be a LTS , let i, s ∈ S. If i / iocos s then there exist n ∈ N such that the function call TE(s, i, n) in Algorithm 1 returns % .

n 2 = 1 x= = ⇒ n 1 .

 211 ( * , a). i.e., we are in the second subset of R . Trivially we have ins(n 1 ) ⊇ ∅ = ins(n 2 ) (statement 2 of Definition 8). As ( * , x) = ⇒ ( * , y) for any x, y ∈ L and (n 1 , ( * , a)) ∈ R for any n 1 , then statement 3 of Definition 8 holds. n 1 = ( * , a). As R is defined, n 2 = ( * , a), and it is solved as in the previous case. n 1 = ( * , a) and n 2 = ( * , a). Let us assume that n 1 = (i, a) and n 2 = (s, a). Since R is an iocos simulation, we obtain ins(n 1 ) = ins((i, a)) = ins(i) ⊇ ins(s) = ins((s, a)) = ins(n 2 ) (statement 2 of Definition 8). Now let us take action x ∈ L such that n If x ∈ O then we obtain that there exist i such that i x

  Proof. Let (i, s) ∈ R. By construction of R, there exists a ∈ L and n 1 = (i, a) and n 2 = (s, a) such that (n 1 , n 2 ) ∈ R . Since R is a g-iocos simulation, we have ins(i) = ins((i, a)) = ins(n 1 ) ⊇ ins(n 2 ) = ins((s, a)) = ins(s) according to the statement 1 of the definition of iocos. Now let us check the other two conditions: -Let us consider b? ∈ ins(s) such i b? --→ i , so (i, a) b? = = ⇒ (i , b?). Since R is a g-iocos simulation there exists n 2 = (s , b?) such that n 2 b?

Definition 9 .

 9 Let L = (S, I, O, -→ ) be a labelled transition system and T(L) = (N, = ⇒ ) its transformed graph.1. A partition pair is a tuple S, such that S = {α, β, . . . } is a partition of N and is a reflexive and acyclic relation on S. 2. Let S be a partition and let n ∈ N , we write [n] S as the unique element of S that contains n. 3. Let α, β ∈ S, we write α = ⇒ ∃ β iff ∃a ∈ α such that a = ⇒ g for some b ∈ β.

Lemma 4 .

 4 Let G = (N, = ⇒ ) be the transformed graph of an LTS and let S, be a partition pair such that (N ) is a g-iocos-simulation. Then S, N ≡ g-iocos , g-iocos .Proof. First let us consider α ∈ S and a, b ∈ α. Since is reflexive we obtain (α, α) ∈ and therefore (a, b) ∈ (N ) and (b, a) ∈ (N ). Now considering that (N ) ⊆ g-iocos we obtain (a, b) ∈≡ g-iocos . Therefore all elements of α are in the same equivalence class in N/ ≡ g-iocos , so S is a refinement of N/ ≡ g-iocos . Now let us consider α, β ∈ , let us consider a, b ∈ N such that [a] S = α and [b] S = β. Since (N ) ⊆ g-iocos, we obtain (a, b) ∈ g-iocos and ([a] g-iocos , [b] g-iocos ) ∈ g-iocos . Since [a] S ⊆ [a] g-iocos and [b] S ⊆ [b] g-iocos , we obtain ([a] S , [b] S ) ∈ g-iocos (S).

  By the fairness hypothesis the implementation will eventually produce that output and will go to state i . Let us name n i the number of iterations needed to reach this state. On the other hand, s pass {T s o! | s o! --→ s o! } for any s ∈ s after o!. So by induction hypothesis for any s ∈ s after o! there exist n s ∈ N such that TE REC (s , i, n s ) returns % . So by choosing n 0 ≥= n i + s ∈saftero! n s , there exists n such that the TE REC (s, i, n 0 )

	returns % , n . 3. i / pass o!∈O
	o! ∈outs(s)

/ pass o!∈outs(s) o!; {T s o! | s o! --→ s o! }. In this case there is o! ∈ outs(s) such that i produces output o! and goes to an state i such that i / pass {T s o! | s o! --→ s o! }.

As a general overview, we could say that while deciding trace inclusion on finite-state processes is PSPACE-hard[START_REF] Stockmeyer | Word problems requiring exponential time: Preliminary report[END_REF], the simulation preorder is decidable in polynomial time. Actually, simulation preorder is the coarsest preorder included in trace inclusion with this property.

in Definition

(iocos) should be tested: at least one of the descendant tests must be passed by the current state of the implementation, otherwise the final return statement outside the loop will propagate the % verdict. The copy clause (line 19) -theoretically essential, see[START_REF] Abramsky | Observational equivalence as a testing equivalence[END_REF][START_REF] Rabanal | Testing restorable systems: formal definition and heuristic solution based on river formation dynamics[END_REF]-is used to check every descendant test against the same state of the implementation. For software artifacts, and even embedded systems that can be easily replicated, this is indeed a feasible operation.In a similar way, if we focus on output actions, conditional in lines 28 and 29 detects unexpected outputs from the implementation. Otherwise, if an output received from the IUT is acceptable, the algorithm has to proceed and check condition 3 in Definition 3 (iocos) as described previously.Algorithm 1 is non-deterministic and the three cases in the choice statement (line 13) are arbitrarily chosen in every run of the function TE REC . The reset case introduces the possibility of breadth exploration of the IUT, while the other two choices produce a (one step) deep exploration.2 Of course, there is a very interesting line of research in MBT that tries to reduce the size of the test suite while keeping a good coverage.

To introduce environments might lead to a reduction of the search-space because this additional knowledge can be used to further restrict the testing process.

The behaviour of IUT can be described in the model domain. Only the existence is assumed, not a concrete and known instance.

Research partially supported by the Spanish MEC projects TIN2009-14312-C02-01 and TIN2012-36812-C02-01