Alexandre Petrenko
email: petrenko@crim.ca

Omer Nguena Timo

S Ramesh
email: ramesh.s@gm.com

Multiple Mutation Testing from FSM

Keywords: FSM, Conformance testing, Mutation testing, Fault modelling, Fault model-based test generation, Test coverage, Fault coverage analysis

Fault model based testing receives constantly growing interest of both, researchers and test practitioners. A fault model is typically a tuple of a specification, fault domain, and conformance relation. In the context of testing from finite state machines, the specification is an FSM of a certain type. Conformance relation is specific to the type of FSM and for complete deterministic machines it is equivalence relation. Fault domain is a set of implementation machines each of which models some faults, such as output, transfer or transition faults. In the traditional checking experiment theory the fault domain is the universe of all machines with a given number of states and input and output sets of the specification. Another way of defining fault domains similar to the one used in classical program mutation is to list a number of FSM mutants obtained by changing transitions of the specification. We follow in this paper the approach of defining fault domain as a set of all possible deterministic submachines of a given nondeterministic FSM, called a mutation machine, proposed in our previous work. The mutation machine contains a specification machine and extends it with a number of mutated transitions modelling potential faults. Thus, a single mutant represents multiple mutations and mutation machine represents numerous mutants. We propose a method for analyzing mutation coverage of tests which we cast as a constraint satisfaction problem. The approach is based on logical encoding and SMT-solving, it avoids enumeration of mutants while still offering a possibility to estimate the test adequacy (mutation score). The preliminary experiments performed on an industrial controller indicate that the approach scales sufficiently well.

Introduction

In the area of model based testing, one of the key questions concerns a termination rule for test generation procedures. It seems to us that there are two main schools of thought considering this rule. One of them follows a traditional approach of covering a specification model. In terms of the Finite State Machine (FSM) model, one could consider for coverage various features of an FSM, such as transitions or sequences of them which model test purposes often used to guide and terminate test generation.

Another school focuses on fault coverage and thus follows fault model based testing, see, e.g., [START_REF] Bochmann | Fault models in testing[END_REF][START_REF] Petrenko | On fault coverage of tests for finite state specifications[END_REF][START_REF] Simao | Comparing finite state machine test coverage criteria[END_REF][START_REF] Godskesen | Fault models for embedded systems[END_REF][START_REF] Cheng | A functional fault model for sequential machines[END_REF][START_REF] Petrenko | Fault model-driven test derivation from finite state models: Annotated bibliography. Modeling and verification of parallel processes[END_REF]. Fault model based testing receives constantly growing interests of both, researchers and test practitioners. Fault models are defined in the literature in a variety of ways [START_REF] Bochmann | Fault models in testing[END_REF]. In [START_REF] Petrenko | Fault models for testing in context[END_REF], we propose to define a fault model as a tuple of a specification, a fault domain, and a conformance relation. In the context of testing from finite state machines, the specification is a certain type of an FSM. A conformance relation is specific to the FSM type and for complete deterministic machines it is equivalence relation. A fault domain is a set of implementation machines, aka mutants, each of which models some faults, such as output, transfer and transition faults.

In the traditional checking experiment theory the fault domain is the universe of all machines with a given number of states and input and output alphabets of the specification, see, e.g., [START_REF] De Moura | Yices 1.0: An efficient SMT solver[END_REF][START_REF] Moore | Gedanken -Experiments on sequential machines[END_REF][START_REF] Vasilevskii | Failure diagnosis of automata[END_REF][START_REF] Chow | Testing software design modeled by finite-state machines[END_REF][START_REF] Lee | Principles and methods of testing finite-state machines -a survey[END_REF][START_REF] Vuong | A novel approach to protocol test sequence generation[END_REF]. While this theory offers clear understanding what does it mean to have sound and exhaustive, i.e., complete tests, it leads to tests whose number grows in the worst case exponentially with the FSM parameters. To us, this is a price to pay for considering the universe of all FSMs. Intuitively, choosing a reasonable subset of this fault domain might be the way to mitigate the test explosion effect. As an example, if one considers the fault domain of mutants that model output faults, a test complete for this fault model is simply a transition tour. The space between these two extreme fault models has received in our opinion insufficient attention. In what follows, we present a brief account of what has been done in this respect.

In the area of program mutation testing, mutants are generated by modifying programs. The number of tests is limited by the number of mutants, which usually need to be compared one by one with the original program to determine tests that kill them [START_REF] Demillo | Hints on test data selection: help for the practicing programmer[END_REF][START_REF] Demilli | Constraint-based automatic test data generation[END_REF]. Test minimization could then be achieved via explicit enumeration of all the mutants in the fault domain followed then by solving a set cover problem.

Mutation testing in hardware area seems to predate program mutation. An early work of [START_REF] Poage | Derivation of optimal test sequences for sequential machines[END_REF] [START_REF] Poage | Derivation of optimal test sequences for sequential machines[END_REF] focuses on hardware faults in FSM implementations and builds a fault domain by extracting FSM mutants from modified circuits. The idea of this approach is to consolidate the comparisons of individual mutants aiming at reduction of the number of tests, however, mutants still need to be analyzed one by one. The approach in [START_REF] Pomeranz | Test generation for multiple state-table faults in finite-state machines[END_REF] focuses on detection of single FSM mutations with the same test, but provides no guarantees that mutants with multiple mutations (higher order mutants) can always be killed.

Explicit mutant enumeration can be avoided by defining a fault domain as a set of all possible submachines of a given nondeterministic FSM, called a mutation machine, proposed in our previous work [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF]. The mutation machine contains a specification machine and extends it with a number of mutated transitions modelling potential faults. Mutated transitions might be viewed as faults injected in the specification machine, see, e.g., [START_REF] Rӧsch | Review of model-based testing approaches in production automation and adjacent domains -current challenges and research gaps[END_REF]. Thus, a single mutant represents multiple mutations and mutation machine represents numerous mutants. In our previous work, methods were developed for test generation using this fault model [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF]. The main idea was to adjust classical checking experiments for a fault domain smaller than the universe of all FSMs. A checking experiment once obtained is in fact a complete test suite, however, this approach does not offer a means of analyzing mutation coverage of an arbitrary test suite or individual tests.

Traditional program mutation testing uses explicit mutant enumeration to determine test adequacy or mutation score. It is a ratio of the number of dead mutants to the number of non-equivalent mutants. We are not aware of any attempt to characterize a fault detection power of tests considering multiple mutants that avoids their enumeration.

The paper aims at solving this problem. We propose a method for analyzing mutation coverage of tests which we cast as a constraint satisfaction problem. The approach is based on logical encoding and SMT-solving, it avoids enumeration of mutants while still offering a possibility to estimate the test adequacy (mutation score). The analysis procedure can be used for test prioritization and test minimization, and could eventually lead to an incremental test generation.

The remaining of this paper is organized as follows. Section 2 defines a specification model as well as a fault model. In Section 3, we develop a method for mutation coverage analysis. Section 4 reports on our preliminary experiments performed on an industrial controller. Section 5 summarizes our contributions and indicates future work. An execution of M from state s is a sequence of transitions forming a path from s in the state transition diagram of M. The machine M is initially connected, if for any state s  S there exists an execution from s0 to s. An execution is deterministic if each transition (s, x, o, s) in it is the only transition for (s, x)  S  I; otherwise, i.e., if for some transition (s, x, o, s) in the execution there exists in it a transition (s, x, o, s) such that o ≠ o or s ≠ s, the execution is nondeterministic. Clearly, a DFSM has only deterministic executions, while an NFSM can have both.

Background

Finite State Machines

A trace of M in state s is a string of input-output pairs which label an execution from s. Let TrM(s) denote the set of all traces of M in state s and TrM denote the set of traces of M in the initial state. Given sequence   (IO)*, the input (output) projection of , denoted I (O), is a sequence obtained from  by erasing symbols in O (I).

We say that an input sequence triggers an execution of M (in state s) if it is the input projection of a trace of an execution of M (in state s).

Given input sequence , let outM(s, ) denote the set of all output sequences which can be produced by M in response to  at state s, that is outM(s, ) = {O |   TrM(s) and I = }.

We define several relations between states in terms of traces of a complete FSM. We also use relations between machines. Given FSMs M = (S, s0, I, O, T) and

N = (P, p0, I, O, N), N  M if s0  p0; N ≃ M if s0 ≃ p0; N ≄ M if s0 ≄ p0.
In this paper, we use equivalence relation between machines as a conformance relation between implementation and specification machines. Given a complete initially connected NFSM M = (S, s0, I, O, T), a complete initially connected machine N = (S, s0, I, O, N) is a submachine of M if S  S and N  T. The set of all complete deterministic submachines of M is denoted Sub(M). Obviously, each machine in Sub(M) is a reduction of M; moreover, if M is deterministic then Sub(M) contains just M.

Fault Model

Let A = (S, s0, I, O, N) be a complete initially connected DFSM, called the specification machine.

Definition 1. A complete initially connected NFSM M = (S, s0, I, O, T) is a mutation machine of A = (S, s0, I, O, N), if N T, i.e., if A is a submachine of M.

We assume that all possible implementation machines for the specification machine A constitute the fault domain Sub(M), the set of all deterministic submachines of the mutation machine M of A. A submachine B  Sub(M), B ≠ A is called a mutant. Transitions of M that are also transitions of A are called unaltered, while others, in the set T \ N, are mutated transitions. Given (s, x)  S  I, we let T(s, x) denote a set of transitions from state s and input x in M. If T(s, x) is a singleton then its transition is called a trusted transition. The set T(s, x) is called a suspicious set of transitions if it is not a singleton, transitions in a suspicious set are called suspicious. Trusted transitions are present in all mutants, but suspicious transitions in each set T(s, x) are alternative and only one can be present in a deterministic mutant.

A mutant B is nonconforming if it is not equivalent to A, otherwise, it is called a conforming mutant. We say that input sequence   I* such that B ≄ A detects or kills the mutant B.

The tuple A, ≃, Sub(M) is a fault model following [START_REF] Petrenko | Fault models for testing in context[END_REF]. For a given specification machine A the equivalence partitions the set Sub(M) into conforming implementations and faulty ones. In this paper, we do not require the FSM A to be reduced, this implies that a conforming mutant may have fewer states than the specification A; on the other hand, we assume that no fault creates new states in implementations, hence mutants with more states than the specification FSM are not in the fault domain Sub(M).

Consider the following example.

Fig. 1.

A mutation machine with the specification machine as its submachine, where mutated transitions are depicted with dash lines, state 1 is the initial state.

The mutation machine M contains six suspicious transitions, one mutated transition represents output fault and the other two transfer faults. M contains eight deterministic submachines, the specification machine and seven mutants which share the same five trusted transitions.

As discussed in previous work [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF], the mutation machine formally models test hypotheses about potential implementation faults. The mutation machine M allows compact representation of numerous mutants in the fault domain Sub(M). More precisely, their number is given by the following formula:

|Sub(M)| = (s,x)SI|T(s, x)|
In the extreme case, considered in classical checking experiments a fault domain is the universe of all machines with a given number of states and fixed alphabets. The corresponding mutation machine becomes in this case a chaos machine with all possible transitions between each pair of states. The number of FSMs it represents is the product of the numbers of states and outputs to the power of the product of the numbers of states and inputs.

Mutation testing

A finite set E  I * of finite input sequences is a test suite for A. A test suite is said to be complete w.r.t. the fault model A, ≃, Sub(M) if for each nonconforming mutant B  Sub(M) it contains a test detecting B.

In the domain of program mutation testing, such a test suite is often called adequate for a program (in our case, a specification machine) relative to a finite collection of programs (in our case the set of mutants), see, e.g., [START_REF] Demilli | Constraint-based automatic test data generation[END_REF].

Differently from the classical program mutation testing, where the mutant killing tests are constructed mostly manually, in case of deterministic FSMs, tests that kill a given mutant FSM can be obtained from the product of the two machines, see, e.g., [START_REF] Poage | Derivation of optimal test sequences for sequential machines[END_REF][START_REF] Pomeranz | Test generation for multiple state-table faults in finite-state machines[END_REF][START_REF] Petrenko | Testing from partial deterministic FSM specifications[END_REF]. The problem can also be cast as model checking for a reachability property, considered in several work, see, e.g., [START_REF] Gordon | Testing with model checkers: a survey[END_REF]. This approach can also be used to check whether a given test kills mutants, but it requires mutant enumeration.

In this work, we develop an analysis approach that avoids mutant enumeration while still offering a possibility to estimate the test adequacy (mutation score).

Distinguishing automaton

Tests detecting mutants of the specification are presented in a product of the specification and mutation machines obtained by composing their transitions as follows.

 c0 = (s0, s0)  For any (s, t)  C and x  I, ((s, t), x, (s, t))  D, if there exist (s, x, o, s)  N, (t,
x, o, t)  T, such that o = oand ((s, t), x, )  D, if there exist (s, x, o, s)  N, (t, x, o, t)  T, such that o  o  (, x, )  D for all x  I.

We illustrate the definition using the specification and mutation machines in Fig. 1. Fig. 2 presents the distinguishing automaton for A and M.

The accepting state defines the language LD of the distinguishing automaton D for A and M and possesses the following properties. First, all input sequences detecting each and every mutant belong to this language. Theorem 1. Given the distinguishing automaton D for A and M, if

B ≄ A, B  Sub(M), then   LD.
Notice that for any nonconforming mutant there exists an input sequence of length at most n 2 , where n is the number of states of the specification machine, since distinguishing automaton has no more than n 2 states.

At the same time, not each and every word of the language detects a mutant. An input sequence  LD triggers several executions in the distinguishing automaton D which are defined by a single execution in the specification machine A and some execution in the mutation machine M both triggered by . The latter to represent a mutant must be deterministic. Such a deterministic execution of the mutation machine M defining (together with the execution of A) an execution of the distinguishing automaton D to the sink state is called -revealing. Input sequences triggering revealing executions enjoy a nice property of being able to detect mutants.

Theorem 2. Given an input sequence   I* such that  LD, an -revealing execution includes at least one mutated transition, moreover, each mutant which has this execution is detected by the input sequence .

Given an input sequence  LD, the question arises how all the mutants (un)detected by this input sequence can be characterized. We address this question in the next section.

Mutation coverage analysis

Consider an input sequence   I* which detects a nonconforming mutant by triggering -revealing executions. Analyzing these executions we can determine all mutated transitions involved in each of them. This analysis can performed by using a distinguishing automaton constrained to a given input sequence. Let   I* and Pref() be the set of all prefixes of . We define a linear automaton (Pref(), , I, D), such that each prefix of  is a state, and (, x, x)  D if x  Pref(). We illustrate the definition using the input sequence  = baaba for the specification and mutation machines in Fig. 1. Notice that the sequence hits all the mutated transitions in the mutation machine. The resulting -distinguishing automaton for A and M is shown in Fig. 3. The suspicious transitions are in bold. The executions are deterministic and include two mutated transitions (3, a, 1, 3) and (3, b, 0, 3). The third mutated transition (4, a, 1, 2) is in the execution that does not lead to the sink state ∇. Hence, the input sequence baaba detects any mutant with two out of three mutated transitions.

 c0 = (,
The example indicates that -distinguishing automata for the specification and mutation machines provide a suitable means for mutation analysis of a given test suite. Before we formulate a method for such an analysis, we consider yet another example of -distinguishing automata with  = babaaba. The executions of the automaton in Fig. 4 leading to the sink state define the following executions of the mutation machine: The executions 3, 5, 6 and 8 are nondeterministic in the mutation machine, since each of them has both unaltered and mutated transitions for the same pair of state and input.

1. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 3)(3, a, 0, 3) 2. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 3)(3, a, 1, 3)(3, a, 1, 3) 3. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 3)(3,
Consider the first execution, it involves two suspicious transitions, mutated transition (3, b, 0, 3) and unaltered transition (3, a, 0, 3). The prefix baba of the input sequence babaaba detects any mutant in which unaltered transition (3, b, 0, 4) is replaced by the mutated one (3, b, 0, 3) and the suspicious transition (3, a, 0, 3) is left unaltered. Let B be a set of transitions of a mutant B  Sub(M).

A mutant B is then detected by the input sequence babaaba or its prefix if its set of transitions B satisfies at least one of the following constraints on suspicious transitions: As stated above any mutant with the transition relation satisfying one of these constraints is detected by the input sequence babaaba or its prefix, since a wrong output sequence should be produced by such a mutant. On the other hand, a mutant that does not satisfy any of them escapes detection by this input sequence. To characterize these mutants, we formulate constraints which exclude all the executions of detected mutants by considering the negation of the disjunction of the constraints for all the triggered revealing executions. The resulting constraint becomes a conjunction of negated constraints of the executions.

For instance, the negated first constraint is (3, b, 0, 3)  B or (3, a, 0, 3)  B. This reads that the unaltered transition (3, b, 0, 4) or mutated transition (3, a, 1, 3) must be present. The constraint (3, b, 0, 3)  B is equivalent to (3, b, 0, 4)  B; similarly, (3, a, 0, 3)  B is equivalent to (3, a, 1, 3)  B. We have that the negated constraint is (3, b, 0, 4)  B or (3, a, 1, 3)  B.

To formalize the above discussions we cast the execution analysis as a constraint satisfaction problem by using auxiliary variables to specify the choices between suspicious transitions. Let T1, T2, …, Tm be the sets of suspicious transitions, where unaltered transitions are the first elements and the remaining elements of each set are lexicographically ordered. We introduce auxiliary variables z1, z2, …, zm, such that variable zi represents the suspicious set Ti. For the variable zi the domain is Di = {1, 2, …, |Ti|}, such that zi = 1 represents the unaltered transition in the set Ti and the other values correspond to mutated transitions. We use conditional operators {=, } and logical operators AND () and OR () for constraint formulas.

Each execution of a mutation machine that involves suspicious transitions yields assignments on variables representing these transitions, which expresses a constraint formula as the conjunction of individual assignments (zi = c), where c  Di. Then the negated constraint formula becomes the disjunction of individual constraints (zi  c).

A set of revealing executions triggered by one or more input sequences is then the conjunction of disjunctions of individual constraints.

In our example, the sets of suspicious transitions are

T1(3, a) = {(3, a, 0, 3), (3, a, 1, 3)}, T2(3, b) = {(3, b, 0, 4), (3, b, 0, 3)} and T3(4, a) = {(4, a, 1, 1), (4, a, 1, 2)}.
Each of these sets define two values of variables z1, z2 and z3, where the value 1 of each variable represents a corresponding unaltered transition.

The constraint formula becomes:

((z2  2)  (z1  1))  ((z2  2)  (z1  2))  ((z2  2)  (z1  2)  (z1  1)  (z2  1)  (z3  1))  ((z2  1)  (z3  2))  ((z2  1)  (z3  2)  (z3  1))  ((z2  2)  (z1  2)  (z1  1))  ((z2  1)  (z3  2)  (z1  2))  ((z2  2)  (z1  2)  (z1  1)  (z2  1)  (z3  2)).
Clearly, the formula always has a solution where values of variables determine unaltered transitions representing a specification machine, but we need a solution if it exists which has at least one mutated transition. To this end, we add the constraint (z1  1)  (z2  1)  (z3  1) excluding the solution defining the specification machine.

The final constraint formula is

((z2  2)  (z1  1))  ((z2  2)  (z1  2))  ((z2  2)  (z1  2)  (z1  1)  (z2  1)  (z3  1))  ((z2  1)  (z3  2))  ((z2  1)  (z3  2)  (z3  1))  ((z2  2)  (z1  2)  (z1  1))  ((z2  1)  (z3  2)  (z1  2))  ((z2  2)  (z1  2)  (z1  1)  (z2  1)  (z3  2))  ((z1  1)  (z2  1)  (z3  1)).
To solve it, we use the SMT solver Yices [START_REF] De Moura | Yices 1.0: An efficient SMT solver[END_REF] which finds the solution (z1 = 2), (z2 = 1), (z3 = 1). The solution defines a mutant with the single mutated transition (3, a, 1, 3). The mutant is nonconforming, which can be verified with the help of a distinguishing automaton obtained for the specification machine and the mutant. This means that the input sequence babaaba does not detect the mutant defined by the solution. To ensure its detection we have two options, to add a new input sequence or to try to extend the input sequence babaaba until it detects the remaining mutant. The latter option avoids using the reset operation in testing, required in the former option.

Following the first option we notice that the input sequence which detects the escaped mutant is baa already obtained in the example of the -distinguishing automaton in Fig. 3, where = baaba. Considering the revealing execution (1, b, 0, 2)(2, a, 0, 3)(3, a, 1, 3) triggered by its prefix baa, we generate an additional constraint (z1  2) which prevents the suspicious transition (3, a, 1, 3) to be chosen and add it to the final constraint formula which has no solution. The set {babaaba, baa} is therefore a complete test suite for the specification machine A and mutation machine M in Fig. 1.

Following the second option, we find that it is possible to extend the input sequence babaaba which leaves the specification machine in state 3 with the input a to detect the mutated transition (3, a, 1, 3). As before, we add constraint (z1  2) and the final constraint has no solution. The set {babaabaa} is also a complete test suite.

This example indicates that various test generation strategies could be investigated, complementing checking experiments and checking sequences approaches. The latter allows one to avoid using multiple resets in testing. Notice that a classical checking experiment for this example derived by using, e.g., the W-method [START_REF] Vasilevskii | Failure diagnosis of automata[END_REF][START_REF] Chow | Testing software design modeled by finite-state machines[END_REF], contains many more input sequences, moreover, the specification machine in Fig. 1 has no distinguishing sequence, which is usually required to generate a checking sequence. By this reason the existing methods cannot construct a single test, however, the example indicates that the mutation analysis allows us to do so. We leave the detailed elaboration of a test generation method for future work and formulate in this paper a procedure for mutant coverage analysis.

The procedure uses as inputs a test suite TS for a specification machine A and mutation machine M and consists of the following steps:

1. For each input sequence   TS (a) Determine the -distinguishing automaton (b) Find all executions leading to the sink state (c) Determine -revealing executions of the mutation machine (d) Build the disjunction of constraints excluding the -revealing executions 2. Build the conjunction of the obtained disjunctions and add the constraint that excludes the solution defining the specification machine 3. Solve the constraint formula by calling a solver 4. If it finds no solution terminate with the message "TS is complete", otherwise check whether the mutant defined by a solution is conforming 5. If it is nonconforming terminate with the message "TS is incomplete", otherwise add the constraint that excludes the solution defining the conforming mutant and go to Step 3.

The main steps of the procedure have already been discussed and illustrated on the examples, except of the last two steps which deserve more explanation. Constraint solvers normally provide a single solution if it exists. An extra constraint prevents the solution to point to just the specification machine, but the found solution may correspond to a conforming mutant. In the domain of general mutation testing the problem of dealing with mutants equivalent, i.e., conforming, to the specification is well understood. In testing from an FSM, most approaches assume that the specification machine is reduced, so conforming mutants are isomorphic machines. Checking FSM equivalence is based on an FSM product. Notice that the proposed approach does not require the specification machine be reduced.

The complexity of the proposed method is defined by the number of constraints. We expect that the method scales well, since the recent advances in solving techniques drastically improve their scalability [START_REF] De Moura | Yices 1.0: An efficient SMT solver[END_REF][START_REF] De Moura | Z3: An efficient SMT solver[END_REF]. The number of constraints for a single execution is limited by the number of states of a mutation machine, but the number of executions increases with the number of mutated transitions. On the other hand, the number of executions of the distinguishing automaton which do not end up in the sink state grows with the number of mutated transitions, as faults may compensate each other. These executions are not revealing and do not contribute to the number of constraints. In Section 4 we present the results of our preliminary experiments performed on an industrial controller to assess the scalability of the approach.

Applications

The proposed mutation coverage analysis approach allows one to check if a given test suite is a complete test suite. A logical formula constructed by the proposed method represents the coverage of the test suite for a given fault model. If the test suite is found to be incomplete the question arises on how its quality in terms of fault coverage can be characterized. In the traditional software mutation testing, the fault detection power of tests is characterized by mutation score. It is a ratio of the number of killed mutants to the number of non-equivalent mutants. Note that the number of all possible mutants remains unknown and the mutation score is determined based on a limited set of generated mutants. As opposed to this approach, in our approach the total number of mutants can always be determined using the formula given in Section 2.2. Moreover, while the mutation analysis method avoids complete mutant enumeration, it does generate conforming mutants while searching for nonconforming ones.

The enumeration of conforming mutants is achieved by adding constraints to a logical formula excluding repeated generation of already found mutants.

In the same vain, our method can be enhanced to generate and enumerate (at least partially) undetected nonconforming mutants. Once a nonconforming mutant is given by a solution found by a SMT solver and the method terminates declaring the test suite to be incomplete, we may continue this process by adding a constraint excluding its repeated generation. As a result a list of nonconforming mutants can be obtained. Two extreme cases of incomplete tests are worth to be discussed here.

First, a given test suite may have no detection capability at all. This property is in fact detected very early by the method; in this case all the -distinguishing automata have no sink state reachable from the initial states, tests generate no constraints, the method can terminate at this step since there is no need to call a solver. No mutant in Sub(M) is killed, the score is zero.

Second, a given test suite is "almost" complete and kills most of the mutants in Sub(M). In this case, the process of nonconforming mutant generation does not take much time and once terminated yields the number of conforming mutants c as well as the number of survived nonconforming ones n. Then the mutation score is computed as follows:

(|Sub(M)| -c -n) / (|Sub(M)| -c).
It is worth to note that the way the mutation score is determined is completely different from that in software mutation testing, as our method generates mutants based on a given test suite and not the other way around.

When a given test suite is "far" from being complete the number of survived nonconforming mutants can explode especially when a mutation machine is close to a complete chaos machine which represents the complete universe of FSMs. In this situation one possible solution to cope with the mutant explosion problem is to terminate generating nonconforming mutants once their number reaches a predefined maximum, e.g., a percentage of |Sub(M)| or the time period allocated for mutation analysis ends. The obtained score is an (optimistic) estimation of an upper bound of the actual mutation score.

The proposed procedure could also be used for test minimization by defining a subsume relation between tests based on comparison of the logical formulas generated from them. Tests subsumed by other tests can always be removed from the original test suite. Similarly the generated formulas can be used to prioritize tests when needed, see, e.g., [START_REF] Korel | Test prioritization using system models[END_REF].

Experimental results

In this section we report on a prototype tool implementing the proposed approach and its use on a case study of an FSM model of an automotive controller of industrial size.

4.1

Prototype tool

The prototype tool takes as inputs a mutation machine and a test suite, both described in text format. The inputs are parsed with an ANTLR-based module [START_REF] Parr | The definitive ANTLR 4 reference[END_REF] to build an internal representation of the two objects. The mutation analysis algorithm manipulates these representations to build -distinguishing automata, determine revealing executions of the mutation machine and generate constraints for the Yices SMT solver [START_REF] De Moura | Yices 1.0: An efficient SMT solver[END_REF]. The solver is used as a backend to decide the satisfiability of the constraints.

The tool parses the outputs from Yices to extract a solution if it is found to build a mutant. The prototype can also be used with other SMT solvers compatible with the SMT-LIB 2.0.

Case study

In our experiments, we use as a case study an automotive controller of the air quality system, which we also used in our previous work [START_REF] Petrenko | A method and tool for test optimization for automotive controllers[END_REF]. The functionality of the controller is to set an air source position depending on its current state and a current input from the environment. The controller is initially specified as a hierarchical Simulink Stateflow model. Fig. 5 gives an overview of the model which is composed of three super-states s1, s2 and s23 and 13 simple states. Each super-state is composed of states and transitions. The initial state is the simple state s3. To obtain an FSM we introduced an input alphabet replacing transitions guards and flattened the hierarchical machine. We have identified 24 abstract inputs and two outputs. The resulting FSM has 14 states, since we added (for modeling of a branching behavior implemented with C code in the original state) one extra state to the given 13 simple states. It has 24 x 14 = 336 transitions.

The mutation machine was constructed from the following assumption about potential implementation faults. These faults may occur in outgoing transitions from any of the simple states in two super-states, namely s2 and s23 and four inputs, as Table 1 shows. The obtained mutation machine has 46 mutated transitions. The formula in Section 2 gives the number of mutants being equal to 3 12 x 2 17 = 69,657,034,752 including the specification machine.

Mutation analysis

To perform the mutation analysis, we needed a test suite, which could be generated randomly, however, we find it difficult to obtain tests that hit suspicious transitions in this case study, since 26 out of 336 transitions of the specification machine become suspicious in the mutation machine. We decided to use an early prototype of a test generation tool (which is work in progress) as an input for the mutation analysis tool.

The tool generates test cases one by one, so that the mutation analysis tool processes a test suite of an increasing size. The process terminates once a current test suite is found to be complete. In this experiment, the test suite completeness was determined when it had 31 test cases. The length of the test cases varies from 4 to 25 and the number of revealing executions triggered by each of them varies from 1 to 13. In the last, 31 st execution of Yices, it was given the formula of 69 clauses, for which it found no solution, meaning that the test suite is complete for the given mutation machine. The mutation analysis process took less than one minute on a desktop computer with the following settings: 3.4 Ghz Intel Core i7-3770 CPU, 16.0 GB of RAM, Yices 2.4.1, and ANTLR 4.5.1. The fact that the tool was able to determine that the given test suite kills each nonconforming mutant out of 69,657,034,752 possible mutants indicates that the approach scales sufficiently well on a typical automotive controller even when the number of mutants is big. In this experiment, we varied only the number of tests (from 1 to 31), hence more experiments by varying the specification as well as mutation machines are needed to assess the tool scalability.

Conclusions

In this paper we focused on fault model based testing, assuming that a fault model is given as a tuple of a specification FSM, equivalence as a conformance relation and a fault domain. A fault domain is a set of implementation machines, aka mutants, each of which models some faults, such as output, transfer or transition faults. Avoiding their enumeration we define the fault domain as a set of all possible submachines of a given nondeterministic FSM, called a mutation machine, as we did in our previous work. The mutation machine contains a specification machine and extends it with a number of mutated transitions, modelling potential faults. Thus a single mutant represents multiple mutations and mutation machine represents numerous mutants. In the area of mutation testing we could not find any attempt to analyze fault detection power of tests considering multiple mutants that avoids their enumeration. We proposed a method for analyzing mutation coverage of tests which we cast as a constraint satisfaction problem. The method relies on the notion of a distinguishing automaton that is a product of the specification and mutation machines. To analyze mutation coverage of a single input sequence we define a distinguishing automaton constrained by this sequence. This allows us to determine all mutants revealing executions that are triggered by the input sequence. The executions are then used to build constraint formulas to be solved by an existing solver, Yices, in our experiments. The approach avoids enumeration of mutants while still offering a possibility to estimate the test adequacy (mutation score).

The preliminary experiments performed on an industrial controller indicate that the approach scales sufficiently well. We are planning to further enhance the approach to Extended FSMs [START_REF] Petrenko | Confirming configurations in EFSM testing[END_REF] using mutation operators already defined for this type of FSMs.

Definition 2 .

 2 Given a complete deterministic specification machine A = (S, s0, I, O, N) and a mutation machine M = (S, s0, I, O, T), a finite automaton D = (C  {}, c0, I, D, ), where C  S  S, and  is an accepting (sink) state is the distinguishing automaton for A and M, if it holds that

Fig. 2 .

 2 Fig. 2. The distinguishing automaton D for the specification A and mutation M machines in Fig.1, state 11 is the initial state.

Definition 3 .

 3 Given input sequence   I*, a specification machine A = (S, s0, I, O, N) and a mutation machine M = (S, s0, I, O, T), a finite automaton D = (C  {}, c0, I, D, ), where C Pref()  S  S, and  is a designated sink state is the distinguishing automaton for A and M, if it holds that

Fig. 3 .

 3 Fig. 3. The -distinguishing automaton D for the specification A machine and mutation machine M in Fig. 1, where = baaba. Notice that the input sequence baaba and its prefix baa trigger two executions which end up in the sink state ∇. These are 1. (1, b, 0, 2)(2, a, 0, 3)(3, a, 1, 3) 2. (1, b, 0, 2)(2, a, 0, 3)(3, a, 0, 3)(3, b, 0, 3)(3, a, 0, 3).

Fig. 4 .

 4 Fig. 4. A fragment of -distinguishing automaton D for the specification A machine and mutation machine M in Fig. 1, where = babaaba; executions missing the sink state are not shown.

a, 1 , 3 )( 3 ,

 133 a, 0, 3)(3, b, 0, 4)(4, a, 1, 1) 4. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2) 5. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 1) 6. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 3)(3, a, 1, 3)(3, a, 0, 3)(3, a, 1, 3) 7. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, a, 0, 3)(3, a, 1, 3) 8. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 3)(3, a, 1, 3)(3, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)

1. ( 3 ,

 3 b, 0, 3), (3, a, 0, 3)  B 2. (3, b, 0, 3), (3, a, 1, 3)  B 3. (3, b, 0, 3), (3, a, 1, 3), (3, a, 0, 3), (3, b, 0, 4), (4, a, 1, 1)  B 4. (3, b, 0, 4), (4, a, 1, 2)  B 5. (3, b, 0, 4), (4, a, 1, 2), (4, a, 1, 1)  B 6. (3, b, 0, 3), (3, a, 1, 3), (3, a, 0, 3) b, 0, 4), (4, a, 1, 2), (3, a, 1, 3)  B 8. (3, b, 0, 3), (3, a, 1, 3), (3, a, 0, 3), (3, b, 0, 4), (4, a, 1, 2)  B Clearly nondeterministic executions 3, 5, 6 and 8 have unsatisfiable constraints since they require, e.g., that suspicious transition (3, b, 0, 4) is unaltered and replaced by the mutated transition (3, b, 0, 3) in the same mutant.

Fig. 5 . 1 .

 51 Fig. 5. An overview of the Simulink/Stateflow model in the controller

  s0, p0)  For any (, s, t)  C and x  I, such that x  Pref(), ((, s, t), x, (x, s, t))  D, if there exist (s, x, o, s)  N, (t, x, o, t)  T, such that o = oand ((, s, t), x, )  D, if there exist (s, x, o, s)  N, (t, x, o, t)  T, such that o  o.

Acknowledgements. This work is supported in part by GM R&D and the MEIE of Gouvernement du Québec. The authors would like to thank the reviewers for their useful comments.


Jorge A Pérez

The Challenge of Typed Expressiveness in Concurrency

By classifying behaviors (rather than data values), behavioral types abstract structured protocols and enforce disciplined messagepassing programs. Many different behavioral type theories have been proposed: they offer a rich landscape of models in which types delineate concurrency and communication. Unfortunately, studies on formal relations between these theories are incipient. This paper argues that clarifying the relative expressiveness of these type systems is a pressing challenge for formal techniques in distributed systems. We overview works that address this issue and discuss promising research avenues.

Introduction

Communication and types are increasingly relevant in (concurrent) programming. To bear witness of this trend, several languages promoted by industry offer advanced type systems (or type-based analysis tools) and/or support (messagepassing) communication. For instance, Facebook's Flow [START_REF]Flow: A Static Type Checker for JavaScript[END_REF] is a type checker for JavaScript based on gradual typing; Mozilla's Rust [START_REF]The Rust Programming Language[END_REF] exploits affine, ownership types to balance safety and control; Google's Go [START_REF]The Go Programming Language[END_REF] supports process concurrency and channel-based communication. Other languages (e.g., Erlang [START_REF]The Erlang Programming Language[END_REF]) also offer forms of (message-passing) communication.

If communication and types are here to stay, on what foundations languages integrating both features should rest? Much research within formal techniques in distributed systems has been devoted to models for concurrency and communication. In particular, process calculi have been widely promoted as a basis for type systems for concurrent programs. Indeed, building upon the π-calculus, a variety of behavioral type systems have been put forward [START_REF] Dezani-Ciancaglini | Sessions and session types: An overview[END_REF][START_REF] Huttel | Foundations of session types and behavioural contracts[END_REF]: by classifying behaviors (rather than values), these type structures abstract structured protocols and enforce disciplined message-passing programs. Existing work suggests that rather than a shortage of foundations for types and communication, we have the opposite problem: there are many formal foundations and it is unclear how to build upon them to transfer analysis techniques into practice.

The current situation calls for rigorous comparisons between well-established (but distinct) behavioral typed frameworks. Besides revealing bridges between different models of typed processes, such comparisons should clarify the complementarities and shortcomings of analysis techniques based on types. Developing a theory of typed expressiveness is thus a challenge for the specification and analysis of distributed systems. The consolidation of communication-centered software systems (collections of interacting, heterogeneous services) and the renewed interest of software practitioners in communication and types endow this research challenge with practical significance.

We argue that the much needed formal comparisons may draw inspiration from results and frameworks for relative expressiveness, as studied in concurrency theory. This area has elucidated important formal relations between untyped process languages (see [START_REF] Parrow | Expressiveness of process algebras[END_REF] for a survey); it thus appears as an adequate basis for analogous formal results in a typed setting.

This short paper is organized as follows. Next we overview main achievements in untyped expressiveness ( § 2). Then, we briefly review expressiveness results that consider behavioral types and/or behaviorally typed processes ( § 3). We conclude by discussing promising research directions ( § 4).

Expressiveness in Concurrency: The Untyped Case

Important studies of expressiveness in concurrency concern process calculi, a wellestablished approach to the analysis of concurrent systems. These formalisms, in particular the π-calculus, also provide a basis for typed systems for communicating programs. Process calculi promote the view of concurrency as communication: they abstract the interactions of a system by means of atomic communication actions. This view is simple and powerful, and has deep ramifications to computing at large.

The process calculi approach to concurrency has proved prolific. Starting from a few "basic" process calculi (including CSP, CCS, the π-calculus, amongst others), many extensions have been put forward, following modeling requirements (e.g., quantitative information) but also the need of representing forms of interaction typical of application domains such as, e.g., systems biology, security, and service-oriented computing. Given this jungle of process models [START_REF] Nestmann | Welcome to the jungle: A subjective guide to mobile process calculi[END_REF], the need for establishing formal relationships between them was soon evident. To rise to this challenge, since the early 1990s a sustained body of work has assessed the expressiveness of process languages. These studies may pertain, for instance, to the nature of a process construct (e.g., whether it can be implemented using more basic ones) or to the transfer of reasoning techniques (e.g., process equivalences) across languages.

The main device used in expressiveness studies is the notion of encoding: a translation of a source language L S into a target language L T that satisfies certain properties. Such properties are usually defined as syntactic and semantic criteria; they are abstract indicators of an encoding's quality. Two common criteria are homomorphism with respect to parallel composition, which promotes compositional encodings, and operational correspondence, which relates the (visible) behavior of source and target processes. Abstract formulations of encodings and their criteria have been put forward (cf. [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]). An encoding of L S into L T (a positive encodability result) indicates that L T is at least as expressive as L S : all behaviors expressible in L S can also be expressed in L T . The non existence of an encoding (a negative encodability result) may indicate that L S is more expressive than L T : there are behaviors expressible in L S but not in L T .

Encodability results have clarified our understanding of notions of interaction and communication as abstracted by process calculi. They have been crucial to: a) Formally relate different computational models. Two notable examples are (i) the encodability of the λ-calculus in the π-calculus [START_REF] Milner | Functions as processes[END_REF], and (ii) decidability results for termination/convergence for CCS, which distinguish the expressive power of processes with replication and recursion [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF]. b) Assess the expressive power of process languages. As an example, several influential works have clarified the interplay of choice operators and (a)synchronous communication, and its influence on the expressive power of the π-calculus (see, for instance, [START_REF] Palamidessi | Comparing the expressive power of the synchronous and asynchronous pi-calculi[END_REF]). c) Transfer proof techniques between different calculi. For instance, the fully abstract encodability of process mobility (process passing) into name mobility has important consequences on the behavioral theory of higher-order process calculi [START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF].

Expressiveness results can be useful in the design of concurrent languages. For instance, the formalization of compilers usually requires encodings and behaviorpreserving translations. Similarly, the development of type systems for process calculi, in particular behavioral types, has further reconciled process models and actual concurrent languages.

Towards Relative Expressiveness for Behavioral Types

The development of process languages with verification techniques based on type systems has received much attention. From Milner's sortings [START_REF] Milner | The Polyadic pi-Calculus: A Tutorial[END_REF] until recently discovered logic foundations of concurrency [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF]-passing through, e.g., graph types [START_REF] Yoshida | Graph types for monadic mobile processes[END_REF], linear types [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF], session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF], and generic types [START_REF] Igarashi | A generic type system for the pi-calculus[END_REF]-type systems have revealed a rich landscape of concurrent models with disciplined communication. Within these different type systems, behavioral types stand out by their ability to abstract notions such as causality, alternatives (choices), and repetition [START_REF] Huttel | Foundations of session types and behavioural contracts[END_REF]. A behavioral type defines the resource-usage policy of a communication channel, but also describes a series of actions realized through that channel along time. Behavioral types are often defined on top of process calculi; this enables the definition of general verification techniques that may be then adapted to different languages. Given this jungle of typed process models, the need for establishing formal relations between them rises again. Mirroring the achievements of untyped expressiveness (cf. (a)-(c) above), we believe that research on formal methods for distributed systems would benefit from efforts aimed at: i) Formally relating different typed models. ii) Assessing the expressiveness of languages governed by behavioral types. iii) Transferring analysis techniques between different typed languages and formalisms.

These are challenging issues: as different type systems rely on unrelated concepts, discrepancies on typability arise easily. Hence, objective comparisons are hard to establish. Next we briefly review some works that address (i)-(iii) from various angles. Most of them concern session types, one of the most representative classes of behavioral types. Session types abstract structured communications (protocols) by allowing sequential actions (input and output), labeled choices (internal and external), and recursion. Binary session types [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF] abstract protocols between two partners; multiparty session types [START_REF] Honda | Multiparty asynchronous session types[END_REF] overcome this limitation: a global type (choreography) offers a high-level perspective for the local types realized by each partner. Different formulations for binary/multiparty session types have been developed, with varying motivations [START_REF] Huttel | Foundations of session types and behavioural contracts[END_REF].

Linear Types and Session Types. Kobayashi appears to be the first to have related distinct type disciplines for the π-calculus by encoding the (finite) session π-calculus into a π-calculus with linear types with usages and variant types [38, §10]. His encoding represents a session name by multiple linear channels, using a continuation-passing style. Since Kobayashi does not explore the correctness properties of his encoding, Dardha et al.

[17] revisit it by establishing type and operational correspondences and by giving extensions with subtyping, polymorphism, and higher-order communication. An extension of [17] with recursion in processes and types is reported in [START_REF] Dardha | Recursive session types revisited[END_REF].

In a similar vein as [17], Demangeon and Honda [START_REF] Demangeon | Full abstraction in a subtyped pi-calculus with linear types[END_REF] encode a session πcalculus into a linear/affine π-calculus with subtyping based on choice and selection types, which generalize input and output types, resp. Their encoding preserves subtyping. In contrast to [17], the encoding in [START_REF] Demangeon | Full abstraction in a subtyped pi-calculus with linear types[END_REF] is fully abstract up to may/must barbed congruences. Their linear/affine π-calculus can also encode a call-by-value λ-calculus.

Gay et al. [START_REF] Gay | Session types as generic process types[END_REF] encode a monadic π-calculus with (finite) binary session types (as in [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]) into a polyadic π-calculus with generic process types (as in [START_REF] Igarashi | A generic type system for the pi-calculus[END_REF], instantiated with linear, race-free communications). They aim at retaining original constructs in both models and to ensure operational and type correspondences. Their encoding enjoys these correspondences, but does not preserve subtyping. The authors notice that encoding labeled choice into guarded, unlabeled summation is challenging; also, that the target languages considered in [17,[START_REF] Demangeon | Full abstraction in a subtyped pi-calculus with linear types[END_REF] admit simple encodings of labeled choice.

Concerning transfer of techniques, Carbone et al. [START_REF] Carbone | Progress as compositional lock-freedom[END_REF] use the encoding in [17] to relate progress in the session π-calculus to lock-freedom [START_REF] Kobayashi | A type system for lock-free processes[END_REF] in the linear πcalculus. This path to progress in binary sessions is an improvement with respect to previous works [START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF][START_REF] Carbone | A graphical approach to progress for structured communication in web services[END_REF], as more session processes with progress are accepted as well-typed.

Session Types and Automata-like Models. Just as (untyped) process calculi have been related to sequential models of computation to characterize (un)decidability properties (therefore identifying expressiveness gaps-see, e.g., [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF]), session types have been related to automata-like models. Initial results are due to Villard [START_REF] Villard | Heaps and Hops[END_REF] who, in the context of dual channel contracts, shows that a subclass of communicating finite state machines (CFSMs) characterizes binary session types. Deniélou and Yoshida [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF] extend this characterization to the multiparty setting by giving a class of generalized multiparty session types and their interpretation into CFSMs. This class inherits key safety and liveness properties from CFSMs. The work [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF] complements [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF] by offering a sound and complete characterization of multiparty session types as CFSMs, identifying the key notion of multiparty compatibility. Lange et al. [START_REF] Lange | From communicating machines to graphical choreographies[END_REF] extend this work by developing techniques to synthesize global graphs from CFSMs, covering more global protocols than [START_REF] Deniélou | Multiparty session types meet communicating automata[END_REF][START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]. Fossati et al. [START_REF] Fossati | Multiparty session nets[END_REF] overcome modeling limitations of textual multiparty session types through an integration with Petri nets. Using Petri nets token semantics they define a conformance relation between syntactic local types and session nets.

Types in the ψ-calculi. The ψ-calculi [START_REF] Bengtson | Psi-calculi: Mobile processes, nominal data, and logic[END_REF] are a family of name-passing process calculi that extends the π-calculus with terms, conditions, and assertions. Generality arises by treating terms as subjects in communication prefixes and by allowing input patterns. Hüttel [START_REF] Hüttel | Typed ψ-calculi[END_REF] proposes a type system for ψ-calculi that generalizes simple types for the π-calculus; it enjoys generic formulations of type soundness and type safety. Instantiations are shown for other process languages, including the fusion calculus, the distributed π (Dπ), and the spi-calculus. The work [START_REF] Hüttel | Types for resources in ψ-calculi[END_REF] extends [START_REF] Hüttel | Typed ψ-calculi[END_REF] to the case of resource-aware type systems: it proposes a type system for ψ-calculi that subsumes the system for linear channel usage of [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF], the action types of [START_REF] Yoshida | Strong normalisation in the pi -calculus[END_REF], and a type system similar to that in [START_REF] Deng | Ensuring termination by typability[END_REF].

Other Approaches. López et al. [START_REF] López | Towards a unified framework for declarative structured communications[END_REF] encode binary session processes into a declarative process calculus, enabling the transfer of LTL reasoning to scenarios of session communications. Cano et al. [START_REF] Cano | Declarative interpretations of session-based concurrency[END_REF] encode a session π-calculus into declarative process calculus with explicit linearity and establish strong operational correspondences. Padovani [START_REF] Padovani | Session types = intersection types + union types[END_REF] relates labeled choice operators in session types with intersection and union types. Orchard and Yoshida [START_REF] Orchard | Effects as sessions, sessions as effects[END_REF] encode PCF with an effect type system into a session π-calculus; a reverse encoding that embeds the session π-calculus into PCF with concurrency primitives is used to offer a new implementation of sessions into Haskell.

Concluding Remarks and Future Directions

The works discussed above define insightful relations between different frameworks of behavioral types. Although some works define the transfer of techniques between typed models and/or enable practical applications (cf. [START_REF] Carbone | Progress as compositional lock-freedom[END_REF][START_REF] Orchard | Effects as sessions, sessions as effects[END_REF][START_REF] López | Towards a unified framework for declarative structured communications[END_REF]), most existing works define isolated studies: since each work uses different techniques to relate typed models, further research is needed to integrate their results. There are promising research directions towards this ambitious goal. For space reasons, below we discuss only three of them.

Expressiveness Without Processes

Using process calculi to study behavioral types allows to establish their properties by exploiting well-established process techniques. In practical multiparty communications [START_REF] Carbone | Deadlock-freedom-by-design: multiparty asynchronous global programming[END_REF][START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF][START_REF] Lange | From communicating machines to graphical choreographies[END_REF], however, one is mostly interested in types (rather than in processes), as they offer contracts/interfaces to derive safe implementations. These works use process calculi techniques to define, e.g., operational semantics and equivalences for global types. If one focuses on types then expressiveness results should relate different behavioral types and their semantics. Demangeon and Yoshida [START_REF] Demangeon | On the expressiveness of multiparty sessions[END_REF] develop this approach: they contrasted the expressivity of different models of multiparty session types by comparing their trace-based denotations. As global types become richer in structure, comparisons will need to use techniques from relative expressiveness. The recent work of Cruz-Filipe and Montesi [START_REF] Cruz-Filipe | Choreographies, computationally[END_REF] goes in this direction.

A Logic Yardstick for Typed Expressiveness

The variety of behavioral types rises a natural question: what should be a "fair yardstick" to compare them? Recently developed Curry-Howard correspondences for concurrency [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Carbone | Multiparty session types as coherence proofs[END_REF] define a fundamental model of behavioral types: by relating session types and linear logic, they identify type preserving and deadlockfree process models. Some works connect [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF] and other models. Wadler [START_REF] Wadler | Propositions as sessions[END_REF] gives a deadlockfree fragment of the session-typed functional language in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] by encodings into concurrent processes. The work [START_REF] Dardha | Comparing deadlock-free session typed processes[END_REF] contrasts two classes of deadlock-free, session processes: the first class results from [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF]; the other results by combining the encoding in [17] and usage types [START_REF] Kobayashi | A type system for lock-free processes[END_REF]. The former class is shown to be strictly included in the latter. The work [START_REF] Caires | Multiparty session types within a canonical binary theory, and beyond[END_REF][START_REF] Caires | A typeful characterization of multiparty structured conversations based on binary sessions[END_REF] defines an analysis of multiparty session types (lock-free choreographies, as in [START_REF] Deniélou | Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types[END_REF]) using techniques for binary session types (as in [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF]). Further work should relate [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Carbone | Multiparty session types as coherence proofs[END_REF] and other behavioral types.

Typed Encodability Criteria

Related to § 4.1, another direction is clarifying how existing frameworks for relative expressiveness (such as [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF]) can account for behavioral types. This is needed to understand how types induce encodability results, but also to relate different behavioral types in source/target languages.

In their recent study of the relative expressivity of higher-order session communication, Kouzapas et al. [START_REF] Kouzapas | On the relative expressiveness of higherorder session processes[END_REF] define a notion of typed encoding that extends [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF] with session types. This work considers translations of processes and types and two new encodability criteria: type soundness and type preservation. The former says that translations preserve typability (well-typed source processes are encoded into well-typed target processes), the latter says that encodings of types preserve the structure of the session protocol, as represented by session type operators. While demanding and focused to the case of binary session types, these criteria are shown to be appropriate in classifying session-based π-calculi. Further work is needed to generalize/relax these typed encodability criteria, so to consider source and target languages with different type systems.

Acknowledgments. I would like to thank Ilaria Castellani, Ornela Dardha, Mariangiola Dezani-Ciancaglini, Dimitrios Kouzapas, Hugo A. López, and Camilo Rueda for their useful feedback on previous drafts of this paper.


Nicola Atzei
email: atzeinicola@unica.it

Massimo Bartoletti

Developing honest Java programs with Diogenes

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Developing modern distributed applications is a challenging task: programmers have to reliably compose loosely-coupled services which can dynamically discover and invoke other services through open networks, and may be subject to failures and attacks. Unless these services are implemented in a decentralized manner (e.g., as smart contracts in Ethereum or Contractvm [START_REF]Ethereum[END_REF]11]), they will be under the governance of mutually distrusting providers, possibly competing among each other. Typically, these providers offer little or no guarantees about the services they control, and in particular they reserve the right to change the service code (if not the Service Level Agreement tout court) at their discretion.

Therefore, to guarantee the reliability and security of distributed applications, one cannot directly apply standard analysis techniques for programming languages (like e.g., type systems or model checking). Indeed, these analysis techniques usually need to inspect the code of the whole application, while under the given assumptions one can only reason about the services under their control. In particular, compositional verification based on choreographies [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF] is not suitable in this setting, because to ensure the correctness of the whole application, all its components have to be verified.

From service-oriented to contract-oriented computing. A possible countermeasure to these issues is to use contracts to regulate the interaction between services. By advertising a contract, a service commits itself to respect a given behaviour when, after stipulation, it will interact with others. In this setting, a service infrastructure acts as a trusted third party, which collects all the advertised contracts, and establishes sessions between participants with compliant ones. Participants can then interact through sessions, by sending and receiving messages as required by their contracts (or even choosing to violate them, if they find this choice more convenient). An actual implementation of this paradigm is the middleware in [START_REF] Bartoletti | A contractoriented middleware[END_REF], which offers a set of APIs through which services can advertise, stipulate, and execute contracts (based on binary session types [START_REF] Honda | Types for dyadic interaction[END_REF]).

To incentivize honest behaviour, contract-oriented infrastructures monitor all the messages exchanged among services, to sanction those which do not respect their contracts. Sanctions can be of different nature: e.g., pecuniary compensations, adaptations of the service binding [START_REF] Mukhija | QoS-aware service composition in Dino[END_REF], or they can decrease the reputation of a service whenever it violates a contract, in order to marginalize dishonest services in the selection phase [START_REF] Bartoletti | A contractoriented middleware[END_REF].

Experimental evidence about the programming paradigm and incentive mechanisms of [START_REF] Bartoletti | A contractoriented middleware[END_REF] shows that contract-orientation can mitigate the effort of handling potential misbehaviour of external services, at the cost of a tolerable loss in efficiency due to the contract-based service selection and monitoring.

Honesty attacks. The sanction mechanism of contract-oriented services allows a new kind of attacks: adversaries can try to exploit possible discrepancies between the promised and the actual behaviour of a service, in order to make it sanctioned. For instance, consider a naïve online store with the following behaviour:

1. advertise a contract to "receive an order from a client, and then either ship the ordered item or abort the transaction"; 2. wait to receive an order; 3. advertise a contract to "receive a quote from a package delivery service, and then either confirm or abort"; 4. wait to receive a quote from the delivery service; 5. if the quote is below a certain threshold, then confirm the delivery and ship to the client; otherwise, abort both transactions. Now, assume an adversary which plays the role of a delivery service, and never sends the quote. This makes the store violate its contract with the client: indeed, the store should either ship or abort, but these actions can only be performed after the delivery service has sent a quote. Therefore, the store can be sanctioned. Since these honesty attacks may compromise the service and cause economic damage to its provider, it is important to detect the underlying vulnerabilities before deployment. Intuitively, a service is vulnerable if, in some execution context, it does not respect some of the contracts it advertises. This may happen either unintentionally (because of errors in the service specification, or in its implementation), or even because of malicious behaviour. Therefore, to avoid sanctions a service must be able to respect all the contracts it advertises, in all possible contexts -even those populated by adversaries. We call this property honesty. Whenever compliance between contracts ensures their deadlock-freedom (as for the relations in [START_REF] Acciai | Behavioural contracts with request-response operations[END_REF][START_REF] Barbanera | Two notions of sub-behaviour for session-based client/server systems[END_REF][START_REF] Laneve | The must Preorder Revisited[END_REF][START_REF] Rensink | Fair testing[END_REF]), the honesty property can be lifted from contracts to services: systems of honest services are deadlock-free (Theorem 6 in [START_REF] Bartoletti | On the decidability of honesty and of its variants[END_REF]). Some recent works have studied honesty at the specification level, using the process calculus CO 2 for modelling contract-oriented services [START_REF] Bartoletti | Verifiable abstractions for contract-oriented systems[END_REF][START_REF] Bartoletti | Contract-oriented computing in CO2[END_REF][START_REF] Bartoletti | On the decidability of honesty and of its variants[END_REF]. Practical experience with CO 2 has shown that writing honest specifications is not an easy task, especially when a service has to juggle with multiple sessions. The reason of this difficulty lies in the fact that, to devise an honest specification, a designer has to anticipate all the possible moves of the context, but at design time he does not yet know in which context his service will be run. Hence, tools to automate the verification of honesty in CO 2 may be of great help.

A further obstacle to the development of honest services is that, even if we start from an honest CO 2 specification, it is still possible that honesty is not preserved when refining the specification into an actual implementation. Analysis techniques for checking honesty at the level of the implementation are therefore needed in order to develop reliable contract-oriented applications.

Contributions. To support programmers in the development of contract-oriented applications, we provide a suite of tools (named Diogenes) with the following features: (i) writing CO 2 specifications of services within an Eclipse plugin; (ii) verifying honesty of these specifications; (iii) generating from them skeletal Java programs which use the contract-oriented APIs of the middleware in [START_REF] Bartoletti | A contractoriented middleware[END_REF]; (iv) verifying the honesty of Java programs upon refinement. We validate our tools by applying them to all the case studies in [START_REF] Bartoletti | Verifiable abstractions for contract-oriented systems[END_REF]: in particular, we specify each of these case studies in CO 2 , and we successfully verify the honesty of both the specifications and their Java refinements. Overall, we can execute these verified services using the middleware in [START_REF] Bartoletti | A contractoriented middleware[END_REF], being guaranteed that they will not incur in sanctions, and that interactions with other honest services will be deadlock-free. Our tools, the case studies, and a tutorial are available at co2.unica.it/diogenes.

Diogenes in a nutshell

In this section we show the main features of our tools with the help of a small example. Suppose we want to implement an online store which receives orders from customers, and relies upon external distributors to retrieve items.

Contracts. The store has two contracts: C specifies the interaction with customers, and D with distributors. In C, the store declares that it will wait for an order, and then send either the corresponding amount or an abort message (e.g., in case the ordered item is not available). The answer may depend on an external distributor service, which waits for a request, and then answers ok or no. We specify these two contracts as the following binary session types [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF]: Receive actions are marked with the symbol ? and grouped by +; instead, send actions are marked with ! and grouped by (+). The symbol . denotes sequential composition. We specify the sort of a message (int, string, or unit) after the action label; sort unit is used for pure synchronization, and it can be omitted. Specification. A naïve CO 2 specification of our store is the following: At line 2, the store advertises the contract C, and then waits until a session is established with some customer; when this happens, the variable x is bound to the session name. At line 3 the store waits to receive an order, binding it to the variable v. At line 4 the store advertises the contract D to establish a session y with a distributor; at line 5, it sends a request with the value v. Finally, the store waits to receive a response ok or no from the distributor, and accordingly responds amount or abort to the customer (lines 6-8). The sent amount *:int is placeholder, to be replaced upon refinement. The internal action t at line 9 models a timeout, fired in case no response is received from the distributor.

1 specification StoreDishonest { 2 tellAndWait x C .
Our tool correctly detects that this specification is dishonest, outputting: There are two causes for dishonesty. First, if the session y is never established (e.g., because no distributor is available), the store is stuck at line 4 and cannot fulfil C at session x ($0 in the output message). Second, if the distributor response arrives after the timeout (line 9), the store does not consume its input, and so it does not respect the contract D at session y ($1 in the output message).

A possible way to fix the previous specification is the following: The primitive tellRetract at line 4 ensures that if the session x is not established within a given deadline (immaterial in the specification) the contract D is retracted, and the control passes to line 10. Further, in the timeout branch we have added a parallel execution of a receive to consume orphan inputs (line 9). Now the tool correctly detects that the revised specification is honest.

1 specification StoreHonest { 2 tellAndWait x C .
An execution context. We now show a possible context wherein to execute our online store. Although the context is not needed for checking the honesty of the store, we use it to complete the presentation of the primitives of CO 2 . The contracts of the Buyer (lines 2) and that of the Distributor (line 11) are compliant with the contracts C and D advertised by the store. The Buyer uses the statement tellAndReturn to advertise its contract: it does not wait the session is established, but postpone the waiting phase until it is strictly required (line 3 in this case), although the session could be already started in the meantime. The Distributor uses a conditional statement (with a dummy guard *:boolean) to choose whether accepting or not the store request.

Code generation and refinement. Diogenes translates CO 2 specifications into Java skeletons, using the APIs of the middleware in [START_REF] Bartoletti | A contractoriented middleware[END_REF]. For instance, from the StoreHonest specification given above, it generates the following skeleton1 : We use Java exceptions to deal with both the tellRetract and receive primitives: the ContractExpiredException is thrown by line 9 if the session y is not established within a given timeout (10 sec), while the TimeExpiredException is thrown by line 13 if a message is not received within the timeout. The parallel method at lines 20-21 starts a new thread which executes the given Runnable instance. The timeout values, as well as the order amount at line 15, are just placeholders; in an actual implementation of the store service, we may want to delegate the computation of amount to a separated method, e.g.: and change the placeholder intP at line 15 with getOrderAmount(v). The method could read the order amount from a file or a database, and suppose that each possible exception is caught and hidden behind MyException. The failure of this method can be considered non-deterministic, so we need to "instruct" our verification tool in order to consider all the possible ways the method can terminate. To this purpose, we provide the annotation @SkipMethod(value="<value>"), interpreted by the checker as follows: (i) assumes that the method does not perform any action directed to the middleware; (ii) considers <value> as the returning value on success; (iii) considers the declared exceptions as possible exit points on failure. Diogenes can symbolically consider both the case of a normal method termination and all the possible exceptional terminations.

Verification. We can check the honesty of a Java program through the static method HonestyChecker.isHonest(StoreHonest.class), which returns one of the following values:

-HONEST: the tool has inferred a CO 2 specification and verified its honesty; -DISHONEST: as above, but the inferred CO 2 specification is inferred, but it is dishonest; -UNKNOWN: the tool has been unable to infer a CO 2 specification, e.g. because of unhandled exceptions within the class under test. For our refined store, the Java honesty checker returns UNKNOWN and outputs: This means that if the method getOrderAmount fails, then the program will terminate abruptly, and so the store may violate the contract. We can recover honesty by catching MyException with x.sendIfAllowed("abort"). With this modification, the Java honesty checker correctly outputs HONEST.

Architecture

Diogenes has three main components: an honesty checker for CO 2 , an honesty checker for Java, and an Eclipse plugin which integrates the two checkers with an editor of CO 2 specifications. We sketch the architecture of our tools in Figure 1.

The CO 2 honesty checker implements the verification technique introduced in [START_REF] Bartoletti | Verifiable abstractions for contract-oriented systems[END_REF]. This technique is built upon an abstract semantics of CO 2 which approximates both values (sent, received, and in conditional expressions) and the actual context wherein a process is executed. This abstraction is a sound overapproximation of honesty: namely, if the abstraction of a process is honest, then also the concrete one is honest. Further, in the fragment of CO 2 without conditional statements the analysis is also complete, i.e. if a concrete process is honest, then also its abstraction is honest. For processes without delimitation/parallel under process definitions, the associated abstractions are finite-state, hence we can verify their honesty by model checking a (finite) state space. For processes outside this class the analysis is still correct, but it may not terminate; indeed, a negative result in [START_REF] Bartoletti | On the decidability of honesty and of its variants[END_REF] excludes the existence of algorithms for honesty that are at the same time sound, complete, and terminating in full CO 2 . Our implementation first translates a CO 2 process into a Maude term [START_REF] Clavel | Maude: Specification and programming in rewriting logic[END_REF], and then uses the Maude LTL model checker [START_REF] Eker | The Maude LTL model checker[END_REF] to decide honesty of its abstract semantics.

The Java honesty checker is built on top of Java PathFinder (JPF, [START_REF] Lerda | Addressing dynamic issues of program model checking[END_REF][START_REF] Visser | Model checking programs[END_REF]). The JPF core is a virtual machine for Java bytecode that can be configured to act as a model checker. We define suitable listeners to catch the requests to the contract-oriented middleware [START_REF] Bartoletti | A contractoriented middleware[END_REF], and to simulate all the possible responses that the application can receive from it. Through JPF we symbolically execute and backtrack the program, and eventually we infer a CO 2 specification that over-approximates its behaviour. Then, we apply the CO 2 honesty checker to establish the honesty of the Java program. The accuracy of the inferred CO 2 specification partially relies on the programmer: the methods involved in the application logic have to be correctly annotated, and in particular they have to declare all possible exceptions that can be thrown at runtime.

The Eclipse plugin supports writing CO 2 specifications, providing syntax highlighting, code auto-completion, syntactic/semantic checks, and static type checking on sort usage. It relies on Xtext (www.eclipse.org/Xtext), a framework for developing programming languages, and on Xsemantics (xsemantics. sourceforge.net), a domain-specific language for writing type systems.

Conclusions

Diogenes fills a gap between foundational research on honesty [START_REF] Bartoletti | Contract-oriented computing in CO2[END_REF][START_REF] Bartoletti | Verifiable abstractions for contract-oriented systems[END_REF][START_REF] Bartoletti | On the decidability of honesty and of its variants[END_REF] and more practical research on contract-oriented programming [START_REF] Bartoletti | A contractoriented middleware[END_REF]. Its effectiveness can be improved in several ways, ranging from the precision of the analysis, to the informative quality of output messages provided by the honesty checkers.

The accuracy of the honesty analysis could be improved e.g., by implementing the type checking technique of [START_REF] Bartoletti | Honesty by typing[END_REF], which can correctly classify the honesty of some forms of infinite-state of processes (while the current honesty checker is only guaranteed to terminate for processes without delimitation/parallel within recursion). Another form of improvement would be to extend the analysis to deal with timing constraints. This could be done e.g. by exploiting the timed version of CO 2 proposed in [START_REF] Bartoletti | A contractoriented middleware[END_REF] and the timed session types of [START_REF] Bartoletti | Compliance and subtyping in timed session types[END_REF]. Although the current analysis for honesty does not consider timing constraints, it may give useful feedback also when applied to timed specifications. For instance, it could detect that some prescribed actions cannot be performed because the actions they depend on may be blocked by an unresponsive context.

The error reporting facilities could be improved in several directions: e.g., it would be helpful for programmers to know which parts of the program make it dishonest, what are the contract obligations that are not fulfilled, and in what session. Further, it would be useful to suggest possible corrections to the designer.

Another direction for future work concerns relating the original CO 2 specification with the refined Java code. In fact, our tools only guarantee that the Java skeleton generated from an (honest) CO 2 specification is (honest and) coherent with the specification. If the programmer further refines the Java code, e.g. by removing some contract advertisements, then the Java honesty checker can still check that the resulting code is honest, but the coherence with the original specification may be lost. An additional static analysis could establish that the CO 2 process inferred from the refined Java code by JPF is a (sort of) subtype of the original specification, and so that it can be safely used in the same contexts.

  contract C { order ? string . ( amount ! int (+) abort ! ) } contract D { req ! string . ( ok ? + no ? ) }

  ok ? . send x amount ! *: int 8 y <-no ? . send x abort ! 9 ] + t . send x abort !) ) 10 }

  result : (" y " , $ 0) ( StoreDishonest [ tell " y " D . ask " y " True . (...) ] | $ 0[" abort " ! unit . 0 (+) " amount " ! int . 0]) result : ( $ 0 , $ 1) ( StoreDishonest [ do $ 0 " abort " ! unit . (0) . Sum ] | $ 0[" abort " ! unit . 0 (+) " amount " ! int . 0] | $ 1[ ready " no " ? unit . 0]) honesty : false

9 ] 10 :

 910 ok ? . send x amount ! *: int 8 y <-no ? . send x abort ! + t . ( send x abort ! | receive y ok ? no ?) ) send x abort !) 11 }

  order ! string . ( amount ? int + abort ? ) } .

3

  send x order ! *: string .

  req ? string . ( ok ! (+) no ! ) } .12 receive x req ? msg : string . 13 if *: boolean then send x ok ! else send x no ! 14 }

1 6 /

 6 public class StoreHonest extends Participant { 2 public void run () { 3 Session < TST > x = tellAndWait ( C ) ; // ( line 2)Message msg = x . waitForReceive ( " order " ) ; // ( line 3)String v = msg . getStringValue () ; y . waitForReceive (10000 , " ok " ," no " ) ; // ( line 6) 14 switch ( msg_1 . getLabel () ) { case " ok " : x . sendIfAllowed ( " amount " , intP ) ; break ; // ( line 7) 16 case " no " : x . sendIfAllowed ( " abort " ) ; break ; // ( line 8) catch ( T i m e E x p i r e d E x c e p t i o n e ) { // ( line 9) 20 parallel (() ->{ x . sendIfAllowed ( " abort " ) ;}) ; 21 parallel (() ->{ y . waitForReceive ( " ok " ," no " ) ;}) ; o n t r a c t E x p i r e d E x c e p t i o n e ) { 25

  30public int getOrderAmount ( String order ) throws MyException {...}

1 error details : MyException : 2

 12 This exception is thrown by the honesty checker . Please catch it ! 3 at i . u . c . store . StoreHonest . getOrderAmount ( Store . java :30) 4 at i . u . c . store . StoreHonest . run ( Store . java :15) 5 at i . u . c . honesty . HonestyChecker . runProcess ( HonestyChecker . java :182)

Fig. 1 .

 1 Fig. 1. Data flow schema

Minor cosmetic changes are applied to improve readability.

Acknowledgments. This work has been partially supported by Aut. Reg. of Sardinia P.I.A. 2013 "NOMAD", and by EU COST Action IC1201 "Behavioural Types for Reliable Large-Scale Software Systems" (BETTY).