Ana Cavalcanti
email: ana.cavalcanti@york.ac.br

Adenilso Simao
email: adenilso@icmc.usp.br

Fault-Based Testing for Refinement in CSP

The process algebra CSP has been studied as a modeling notation for test derivation. Work has been developed using its trace and failure semantics, and their refinement notions as conformance relations. In this paper, we propose a procedure for online test generation for selection of finite test sets for traces refinement from CSP models, based on the notion of fault domains, that is, focusing on the set of faulty implementations of interest. We investigate scenarios where the verdict of a test campaign can be reached after a finite number of test executions. We illustrate the usage of the procedure with a small case study.

Introduction

Model-based testing (MBT) has received increasing attention due to its ability to improve productivity, by automating test planning, generation, and execution. The central artifact of an MBT technique is the model. It serves as an abstraction of the system under test (SUT), manageable by the testing engineers, and can be processed by tools to automatically derive tests. Most notations for test modeling are based on states; examples are Finite State Machines, Labelled Transition Systems, and Input/Output Transition Systems. Many testgeneration techniques are available for them [START_REF] Chow | Testing software design modeled by finite-state machines[END_REF][START_REF] Hierons | Optimizing the length of checking sequences[END_REF][START_REF] Tretmans | Test generation with inputs, outputs, and quiescence[END_REF][START_REF] Petrenko | Testing from partial deterministic FSM specifications[END_REF]. Other notations use state-based machines as the underlying semantics [START_REF] Huang | Exhaustive model-based equivalence class testing[END_REF][START_REF] Moraes | A family of test selection criteria for timed input-output symbolic transition system models[END_REF].

CSP [START_REF] Roscoe | Understanding Concurrent Systems[END_REF] has been used as a modelling notation for test derivation. The pioneering work in [START_REF] Peleska | Test automation of safety-critical reactive systems[END_REF] formalises a test-automation approach based on CSP. More recently, CSP and its model checker FDR [START_REF] Gibson-Robinson | FDR3 A Modern Refinement Checker for CSP[END_REF] have been used to automate test generation with ioco as a conformance relation [START_REF] Nogueira | Test generation from state based use case models[END_REF]. A theory for testing for refinement from CSP has been fully developed in [START_REF] Cavalcanti | Testing for Refinement in Circus[END_REF].

Two sets of tests have been defined and proved to be exhaustive: they can detect any SUT that is non-conforming according to traces or failures refinement. Typically, however, these test sets are infinite. A few selection criteria have been explored: data-flow and synchronisation coverage [START_REF] Cavalcanti | Data Flow coverage for Circus-based testing[END_REF], and mutation testing [START_REF] Alberto | Formal mutation testing for Circus[END_REF] for a state-rich version of CSP. The traditional approaches for test generation from state-based models have not been studied in this context.

Even though the operational semantics of CSP defines a Labelled Transition System (LTS), applying testing approaches based on states in this context is challenging: i) not every process has a finite LTS, and it is not trivial to determine when it has; ii) even if the LTS finite, in may not be deterministic; iii) for refinement, we are not interested in equivalence of LTS; and iv) to deal with failures, the notion of state needs to be very rich.

Here, we present a novel approach for selection of finite test sets from CSP models by identifying scenarios where the verdict of a campaign can be reached after a finite number of test executions. We adopt the concept of fault domain from state-based methods to constrain the possible faults in an SUT [START_REF] Petrenko | On fault coverage of tests for finite state specifications[END_REF]. Faultbased testing is more general than the criteria above, since the test engineering can embed knowledge about the possible faults of the SUT into a fault domain to guide generation and execution [START_REF] Koufareva | Yevtushenko Test Generation Driven by Userdefined Fault Models[END_REF]. We define a fault domain as a CSP process that is assumed to be refined by the SUT. With that, we establish that some tests are not useful, as they cannot reveal any new information about the SUT.

In addition, we propose a procedure for online generation of tests for traces refinement. Tests are derived and applied to the SUT and, based on the verdict, either the SUT is cast incorrect, or the fault domain is refined.

We present some scenarios where our procedure is guaranteed to provide a verdict after a finite number of steps. A simple scenario is that of a specification with a finite set of traces: unsurprisingly, after that set is exhaustively explored our procedure terminates. A more interesting scenario is when the SUT is incorrect; our procedure also always terminates in this case.

We have also investigated the scenario where the set of traces of the specification is infinite, but that of the SUT is finite and the SUT is correct. A challenge in establishing termination is that, while when testing using Mealy and finite state machines every trace of the model leads to a test, this is not the case with CSP. For example, for traces refinement, traces of the specification that lead to states in which all possible events are accepted give rise to no tests. After such a trace, the behavior of the SUT is unconstrained, and so does not need to be tested. Another challenge is that most CSP fault domains are infinite.

Our approach is similar to those adopted in the traditional finite statemachines setting, but addresses these challenges. We could, of course, change the notion of test and add tests for all traces. A test that cannot fail, however, is, strictly speaking, just a probe. For practical reasons, it is important to avoid such probes, which cannot really reveal faults.

The contributions of this paper are: 1) the introduction of the notion of fault domain in the context of a process algebra for refinement; 2) a procedure for online testing for traces refinement validated by a prototype implementation; and 3) the characterization of some scenarios in which the procedure terminates.

Next, in Section 2 we present background material: fault-based testing, and CSP and its testing theory. Section 3 casts the traditional concepts of fault-based testing in the context of CSP. Our procedure is presented in Section 4. Termination is studied in Section 5. Section 6 describes a prototype implementation of our procedure and its use in a case study. Finally, we conclude in Section 7.

Preliminaries

In this section, we describe the background material to our work.

CSP: testing and refinement

CSP is distinctive as a process algebra for refinement. In CSP models, systems and components are specified as reactive processes that communicate synchronously via channels. A prefixing a → P is a process that is ready to communicate by engaging in the event a and then behaves like P . The external choice operator 2 combines processes to give a menu of options to the environment.

Example 1. The process Counter uses events add and sub to count up to 2.

Counter = add → Counter 1 Counter 1 = add → Counter 2 2 sub → Counter Counter 2 = sub → Counter 1
Counter 1 offers a choice to increase (add ) or decrease (sub) the counter.

2

Other operators combine processes in internal (nondeterministic) choice, parallel, sequence, and so on. Nondeterminism can also be introduced by interleaving and by hiding internal communications, for example. There are three standard semantics for CSP: traces, failures, and failure-divergences, with refinement as the notion of conformance. As usual, the testing theory assumes that specifications and the SUT are free of divergence, which is observed as deadlock in a test. So, tests are for traces or failures refinement.

We write P T Q when P is trace-refined by Q; similarly, for P F Q and failures-refinement. In many cases, definitions and results hold for both forms of refinement, and we write simply P Q. In all cases, P Q requires that the observed behaviours of Q (either its traces or failures) are all possible for P .

The CSP testing theory adopts two testability hypothesis. The first is often used to deal with a nondeterministic SUT: there is a number k such that, if we execute a test k times, the SUT produces all its possible behaviours. (In the literature, it appears in [START_REF] Milner | A Calculus of Communicating Systems[END_REF][START_REF] Tretmans | Test generation with inputs, outputs, and quiescence[END_REF][START_REF] Luo | Test selection based on communicating nondeterministic finite-state machines using a generalized Wp-method[END_REF], for example, as fairness hypothesis or all-weather assumption.) The second testability hypothesis is that there is an (unknown) CSP process SUT that characterises the SUT.

The notion of execution of a test T is captured by a process Execution S SUT (T ) that composes the SUT and the test T in parallel, with all their common (specification) events made internal. Special events in T give the verdict: pass, fail , or inc, for inconclusive tests that cannot be executed to the end because the SUT does not have the trace that defines the test.

The testing theory also has a notion of successful testing experiment: a property passes (S , SUT , T ) defines that the SUT passes the test T for specification S . A particular definition for passes (S , SUT , T ) typically uses the definition of Execution S SUT (T ), but also explains how the information arising from it is used to achieve a verdict. For example, for traces refinement, we have the following.

passes T (S , SUT , T ) = ∀ t : traces [[Execution S SUT (T )]] • last(t) = fail
For a definition of passes (S , SUT , T ) and a test suite TS , we use the notation passes (S , SUT , TS ) as a shorthand for ∀ T : TS • passes (S , SUT , T ).

In general, for a given definition of passes (S , SUT , T ), we can characterise exhaustivity Exhaust (TS ) of a test suite TS as follows.

Definition 1. A test suite TS satisfies the property Exhaust (S , TS ), that is, it is exhaustive for a specification S and a conformance relation exactly when, for every process P , we have S P ⇔ passes (S , P , TS ).

Different forms of test give rise to different exhaustive sets. We use Exhaust (S ) to refer to a particular exhaustive test suite for S and .

For a trace a 1 , a 2 , . . . with events a 1 , a 2 , and so on, and one of its forbidden continuations a, that is, an event a not allowed by the specification after the trace, the traces-refinement test T T ( a 1 , a 2 , . . . , a) is given by the process inc → a 1 → inc → a 2 → ... → pass → a → fail . In alternation, it gives an inc verdict and offers an event of the trace to the SUT, until all the trace is accepted, when it gives the verdict pass, but offers the forbidden continuation. It it is accepted, the verdict is fail . The exhaustive test set Exhaust T (S ) for traces refinement includes all tests T T (t, a) formed in this way from the traces t and forbidden continuations a of the specification.

Example 2. We consider the specification S 1 = a → b → S 1 . The exhaustive test set for for S 1 and traces refinement is sketched below.

{ pass → b → fail → STOP , inc → a → pass → a → fail → STOP , inc → a → inc → b → pass → b → fail → STOP , . . .} 2
In [START_REF] Cavalcanti | Testing for Refinement in CSP[END_REF], it is proven that Exhaust T (S , Exhaust T (S )).

Fault-based testing

The testing activity is constrained by the amount of resources available. Some criteria is needed to select a finite subset of finite tests. Fault-based criteria consider that there is a fault domain, modelling the set of all possible faulty implementations [START_REF] Petrenko | On fault coverage of tests for finite state specifications[END_REF][START_REF] Koufareva | Yevtushenko Test Generation Driven by Userdefined Fault Models[END_REF]. They restrict the set of required tests using the assumption that the SUT is in that domain [START_REF] Yu | Fault-based test suite prioritization for specification-based testing[END_REF]. Testing has to consider the possibility that the SUT can be any of those implementations, but no others [START_REF] Morell | A theory of fault-based testing[END_REF].

For Finite State Machines (FSMs), many test-generation techniques assume that the SUT may have a combination of initialisation faults (that is, the SUT initialises in a wrong state), output faults (that is, the SUT produces a wrong output for a given input), transfer faults (that is, a transition of the SUT leads to the wrong states), and missing or extra states (that is, the set of states of the SUT is increased or decreased). Therefore, for a specification with n states, it is common that the fault domain is defined denotationally as "the set of FSMs (of a given class) with no more than m states, for some m ≥ n." [START_REF] Fujiwara | Testing non-deterministic state machines with fault coverage[END_REF][START_REF] Chow | Testing software design modeled by finite-state machines[END_REF][START_REF] Hierons | Optimizing the length of checking sequences[END_REF]. In this case, all faults above are considered, except for more extra states than m -n.

Fault domains can also be used to restrict testing to parts of the specification that the tester judges more relevant. For instance, some events of the specification can be trivial to implement and the tester may decide to ignore them. An approach for modelling faults of interest, considering FSMs, is to assume that the SUT is a submachine of a given non-deterministic FSM, as in [START_REF] Koufareva | Yevtushenko Test Generation Driven by Userdefined Fault Models[END_REF]. Thus, the parts of the SUT that are assumed to be correct can be easily modelled by a copy the specification; the faults are then modelled by adding extra transitions with the intended faults. Fault domains can also be modelled by explicitly enumerating the possible faulty implementations, known as mutants [START_REF] El-Fakih | FSM-based testing from user defined faults adapted to incremental and mutation testing[END_REF]. Thus, tests can be generated targetting each of those mutants, in turn.

In the next section, we define fault domains by refinement of a CSP process.

Fault-based testing in CSP

For CSP, we define a fault domain as a process FD SUT ; it characterises the set of all processes that refine it. We use the term fault domain sometimes to refer to the CSP process itself and sometimes to the whole collection of processes it identifies. In the CSP testing theory, the specification and SUT are processes over the same alphabet of events. Accordingly, here, we assume that a fault domain FD uses only those events as well.

The usefulness of the concept of fault domain is illustrated below.

Example 3. For S 1 in Example 2, we first take just FD 1 = RUN ({a, b}) as a fault domain. For any alphabet A, the process RUN (A) repeatedly offers all events in A. So, with FD 1 , we add no extra information, since every process that uses only channels a and b trace refines

FD 1 . A more interesting example is FD 2 = a → (a → FD 2 2 b → FD 2 )
. In this case, the assumption that FD 2 T SUT allows us to eliminate the first and the third tests in Example 2, because an SUT that refines FD 2 always passes those tests.

2

In examples, we use traces refinement as the conformance relation, and assume that we have a fixed notion of test. The concepts introduced here, however, are relevant for testing for either traces or failures refinement. It is traditional in the context of Mealy machines to consider a fault domain characterised by the size of the machines, and so, finite. Here, however, if a fault domain FD has an infinite set of traces, it may have an infinite number of refinements. For traces refinement, for example, for each trace t, a process that performs just t refines FD. So, we do not assume that fault domains are finite.

Just like we define the notion of exhaustive test set to identify a collection of tests of interest, we define the notion of a complete test set, which contains the tests of interest relative to a fault domain.

Definition 2. For a specification S , and a fault domain FD, we define a test set TS : P Exhaust (S ) to be complete, written Complete S (TS , FD), with respect to FD if, and only if, for every implementation I in FD we have

¬ (S I ) ⇒ ∃ T : TS • ¬ passes (S , I , T )
This is a property based not on the whole of the fault domain, but just on its faulty implementations. For traces refinement, the exhaustive test set is given by Exhaust T (S ) and the verdict by passes T (S , SUT , T ) defined in Section 2.1.

If FD is the bottom of the refinement relation , then a complete test set TS is exhaustive. It is direct from Definition 2 the fact that a complete test set is a subset of the exhaustive test set and, therefore, unbiased, that is, it does not reject correct programs. We also need validity: only correct programs are accepted. This is also fairly direct as established in the theorem below.

⇒ (S SUT ) [predicate calculus] 2
Finally, if an unbiased test is added to a complete set, the resulting set is still complete. Unbias follows from inclusion in the exhaustive test set. An important set is those of the useless tests for implementations in the fault domain. The fact that we can eliminate such tests from any given test suite has an important practical consequence.

Definition 3.

Useless (S , FD) = {T : Exhaust (S ) | passes (S , FD, T )} Since FD passes the tests in Useless (S , FD), all implementations in that fault domain also pass those tests, provided passes (S , P , T ) is monotonic on P with respect to refinement. This is proved below. Lemma 1. For every I in FD, and for every T : Useless (S , FD), we have passes (S , I , T ), if passes (S , P , T ) is monotonic on P with respect to . We recall that the definition for passes T (S , SUT , T ) is monotonic, as shown below, where we consider processes P 1 and P 2 such that P 1 T P 2 .

Proof

Execution S P1 (T ) = (P 1 |[ αS ]| T )\αS [definition of Execution] ⇒ Execution S P1 (T ) T (P 2 |[ αS ]| T )\αS [monotonicity of CSP operators with respect to refinement] = Execution S P1 (T ) T Execution S P2 (T ) [definition of Execution] ⇒ traces [[Execution S P2 (T )]] ⊆ traces [[Execution S P1 (T )]] [definition of T ] ⇒ (∀ t : traces [[Execution S P1 (T )]] • last(t) = fail ) ⇒ (∀ t : traces [[Execution S P2 (T )]] • last(t) = fail ) [predicate calculus] = passes T (S , P 1 , T ) ⇒ passes T (S , P 2 , T ) [definition of passes T ] 2
Typically, it is expected that the notions of passes (S , P , T ) are monotonic on P with respect to the refinement relation : a testing experiment that accepts a process, also accepts its correct implementations.

It is important to note that there are tests that do become useless with a fault-domain assumption. This is illustrated below.

Generating test sets

To develop algorithms to generate tests based on a fault domain, we need to consider particular notions of refinement, and the associated notions of test and verdict. In this paper, we present an algorithm for traces refinement.

A particular execution of the test can result in the verdicts inc, pass or fail. Due to nondeterminism in the SUT, the test may need to be executed multiple times, resulting in more than one verdict. We assume that the test is executed as many times as needed to observe all possible verdicts according to our testability hypothesis. So, for a test T and implementation SUT , we write verd SUT (T ) to denote the set of verdicts observed when T is executed to test SUT .

If fail ∈ verd SUT (T ), the SUT is faulty (if T is in Exhaust (TS )). In this case, we can stop the testing activity, since the SUT needs to be corrected. Otherwise, we can determine additional properties of the SUT, considering the test verdicts. The SUT is a black box, but combining the knowledge that it is in the fault domain and has not failed a test, we can refine the fault domain.

If fail ∈ verd SUT (T ), both inc and pass bring relevant information. We consider a test T T (t, a), and recall that the SUT refines the fault domain FD.

If pass ∈ verd I (T T (t, a)), then t ∈ traces [[SUT ]], but t a ∈ traces [[SUT ]
]. Thus, the fault domain can be updated, since we have more knowledge about the SUT: it does not have the trace t a . Otherwise, if verd I (T T (t, a)) = {inc}, the trace t was not completely executed, and hence the SUT does not implement t. We can, therefore, update the fault domain as well.

In both cases, we include in the fault domain knowledge about traces not implemented. Information about implemented traces is not useful: given the definition of traces refinement, it cannot be used to reduce the fault domain.

Given a fault domain FD and a trace t, such that t ∈ traces [[SUT ]], we define a new fault domain as follows. First, we define a process NOTTRACE (t), which tracks the execution of each event in t, behaving like the process RUN (Σ) if the corresponding event of the trace does not happen. If we get to the end of t, then NOTTRACE (t) prevents its last event from occurring. It, however, accepts any other event, and, at that point, also behaves like RUN (Σ).

NOTTRACE ( a ) = 2 e : Σ \ {a} • e → RUN (Σ) NOTTRACE ( a t) = a → NOTTRACE (t) 2 (2 e : Σ \ {a} • e → RUN (Σ))
Formally, if the monitored trace is a singleton a , then a is blocked by the process NOTTRACE ( a ). It offers in external choice all events except a: those in the set Σ of all events minus {a}. If a different event e happens, then a is no longer possible and the monitor accepts all events. If the monitored trace is a t, for a non-empty t, then, if a happens, we monitor t. If a different event e happens, then a t is no longer possible and the monitor accepts all events. We notice that NOTTRACE is not defined for the empty trace, which is a trace of every process, and that, as required, t ∈ traces [[NOTTRACE (t)]]. On the other hand, for any trace s that does not have t as a prefix, we have that s ∈ traces [[NOTTRACE (t)]]. To obtain a refined fault domain FDU (t), we compose FD in parallel with NOTTRACE (t). The parallelism requires synchronisation on all events and, therefore, controls the occurrence of events as defined by NOTTRACE (t). So, the fault domain defined by FDU (t) excludes processes that perform t.

FDU (t) = FD |[ Σ ]| NOTTRACE (t)
Since t ∈ traces [[SUT ]] and FD T SUT , then FDU (t) T SUT . Thus, we have FD T FDU (t) T SUT . If the fault domain trace refines the specification S , we have that S T FD T SUT ; thus, we can stop testing, since S T SUT .

Based on these ideas, we now introduce a procedure TestGen for test generation. It is shown for a specification S , an implementation SUT , and an initial fault domain FD init . In the case that there is no special information about the implementation, the initial fault domain can be simply RUN (Σ).

TestGen uses local variables failed , to record whether a fault has been found as a result of a test whose execution gives rise to a fail verdict, and FD, to record the current fault domain. Initially, their values are false and FD init . A variable TS records the set of traces for which tests are no longer needed, because all its forbidden continuations, if any, have already been used for testing.

The procedure loops until it is found that the specification is refined by the fault domain or a test fails. In each iteration, we select a trace t that belongs both to the specification and the fault domain (Step 6). A trace of the specification that is not of the fault domain is guaranteed to lead to an inconclusive verdict, as it is necessarily not implemented by the SUT.

Next, we check whether t has a continuation that is allowed by the fault domain FD, but is forbidden by S . If it has, we choose one of these forbidden continuations a (Step 8). If not, t is not (or no longer) useful to construct tests, and is added to TS . A forbidden continuation a of S that is also forbidden by FD is guaranteed to be forbidden by the SUT. So, testing for a is useless.

The resulting test T T (t, a) is used and the set of verdicts verd is analysed as explained above, leading to an update of the fault domain. The value returned by the procedure indicates whether the SUT trace refines S or not.

Example 6. We consider as specification the Counter from Example 1. A few tests for traces refinement obtained by applying T T (t, a) to the traces t of Counter are sketched below in order of increasing length.

T T ( , sub) = pass → sub → fail → STOP T T ( add , sub , sub) = inc → add → inc → sub → pass → sub → fail → STOP T T ( add , add , add ) = inc → add → inc → add → pass → add → fail → STOP T T ( add , add , sub, add , add ) =
inc →add →inc →add →inc →sub →inc →add →pass →add →fail →STOP T T ( add , add , sub, sub , sub) = . . . This is, of course, an infinite set, arising from an infinite set of traces. We note, however, that there are no tests for a trace that has one more occurrence of add than sub, since, in such a state, Counter has no forbidden continuations.

The verdicts depend on the particular SUT; we consider below one example: SUT = add → add → STOP . We note that, at no point, we use our knowledge of the SUT to select tests. That knowledge is used just to identify the result of the tests used in our procedure.

In considering TestGen(Counter , SUT , RUN (Σ)), the first test we execute is T T ( , sub), whose verdict is pass. So, we have sub ∈ traces [[SUT ]], and the updated fault domain is FD 1 = NOTTRACE ( sub ) = add → RUN (Σ). The parallelism with the fault domain RUN (Σ) does not change NOTTRACE ( sub ).

Counter is not refined by FD 1 , which after the event add has arbitrary behaviour. The next test is T T ( add , sub , sub), whose verdict is inc. Thus, we have that add , sub ∈ traces [[SUT ]]. Now, the fault domain is FD 2 below.

FD 2 = FD 1 |[ Σ ]| NOTTRACE ( add , sub ) = (add → RUN (Σ)) |[ Σ ]| (sub → RUN (Σ) 2 add → add → RUN (Σ)) = add → add → RUN (Σ)
The next test is T T ( add , add , add ) with verdict pass. Thus, FD 3 is the process add → add → sub → RUN (Σ). Next, T T ( add , add , sub, add , add ) gives verdict inc, and we get FD 4 = add → add → sub → sub → RUN (Σ) when we update the fault domain. Finally, T T ( add , add , sub, sub , sub) has verdict inc as well. So, FD 5 = add → add → sub → STOP is the new domain. Since Counter T FD 5 , the procedure terminates indicating that SUT is correct. 2

Our procedure, however, may never terminate. We discuss below some cases where we can prove that it does.

Generating test sets: termination

A specification that has a finite set of (finite) traces is a straightforward case, since it suffices to test with each trace and each forbidden continuation. Our procedure, however, can still be useful, because useless tests may be used if the fault domain is not considered. Our procedure can reduce the number of tests.

In this scenario, our procedure terminates because, for any maximal trace t of the specification (that is, a trace that is not a prefix of any other of its traces), all events are forbidden continuations. Thus, once t is selected and all tests derived from the forbidden continuations are applied, either we find a fault, or the fault domain is refined to a process that has no traces that extends t.

When all maximal traces of the specification are selected (and the corresponding tests are applied), if no test returns a fail verdict, no trace of the fault domain extends a maximal trace of the specification. Thus, if no test returns a fail verdict, any trace of the fault domain is a trace of the specification and the procedure stops indicating success, since, in this case, S T FD.

We now discuss a scenario where the specification does not have a finite set of traces, but the SUT does. Once a trace t is selected, if the set of events, and, therefore, forbidden continuations is finite, with the derived tests, we can determine whether or not the SUT implements any of the forbidden continuations. Moreover, if no pass verdict is observed, t itself is not implemented.

We note that if the SUT is incorrect, that is, it does not trace refine the specification, the procedure always terminates. Let t be the longest prefix of s that is a trace of S , that is, the longest trace in pref (s) ∩ traces [[S ]], which gives rise to the shortest test that reveals an invalid prefix of s. Let a be such that t a ∈ traces

[[SUT ]] \ traces [[S ]]. We know that a is a forbidden continuation of t, since t ∈ traces [[S ]], but t a / ∈ traces [[S ]]. Moreover, since traces [[SUT ]] ⊆ traces [[FD]], it follows that t a ∈ traces [[FD]];
hence a ∈ initials(FD/t)\initials(S /t). Thus, there exists a test T T (t, a) which, when applied to the SUT produces a fail verdict.

Since t is the longest trace in pref (s)∩traces [[S ]], tests generated for any prefix of t do not exclude t from the traces of the updated fault domain. Moreover, the event a remains in initials(FD/t) \ initials(S /t), since no tests for traces longer than t are applied before t. Therefore, the test T T (t, a) is applied (unless a test for a trace of the same length of t is applied and the verdict is fail , in which case the result also follows). In this case, TestGen(S , FD init , SUT ) assigns true to the variable failed , since the verdict is fail and terminates with ¬ failed , that is, false.

2 Now we consider the case when the SUT is correct and finite. For some specifications, like the Counter from Example 1 the procedure terminates, but not for all specifications as illustrated below.

Example 7. We consider UNBOUNDED = a → UNBOUNDED 2 b → STOP , the initial fault domain FD init = RUN (Σ), where Σ = {a, b}, and the SUT STOP . In TestGen(UNBOUNDED, SUT , RUN (Σ)), the first trace we choose is , for which there is no forbidden continuation, and so, no test. The next trace is a , for which again there is no forbidden continuation. For b , the events a and b are forbidden continuations; the test T T ( b , a) results in an inc verdict. Thus, the fault domain is updated to

FD 1 = FDU (FD init , b ) below. FD 1 = FD init |[ Σ ]| NOTTRACE ( b ) = RUN (Σ) |[ Σ ]| a → RUN (Σ) = a → RUN (Σ)
As expected, b is not a trace of the fault domain anymore and no further tests are generated for it: it is never again selected in Step 6.

The next trace we select is a, a , for which there is no forbidden continuation. Then, we select a, b , with forbidden continuations a and b. T T ( a, b , a) is executed with an inc verdict. The next fault domain is

FD 2 = FDU (FD 1 , a, b ). FD 2 = FD 1 |[ Σ ]| NOTTRACE ( a, b ) = (a → RUN (Σ)) |[ Σ ]| (b → RUN (Σ) 2 a → a → RUN (Σ)) = a → a → RUN (Σ)
In fact, the refined fault domains are always of the form a → a → ... → a → RUN (Σ) This is because there is no test generated for a trace a k , for k ≥ 0. So, the procedure does not terminate. This happens for any correct SUT with respect to the specification UNBOUNDED. For an incorrect SUT , the procedure terminates. 2 Example 8. We now consider Counter and why our procedure stops for its correct finite implementations. First, we note that our procedure uses traces of increasing length for deriving and applying tests, and for a finite SUT , there is a k such that all traces of the SUT are shorter than k . We consider a trace t ∈ traces [[Counter ]] of length k . There are three possibilities for Counter /t. If Counter /t = Counter or Counter /t = Counter 2, we have initials(Counter /t) = Σ and, thus, there is a test T T (t, a) for a forbidden sub or add . The verdict for this test is inc because the SUT has no trace of the length of t and the fault domain is updated, removing t as a trace of the fault domain and, thus, as a possible trace of the SUT . If Counter /t = Counter 1, we have that initials(Counter /t) = Σ and no test can be derived from t. However, for each trace s, such that t s ∈ traces [[Counter ]], s starts with either add or sub. In either case, a test will be generated, since Counter /t add = Counter 2 and Counter /t sub = Counter 1, for which there are tests, as seen before. For those tests, the verdict is inc, the fault domain is similarly updated, and the traces t add and t sub are removed. The fact that t for which Counter /t = Counter 1 cannot be arbitrarily extended just to traces without tests is the key property required for the procedure to terminate.

For some specifications, like UNBOUNDED, there may be no tests for an unboundedly long trace. In this case, a correct SUT does not fail and, in spite of this, no test is applied that prunes the fault domain.

2

To characterise the above termination scenario, we introduce some notation. Given traces r and t, we say that r is a prefix of t, denoted r ≤ t if there exists s, such that r s = t. A prefix is proper, denoted r < t, if s = . We say that t is a (proper) suffix of r if, and only if, r is a (proper) prefix of t. We denote by pref (t) all prefixes of t, that is, pref (t) = {s : Σ * | s ≤ t}, and by ppref (t), all proper prefixes of t, that is, ppref (t) = pref (t) \ {t}. Similarly, we denote by suff (t) the set of all suffixes of t.

For a process S and k ≥ 0, we define the set traces

[[S ]] k of the traces of S of length k . Formally, traces [[S ]] k = {t : traces [[S ]] | #t = k }.
Another subset hfc(S , FD) of traces of S includes those for which there is at least a forbidden continuation that takes into account the fault domain. Formally, hfc(S , FD) = {t : traces [[S ]] | initials(FD/t) \ initials(S /t) = ∅}. Importantly, for each t ∈ hfc(S , FD), there exists at least one test T T (t, a) for a forbidden continuation a that is allowed by the fault domain. Finally, given a set of traces Q, we denote by minimals(Q) the set of traces of Q that are not a proper prefix of another trace in Q. Formally,

minimals(Q) = {t : Q | ¬ ∃ s : Q • t < s}.
We use hfc(S , FD) to define conditions for termination of the procedure.

Lemma 3. For a specification S and a fault domain FD init , if for any finite set of traces P ⊆ traces [[S ]], there exists a k ≥ 0, such that, for each r ∈ traces [[S ]] k , we have that there is a prefix of r that is not in P and has a forbidden continuation, that is, ((pref (r ) \ P ) ∩ hfc(S , FD init )) = ∅, then TestGen(S , FD init , SUT ) terminates for any finite SUT .

Proof If ¬ (S T SUT ), by Lemma 2, the procedure terminates. We, therefore, assume that S T SUT , and so traces For each t ∈ M , there exists a ∈ initials(FD init /t) \ initials(S /t), since t ∈ hfc(S , FD init ) and from the definition of hfc(S , FD init ). Then, if the test T T (t, a) is applied to the SUT , the verdict is inc, since

t ∈ traces [[SUT ]] because t ∈ M ⊆ Q and Q ∩ traces [[SUT ]] = ∅.
In this case, the fault domain is updated so that t is not a trace of the fault domain anymore.

Thus, if all tests derived for each t ∈ M are applied, we obtain a fault domain FD such hat traces [[FD]] ⊆ pref (M ). As all traces in M have length at most k , eventually, all traces in M are selected (unless the procedure has already terminated) and the tests derived for those traces are applied. As pref

(M ) ⊆ Q ⊆ hfc(S , FD init ) ⊆ traces [[S ]], it follows that traces [[FD]] ⊆ traces [[S ]],
that is, S T SUT . TestGen(S , FD init , SUT ) then terminates, with failed = false, and the result is true.

2 One scenario where the conditions in Lemma 3 hold is if there is an event in the alphabet which is not used in the model. In this case, that event is always a forbidden continuation and thus a test is generated for all traces. Even though this can be rarely the case for a specification at hand, the alphabet can be augmented with a special event for the purpose, guaranteeing that the procedure terminates. Such an event would act as a probe event. As said before, in practice, it is best to avoid probes since the tests that they induce can reveal no faults.

Tool support and case studies

We have developed a prototype tool that implements our procedure. The tasks related to the manipulation of the CSP model, such as checking refinement, computing forbidden continuations, determining verdicts, and so on, are handled by FDR. The tool is implemented in Ruby. It submits queries (assert clauses) to FDR and parses FDR's results in order to perform the computations required by the procedure. Specifically, FDR is used in two points:

1. for checking whether the specification refines the fault domain (Line 5). It is a straightforward refinement check in FDR; 2. for computing initials and forbidden continuations (Lines 7 and 8). For instance, to compute the complement of initials(S /t), we invoke FDR to check S T TTHENANY (t), where S is compared to the process TTHENANY (t) that performs t and then any event e from Σ. It is defined as follows.

TTHENANY ( ) = 2 e : Σ • e → STOP TTHENANY ( a t) = a → TTHENANY (t)

If t is a trace of S , counterexamples to this refinement check provide traces t e , where e is not in the set initials(S /t). Thus, we obtain initials(S /t) by considering the events in Σ for which no such counterexample exists. Currently, our prototype calls FDR many times from scratch. As a future optimization, we will incorporate the caching of the internal results of the FDR, to speed up posterior invocations with the same model.

We have used our prototype to carry out two case studies, the Transputerbased sensor for autonomous vehicles in [START_REF] Probert | Transputer architectures for sensing in a robot controller: Formal methods for design[END_REF], and the Emergency Response System (ERS) in [START_REF] Andrews | Model-based development of fault tolerant systems of systems[END_REF]. The sensor is part of an architecture where each sensor is associated with a Transputer for local processing and can be part of a network of sensors. The ERS allows members of the public to identify incidents requiring emergency response; it is a system of operationally independent systems (a Phone System, a Call Center, an Emergency Response Unit, and so on). The ERS ensures that every call is sent to the correct target. It is used in [START_REF] Mota | Rapid prototyping of a semantically well founded Circus model checker[END_REF] to assess the deadlock detection of a prototype model checker for Circus.

For each case study, we have randomly generated 1000 finite SUTs with the same event alphabet. The experimental results confirm what we expected from the lemmas of the previous section. Namely, all incorrect SUTs are identified and the procedure terminates for all finite SUTs identified in Lemma 3. The prototype tool and the CSP model for the sensor, the ERS and other examples are in http://www.github.com/adenilso/CSP-FD-TGen. The data for the SUTs used in this case study is also available.

Conclusions

In this paper, we have investigated how fault domains can be used to guide test generation from CSP models. We have cast core notions of fault-domain testing in the context of the CSP testing theory. For testing for traces refinement, we have presented a procedure which, given a specification and a fault domain, it tests whether an SUT trace refines the fault domain. If the SUT is incorrect, the procedure selects a test that can reveal the fault. In the case of a correct SUT, we have stated conditions that guarantee that the procedure terminates.

There are specifications for which the procedure does not terminate. We postulate that for those specifications, there is no finite set of tests that is able to demonstrate the correctness of the SUT. Finiteness requires extra assumptions about the SUT. We plan to investigate this point further in future work.

The CSP testing theory also includes tests for conf , a conformance relation that deals with forbidden deadlocks; together, tests for conf and traces refinement can be used to establish failures refinement. Another interesting failuresbased conformance relation for testing from CSP models takes into account the asymmetry of controllability of inputs and outputs in the interaction with the SUT [START_REF] Cavalcanti | Testing with Inputs and Outputs in CSP[END_REF]. It is worth investigating how fault domains can be used to generate finite test sets for these notions of conformance.

Theorem 1

 1 Provided FD SUT , we have that ∃ TS : P Exhaust (S ) • complete(TS , FD) ∧ passes (S , SUT , TS ) implies S SUT . Proof ∃ TS : P Exhaust (S ) • complete(TS , FD) ∧ passes (S , SUT , TS ) = ∃ TS : P Exhaust (S ) • (¬ (S SUT ) ⇒ ∃ T : TS • ¬ passes (S , SUT , T )) ∧ passes (S , SUT , TS ) [Definition 2] = ∃ TS : P Exhaust (S ) • (passes (S , SUT , TS ) ⇒ S SUT ) ∧ passes (S , SUT , TS ) [predicate calculus and definition of passes]

⇒ 2 Example 4 .

 24 passes (S , FD, T ) ⇒ passes (S , I , T ) [monotonicity of passes] = T ∈ Useless (S , FD) ⇒ passes (S , I , T ) [definition of Useless (S , FD)]

Example 5 .

 5 In Example 3, the first and third tests of the exhaustive test set are useless as already indicated. For instance, we can show that FD 2 passes the first test T 1 = pass → b → fail → STOP as follows. Execution S1 FD2 (T 1 ) = (FD 2 |[ {a, b} ]| T 1 ) \ {a, b} [definition of Execution] = (pass → (FD 2 |[ {a, b} ]| b → fail → STOP )) \ {a, b} [step law of parallelism] = pass → (FD 2 |[ {a, b} ]| b → fail → STOP ) \ {a, b} [step law of hiding] = pass → STOP \ {a, b} [step law of parallelism] = pass → STOP [step law of hiding] So, traces [[Execution S1 FD2 (T 1 )]] = { , pass }, none of which finish with fail . 2

Lemma 2 .

 2 If ¬ (S T SUT ), then TestGen(S , FD init , SUT ) terminates (and returns false), for any fault domain FD init and finite SUT . Proof By ¬ (S T SUT ), there exists a trace s ∈ traces [[SUT ]] \ traces [[S ]].

  [[SUT ]] ⊆ traces [[S ]]. Finiteness of the SUT means that traces [[SUT ]] is finite. Let k ≥ 0 be such that, for each r ∈ traces [[S ]] k , we have ((pref (r ) \ traces [[SUT ]]) ∩ hfc(S , FD init )) = ∅. This k is larger than the size of the largest trace of SUT , since otherwise pref (r ) \ traces [[SUT ]] is empty, and it exists because traces [[SUT ]] is finite. Let now Q = (pref (traces [[S ]] k ) \ traces [[SUT ]]) ∩ hfc(S , FD init ) and let M = minimals(Q). Let p ∈ traces [[SUT ]]. Let r ∈ traces [[S ]] k be such that p ≤ r . There is at least an s ∈ pref (r ), such that p ≤ s and s ∈ hfc(S , FD init ) because ((pref (r ) \ traces [[SUT ]]) ∩ hfc(S , FD init )) = ∅. Without loss of generality, assume that s is the shortest such a trace. Thus, s ∈ M and p ∈ pref (M ), since p ≤ s. It follows that traces [[SUT ]] ⊆ pref (M ) since p is arbitrary.

Acknowledgements

The authors would like to thank the partial financial support of the following entities: Royal Society (Grant: NI150186), FAPESP (Grant: 2013/07375-0). The authors also are thankful to Marie-Claude Gaudel, for the useful discussion in an early version of this paper.


Roland Groz

Adenilso Simao
email: adenilso@icmc.usp.br

Catherine Oriat

Adaptive Localizer Based on Splitting Trees

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

Introduction

In testing methods based on FSM models, it is important to ensure that the black box implementation under test is in a known state at key points after applying some prefix input sequence, and before applying a trailing sequence. The same is also true when the test is used to retrieve some kind of state model information from a black box, as in the inference problem.

Hennie [START_REF] Hennie | Fault-detecting experiments for sequential circuits[END_REF] and Kohavi [START_REF] Kohavi | Checking experiments for sequential machines[END_REF] introduced approaches based on locating sequences, to build checking sequences, that can test for conformance. More recently, we introduced a localizer procedure to infer a FSM model of a black box system which cannot be reset [START_REF] Groz | Inferring finite state machines without reset using state identification sequences[END_REF] with two key assumptions: first, an upper bound n on the number of states, and second a characterization set (aka W -set) for the system. Whatever the initial state of the system, the application of the localizer will make it possible to ascertain the state reached at the end of it, or more precisely before applying the last characterizing sequence. For W = {w 1 , w 2 , w 3 }, the localizer's input sequence is (w 2n-1 1 w 2 ) 2n-1 (w 2n-1 1 w 3 ). The core trick, as already suggested by Hennie, is that after applying at most n + 1 times a sequence, the machine must have entered a cycle, and we proved [START_REF] Groz | Inferring finite state machines without reset using state identification sequences[END_REF] that another n -2 applications were enough (in worst case) to identify where the machine is in the cycle, so as to predict the next application. After w 2n-1 1 the answer of the machine to w 1 can be predicted, so by applying w 2 we can know its answers to both w 1 and w 2 . Similarly, after (w 2n-1 1 w 2 ) 2n-1 we know what its answers would be to w 1 AND w 2 after applying w 2n-1 1 , so we now substitute w 3 and therefore we identify the state reached after (w 2n-1

1 w 2 ) 2n-1 w 2n-1 1
. The length of the sequence is exponential in the cardinal of the characterization set.

In this paper, we propose an improved localizer when the characterizing sequences are organized in a splitting tree [START_REF] Smetsers | Minimal separating sequences for all pairs of states[END_REF]. In that case, the length of the localizing sequence is exponential in the height of the tree, so it would reduce to linear in the number of sequences when the tree is balanced. The main difficulty lies in the fact that each input sequence from the W -set must be applied after repeating a fixed number of times (2n -1) a fixed sub-localizing sequence to ensure that the next iteration would be a repeated situation identifiable from the previous observations. The localizer procedure from [START_REF] Groz | Inferring finite state machines without reset using state identification sequences[END_REF] uses a fixed order of input sequences from the W -set to ensure that the same sequence is repeated at each level. With a splitting tree, the sequence to repeat may not be fixed. In this paper, we show that it is possible to combine variable sequences with predictability: differing from [START_REF] Jourdan | Reducing locating sequences for testing from finite state machines[END_REF], we allow cycles that hop through different states and levels up and down the tree. Our new localizer is adaptive, and it does not produce a fixed input sequence, but an adaptive one.

Definitions

In this paper, a FSM is assumed to be a strongly connected complete deterministic Mealy machine M = (Q, I, O, δ, λ), with finite state, input and output sets Q, I, O; δ and λ as transition and output mappings.

Two states q, q ∈ Q are distinguishable by a set H ⊂ I * if there exists a separating sequence γ ∈ H such that λ(q, γ) = λ(q , γ). An FSM is minimal if all states are pairwise distinguishable. A set W of sequences of inputs (therefore conventionally called a W -set) is a characterization set for an FSM M if each pair of states is distinguishable by W .

Figure 1 shows an FSM M 0 , taken from [START_REF] Smetsers | Minimal separating sequences for all pairs of states[END_REF], with 6 states, 2 inputs (a, b) and two outputs (0, 1). W = {b, aab, ab, aaab} is a characterization set for M 0 .

A localizer w.r.t. a set H ⊂ I * and n ∈ N is a procedure that applies an input sequence Ξγ to an unknown machine with at most n states such that γ ∈ H and the output responses to each sequence in H can be ascertained in the state reached after applying Ξ. Note that H is not required to be a characterization set, and we only assume we know a bound on the number of states. Following [START_REF] Smetsers | Minimal separating sequences for all pairs of states[END_REF], we now define splitting trees. A splitting tree for an FSM M = (Q, I, O, δ, λ) is a rooted tree T with a finite set of nodes such that:

each non-leaf node N is labelled by a non-empty sequence of inputs γ ∈ I + ; each edge e : N 1 → N 2 is labelled by a non-empty output sequence of outputs θ ∈ O + of the same length as the label of the source node N 1 .

A splitting tree T is separating for M if each node can be associated with a class of a partition of its states, such that:

the root of T is associated with the full set of states Q of the machine M ; let e : N 1 → N 2 be an edge of T such that N 1 is labelled by

γ ∈ I + , e is labelled by θ ∈ O + . If N 1 is associated with Q 1 ⊆ Q, then N 2 is associated with Q 2 = {q ∈ Q 1 ; λ(q, γ) = θ}.
A splitting tree is fully separating if each leaf node is associated with a single state. In that case, the input sequences from the root of the tree to a leaf separate the state on this leaf from all other states. The advantage of structuring a Wset as a splitting tree is that a state can be identified by applying less input sequences: with a W -set, we potentially have to apply Card W sequences, while with a splitting tree, we only have to apply log(Card W ) sequences, if the tree is balanced. As the localizer algorithm is exponential in Card W , the gain from using splitting trees rather than W -sets is crucial. In figure 1, we choose an initial sequence a / ∈ W that better balances the tree and splits on a short sequence. Given a splitting tree T , and a node N of T , we will use the following notations:

-We denote the subtree rooted at node N also by N .

root(T ) is the root node of T . Following the previous notation, this root node could also be denoted by T . -I(N ) is the input sequence that labels node N .

-Λ(N ) is the output sequence that labels the edge leading to node N .

-Given a child node N of N , T (N ← N ) is the modified tree where N has been replaced by the tree rooted at N . In other words, the subtree rooted at N is grafted one level upwards.

Adaptative localizer procedure

We assume we are given a FSM whose structure is unknown (so we cannot compute a homing sequence for it) but we are given T , a known separating splitting tree for it (see section 4 for a short discussion). The procedure L will bring the machine to an identified state, meaning that we know its output responses for all input sequences in a path of the splitting tree from the root to a leaf N . The procedure L should be called initially with d equal to the height of the splitting tree T . The boolean function Predictable(in i, in Nt, out N 1) returns true when we can be sure that the next (i-th) application of L(d -1, T ) would return a node N 1. N t is an array of nodes from the tree indexed from 0 to i -1.

12 if Nt[i] is a leaf then 13 return Nt[i]
// a leaf will be returned through all // recursive calls as we are now localized We now illustrate the algorithm on the example FSM M 0 and its associated splitting tree T . In the following, we will denote a node N of the tree T by the path from the root of T to N . For instance, the node associated with S3 will be denoted by a/1, ab/11 . We use primes to differentiate inner values of variables in recursive calls. We suppose we start in the state S0. The depth of the splitting tree T is 3, so the first call to the adaptative localizer is L(3, T ).

L(3, T )

i

:= 0 Nt[0] := L(2, T ) i := 0 Nt [0] := L(1, T ) apply a, observe 0 // we are now in S1 Nt [0] = a/0 i := i + 1 = 1 Nt [1] := L(1, T ) apply a, observe 1 // we are now in S2 Nt [1] = a/1 . . .
After five more iterations, we are in S1 and Nt = [ a/0 , a/1 , a/0 , a/1 , a/0 , a/1 , a/0 ] It is predictable that if we applied a, we would observe 1. Predictable(i, Nt , N 1) is true and N 1 = a/1 1 procedure Predictable(i, Nt, out N 1) return boolean The whole localizing sequence has 7 + 2 + 7 + 1 = 17 inputs as follows (here decorated with landmark steps S , S ): a/0 a/1 a/0 a/1 a/0 a/1 a/0 S ab/10 a/1 a/0 a/1 a/0 a/1 a/0 a/1 S b/1

Let us recap: in the state S , we know that if we applied a, we would get 1. We thus apply the input sequence associated with node a/1 , which is ab, and get 10. In the state S , we know that if we applied a, we would get 0. We thus apply the input sequence associated with node a/0 , which is b and get 1. We thus have fully identified the state S in the trace, which is S4 = a/0 b/1 .

If the procedure is started from S1, it localizes in 17 steps also. From S2, S3, S4 and S5 the length of the sequences yielded by the procedure are 9, 8, 26 and 25 respectively. The non-adaptive localizer with optimal ordering (by increasing size) of W = {b, ab, aab, aaab} would yield ((b 11 ab) 11 b 11 aab) 11 (b 11 ab) 11 b 11 aaab) requiring 1885 inputs. Even when the tree is not balanced the gain is huge, because only the worst case will require the full height of the tree.

Perspectives

An adaptive localizer as presented here lowers the complexity of localizing, from an exponential in the number of sequences to an exponential in the height of the splitting tree. This paves the way for new applications of localizing, in conformance testing or inference for non-resettable machines. In particular, it is possible to consider adapting an inference algorithm [START_REF] Groz | Inferring finite state machines without reset using state identification sequences[END_REF] so that the sequences separating subsets of states are discovered instead of being given. Thus it would be possible to infer incrementally with just a bound on the number of states, and with no initial knowledge of separating sequences for a black box system.

Fig. 1 .

 1 Fig. 1. FSM M0 and a splitting tree T for it

1 3 if d = 0 then 4 return root(T ) 5 else if d = 1

 3451 procedure L(d, T ) return Node N // d is max-depth to use 2 then 6 apply I(root(T )), observe some Λ(N ) ] := L(d -1, T )

until

  Predictable(i, Nt, N 1)17 N := L(d -1, T (parent(N 1) ← N 1))

2 r := 0 // repetition factor 3 Ns 4 repeat 5 r := r + 1 6N

 203451 := empty set // set of states in last r elements of Nt Ns := Ns ∪ leaves(Nt[i -r]) // set of all leaf nodes 7 s := card(Ns) 8 until r = i or s ≤ r 9 if s > r then 10 return false 11 else // we have entered a loop, can we predict N 1? 12 while leaves(Nt[i -r -1]) ⊆ Ns and r ≤ i -1 do 13 r := r + 1 14 end 15find greatest j such that16 i -r ≤ j < i -1 and ∀m ∈ [0, r -s -1], Nt[j -m] = Nt[i -1 -m] 17 N 1 := Nt[j + 1] 18 while j > i -s do 19 j := j -1 20 if ∀m ∈ [0, r -s -1], Nt[j -m] = Nt[i -1 -m] and Nt[j + 1] = N 1 then := L(1, T (root(T ) ← a/1 )apply ab, observe 10 // we are now in S3 return a/1, ab/10 Nt[0] = a/1, ab/10 i := i + 1 = 1 Nt[1] := L(2, T ) i := 0 Nt [0] := L(1, T ) apply a, observe 1 // we are now in S4 Nt [0] = a/1 . . .After 6 iterations, we are in S4 and Nt = [ a/1 , a/0 , a/1 , a/0 , a/1 , a/0 , a/1 ] It is predictable that if we applied a, we would observe 0. Predictable(i, Nt , N 1) is true and N 1 = a/0 N := L(1, T (root(T ) ← a/0 ) apply b, observe 1 // we are now in S5 return a/0, b/1 // We have fully identified S4, and we are in S5 Nt[START_REF] Groz | Inferring finite state machines without reset using state identification sequences[END_REF] = a/0, b/1

Acknowledgments The authors acknowledge feedback from A. Petrenko.


Alexandre Petrenko
email: alexandre.petrenko@crim.ca

Florent Avellaneda
email: florent.avellaneda@crim.ca

Roland Groz
email: roland.groz@imag.fr

Catherine Oriat
email: catherine.oriat@imag.fr

From Passive to Active FSM Inference via Checking Sequence Construction

Keywords: FSM testing, machine inference, machine identification, active learning, checking experiments, checking sequences

The paper focuses on the problems of passive and active FSM inference as well as checking sequence generation. We consider the setting where an FSM cannot be reset so that its inference is constrained to a single trace either given a priori in passive inference scenario or to be constructed in active inference scenario or aiming at obtaining checking sequence for a given FSM. In each of the last two cases, the expected result is a trace representing a checking sequence for an inferred machine, if it was not given. We demonstrate that this can be achieved by a repetitive use of a procedure that infers an FSM from a given trace (identifying a minimal machine consistent with a trace) avoiding equivalent conjectures. We thus show that FSM inference and checking sequence construction can be seen as two sides of the same coin. Following an existing approach of constructing conjectures by SAT solving, we elaborate first such a procedure and then based on it the methods for obtaining checking sequence for a given FSM and inferring a machine from a black box. The novelty of our approach is that it does not use any state identification facilities. We only assume that we know initially the input set and a bound on the number of states of the machine. Experiments with a prototype implementation of the developed approach using as a backend an existing SAT solver indicate that it scales for FSMs with up to a dozen of states and requires relatively short sequences to identify the machine.

Introduction

Model-based testing from finite state models of systems, when it is only possible to interact with the system through its input/output interfaces, relies on traversing transitions of the model and being able to check that states reached after transitions in the system are consistent with those expected from the model. At the end of the test, the goal is to be able to guarantee that the system under test behaves as expected in the model. So the test must be built as a checking sequence of inputs that can uniquely identify (up to equivalence) a given model machine.

Computing a checking sequence from a finite state model dates back to the very early history of automata in computer science, starting with the work of Moore [START_REF] Moore | Gedanken experiments on sequential machines[END_REF] and many approaches have been proposed to generate checking sequences for various types of models under various assumptions for the machine w.r.t determinism, completeness, and the existence of specific sequences for a machine such as distinguishing sequences [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF], signatures [START_REF] Sabnani | A protocol test generation procedure[END_REF], state identifiers [START_REF] Petrenko | Testing from partial deterministic FSM specifications[END_REF] etc.

More recently, at the turn of the century, model-based approaches have led to an interest in inference techniques. Instead of checking whether a system behaves as specified by a model, it works the other way round: we try to build a model, called a conjecture that will predict as accurately as possible the behaviour of a system. This can be based on a corpus of given observed behaviours of the system (passive inference), or on the ability to submit test sequences (active inference). One key driver for such approaches is that experience in industrial context have shown that building and maintaining accurate and up-to-date models was complicated, and needed specific expertise. Being able to derive models automatically relieves the burden of creating and maintaining them.

Building a checking sequence can be seen as a top-down approach (from model to implementation) and inference as bottom-up approach (from implementation to conjectured model). The two are in fact closely linked: in active inference, if a sequence is built that uniquely identifies a machine, then this sequence is a checking sequence for this machine. The main difference is in the starting point: for checking sequence generation, we assume we know the (specification) machine to be identified. For inference, the machine is unknown.

In this paper, we propose an iterative approach that alternates passive inference with construction of checking experiments. Initially, an input sequence will be too short to uniquely identify a machine. But one can exhibit one of many possible conjectures that would match the observed input/output sequence (the running trace). So the idea is to build a checking experiment that will distinguish among conjectures, and which is appended to the current trace. Following this experiment, the set of potential conjectures is reduced, and the process is iterated until we get to a point where the set is reduced to a singleton, at which point the input projection of the observed trace is a checking sequence.

Interestingly, this theoretical framework had already been envisioned by J. Kella, in one of the early papers on passive inference [START_REF] Kella | Sequential machine identification[END_REF]. Let us quote the end of his introduction (our comments in brackets): "When the machine has no distinguishing sequences the reducing technique can help in minimizing the length of the checking experiment by iterative construction of the experiment. An initial sequence is applied to the machine and the resulting input-output sequence is reduced [by state merging]; the result will indicate a family of machines responding in the same way. An additional sequence which eliminates nondesired machines is then applied and another reduction is performed; by repeated application of the basic iteration the sequence will reduce uniquely to the checked machine [up to the initial state]. This method of checking experiment construction was tried for some examples but there is no proof yet to whether it is more efficient than other methods [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF] and whether it will converge in all cases."

Our approach shows that it is indeed possible to uniquely identify a non-resettable deterministic complete machine, while building a checking sequence for it, with no priori knowledge apart from a bound on the number of states, and the input set of the machine. Contrary to previous work [START_REF] Groz | Inferring finite state machines without reset using state identification sequences[END_REF], it does not require a characterization set or another assumption on sequences to distinguish states in the machine.

Section 2 will provide precise definitions for our formal framework, while Section 3 will define the inference problems and checking sequence generation in our context, i.e. from a single trace for a non-resettable machine, in relation with the state of the art. Section 4 shows how passive inference, i.e. the computation of a conjecture from a single trace can be encoded into a Boolean formula, so that a SAT solver can be used to efficiently get a conjecture. Sections 5 and 6 present our iterative approaches, showing the two sides of the coin: checking sequence generation and active inference. Section 7 presents experiments that show that the algorithms can work with middle-sized automata. Section 8 concludes.

Definitions

A Finite State Machine (FSM) M is a 5-tuple (S, s0, I, O, T), where S is a finite set of states with an initial state s0; I and O are finite non-empty disjoint sets of inputs and outputs, respectively; T is a transition relation T  S  I  O  S, (s, a, o, s)  T is a transition. When we need to refer to the machine M in a state s  S, we write M/s.

M is completely specified (complete) if for each tuple (s, a)  S  I there exists transition (s, x, o, s)  T. It is deterministic if for each (s, a)  S  I there exists at most one transition (s, a, o, s)  T, otherwise it is nondeterministic. We consider in this paper only deterministic FSMs.

An execution of M/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. M is strongly connected, if the state transition diagram of M is a strongly connected graph.

A trace of M/s is a string of input-output pairs which label an execution from s. Let Tr(s) denote the set of all traces of M/s and TrM denote the set of traces of M/s0. For trace   Tr(s), we use s-after- to denote the state M reached after the execution of , for an empty trace  s-after- = s. When s is the initial state then we write M-after- instead of M/s0-after-.

Let also out(s, ) be an output sequence produced by the input sequence   I* in M/s. For input sequence  applied in state s, we let trs() denote the trace with the input projection ; we will omit the subscript when no confusion occurs.

Given Two complete FSMs M = (S, s0, I, O, T) and M′ = (S′, s′0, I, O, T′) are called isomorphic if there exists a bijection f: S → S′ such that f(s0) = s′0 and for all a  I, o  O, and s  S, f(s-after-ao) = f(s)-after-ao. Isomorphic FSMs are equivalent, but the converse does not necessarily hold. Note that we do not require equivalent machines to be minimal.

Given a trace   (IO)* of length ||, let Pref() be the set of all prefixes of . We define a linear FSMW = (X, x0, I, D), where D is a transition relation, such that |X| = || + 1, and there exists a bijection f:

X  Pref(), such that f(x0) = , (xi, ao, xi+1)  D iff f(xi)ao = f(xi+1) for all i = 0, …, || -1, in other words, TrW = Pref(). We call it an -machine W.
While the set of traces of the -machine is Pref(), there are many FSMs which have the trace  among other traces. We restrict our attention to the class of FSMs with A state of the -machine reached after any prefix of the trace  corresponds to a unique state of the -conjecture that is reached after that prefix. Formally, there exists a mapping : X  S, such that (x) = s0-after-f(x), the state reached by C when the trace f(x)  Pref() is executed. The mapping  induces a partition C on the set X such that x and x belong to the same block of the partition C,

denoted x = C x, iff (x) = (x).
Given an -conjecture C with the partition C, let D be an -conjecture with the partition D, such that   Pref(), we say that the partition C is an expansion of the partition D, if its projection to  coincides with the partition D;

viz D = {P  X| P  C} where X = {xi  X | i  ||}.
An input sequence   I*is a checking sequence for a complete FSM M with n states if for each FSM N  ℑ(n, I, O), such that N ≅ M/s, where s  S, it holds that N ≅ M/s. The trace trs(), where  is a checking sequence, is called a checking trace of M. In this definition, we allow uncertainty in the initial state of M since it may have other states which converge with the initial state on a checking trace (an example of such an FSM can be found in Section 5).

Checking sequence is a special type of checking experiments for FSM, it is usually considered for FSM based testing when a reset operation in FSM implementations is unavailable or formidably costly to execute.

Problem Statement and Related Work

We consider the following closely related problems, passive and active FSM inference as well as checking sequence construction. Significantly, we restrict our setting to the case where a FSM may not be reset, so that the definitions we give here refer to a single trace. Actually, if a FSM can be reliably reset, the reset sequences can be included in the trace, so the definitions below can cover the general case. We state the problems using the definitions given above.

Passive inference is a classical problem whereby given a trace  we need to build an -conjecture with a minimal number of states [START_REF] Kella | Sequential machine identification[END_REF][6] [START_REF] Biermann | On the synthesis of finite-state machines from samples of their behavior[END_REF].

Active inference, aka active automata learning, is another problem addressed in the literature [START_REF] De La Higuera | Grammatical inference: learning automata and grammars[END_REF]. Restated in our FSM context, given a black box, which behaves as an unknown minimal complete strongly connected FSM with the input alphabet I and the number of states equal to n, infer the FSM, i.e. build an -conjecture equivalent to the FSM and its checking trace .

The checking sequence problem differs from active inference in assuming that the expected behavior of a black box with at most n states submitted for testing is given as a strongly connected FSM M called a specification machine (which is unknown in active inference) and we need to determine its checking trace . The relation to passive inference is direct, once  is constructed, any -conjecture must be equivalent to M.

In this section, we briefly discuss the existing approaches addressing these problems which do not rely on the existence of a reset operation.

Passive Inference from a Single Trace

Passive FSM inference problem is stated by Kella in 1971 [START_REF] Kella | Sequential machine identification[END_REF] as sequential machine identification and later as system/automaton identification problem by Gold [START_REF] Gold | Complexity of automaton identification from given data[END_REF]. The problem has been studied ever since. The problem is known to be computationally very hard, nevertheless, numerous proposals have been made, mainly on developing state merging techniques to transform an -machine into an -conjecture as small as possible, see, e.g., [START_REF] Kella | Sequential machine identification[END_REF] [27] etc. The most recent approaches are based on satisfiability (SAT) solvers [START_REF] Abel | MeMin SAT-based exact minimization of incompletely specified mealy machines[END_REF] [START_REF] Heule | Exact DFA identification using SAT solvers[END_REF].

In Section 4, we propose an approach to build an -conjecture within a bound on the number of states using a SAT solver that avoids obtaining conjectures which were already considered.

Checking Sequence Problem

The problem of checking sequence generation from an FSM has a long history starting from work of Moore [START_REF] Moore | Gedanken experiments on sequential machines[END_REF] and Hennie [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF]. Almost all existing methods require a machine be complete and minimal. Moreover, the vast majority of the proposed methods only apply to FSMs which have distinguishing sequences or distinguishing sets, see, e.g. [START_REF] Boute | Distinguishing sets for optimal state identification in checking experiments[END_REF][7] [12][22][23] [START_REF] Yannakakis | Testing finite state machines: fault detection[END_REF]. Not all FSMs possess these sequences and their construction is a non-trivial problem. Only few methods can generate checking sequence from complete and minimal FSM which has just characterization set and no other distinguishing sets, see [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF][19] [START_REF] Porto | Generation of checking sequences using identification sets[END_REF]. Moreover, they cannot be called efficient, since the size of a checking sequence generated by using characterization set grows exponentially with the length and number of sequences in characterization set [START_REF] Vasilevski | Failure diagnosis of automata[END_REF].

The problem of checking sequence generation without even checking the existence of distinguishing sequences or finding an "optimal" or any other characterization set remains open, to the best our knowledge. In Section 5 we propose an approach that does not assume any distinguishing or characterization set computation.

Active Inference without Reset

Active inference has most often been addressed in the context of learning from samples and queries [START_REF] De La Higuera | Grammatical inference: learning automata and grammars[END_REF] [START_REF] Groz | Modular system verification by inference, testing and reachability analysis[END_REF], so that the problem of dealing with a single trace has not received a lot of attention. An early attempt was proposed by [START_REF] Rivest | Inference of finite automata using homing sequences[END_REF], as an adaptation to Angluin's L* algorithm. It assumes that an external oracle can be queried to provide a counterexample (hence an input sequence to distinguish the black box and the conjecture), and starts with the knowledge of a homing sequence. More recently an approach was proposed that does not require an external oracle, but still assumes knowledge of a characterization set [START_REF] Groz | Inferring finite state machines without reset using state identification sequences[END_REF].

However, the assumptions about the existence of an external oracle, knowledge of homing or state characterizing sequences, such as distinguishing sequences and characterization sets, are not easy to justify in practice, therefore the problem of active inference of FSMs with neither reset operation nor strong assumptions about a given back box remains open. In Section 6 we propose an approach that does not require such assumptions.

Passive Inference with SAT solving

Since an -machine is itself an -conjecture, the minimization problem boils down to merging states of the -machine without introducing traces that would contradict the trace . Therefore by encoding a trace into a Boolean formula, and expressing state merging possibilities in that formula, we may use a SAT solver to determine acceptable mergers.

Problem Encoding

Here we present a procedure for encoding a trace into a Boolean formula, and at the same time express a constraint on the number of states.

Let W = (X, x0, I, D) be an -machine. To find an -conjecture with at most n states amounts to determine a partition  on the set of states X such that the number of blocks does not exceed n. This problem can be casted as a constraint satisfaction problem (CSP) [START_REF] Carbonnel | Tractability in constraint satisfaction problems: a survey[END_REF]. Let X be {x0, …, x||}, so each integer variable represents a state of the machine. Since the -machine is deterministic, the state variables satisfy the following constraint:

xi 1) is satisfied defines a mapping : X  S, where S is the set of states of an -conjecture, i.e., the mapping  defines a partition of X into n blocks.

These formulas can be translated to SAT using unary coding for each integer variable x  X, such that x is represented by n Boolean variables vx,0, …, vx,n-1. For each x  X, we have the clause: vx,0 …  vx,n-1

(2) These clauses mean that each state of the -machine W should be in at least one block.

For each state x  X and all i, j  {0, …, n -1} such that i  j, we have the clauses:  vx,i   vx,j (3) The clauses mean that each state of the -machine W should be in at most one block. Since a sought-after -conjecture must be deterministic, the formula ( 1) is encoded into the following clauses. First, distinguishable states of W should be in different blocks, so for every x, y  X such that x ≇ y and all i  {0, …, n -1} vx,i  vy,i (4) Second, states of W equivalent w.r.t. to some input if placed in the same block must have their successors also in one block. Hence for all xi, xj X such that out(xi, a) = out(xj, a) = o and all i, j  {0, …, n -1} we have a formula which can directly be translated into clauses (vx,i  vx,i) ⇒ (v(x-after-ao),i ⇒ v(x-after-ao),i) [START_REF] De La Higuera | Grammatical inference: learning automata and grammars[END_REF] To simplify learning that x = y for some x, y X we further rewrite the clauses (4) and ( 5) using auxiliary variables ex,y modeling the fact that x = y. For every x, y X such that x ≇ y we have ex,y (6) For all x, y X such that out(x, a) = out(x, a) = o, we have ex,y ⇒ ex-after-ao,y-after-ao [START_REF] Gonenc | A method for the design of fault detection experiments[END_REF] The relation between auxiliary state variables is expressed in the following clauses. For every x, y X and all i  {0, …, n -1} ex,y  vx,i ⇒ vy,i (8) ex,y  vx,i ⇒ vy,i (9) The resulting Boolean formula is the conjunction of clauses (2), (3), ( 6), ( 7), ( 8) and (9). To check its satisfiability one can use any of the existing solvers. If a solution exists then we have an -conjecture with n or fewer states. The latter is obtained from the determined partition on X. In the context of passive inference, we are usually interested in finding an -conjecture as small as possible. This requires several trials with varying values of n.

Passive Inference of Different (new) Conjectures

In the context of active inference as well as checking sequence construction we aim at obtaining a single -conjecture while avoiding constructing isomorphic conjectures.

A key building block will be provided by the following procedure to infer a conjecture that differs from already considered conjectures. We identify isomorphic conjectures by their common partition, hence we add as a constraint that we look for an -conjecture that does not expand a set of "forbidden" partitions. If such -conjectures are found they will be used in Sections 5 and 6 to augment the trace  by adding suffixes that eliminate distinguishable conjectures until only one remains.

Algorithm 1. Infer_conjecture(, n, )

Input: A trace , an integer n, and a set of partitions  Output: An -conjecture with at most n states such that its partition does not expand any partition in , or False.

1. formula = conjunction of the clauses (2), ( 3), ( 6), ( 7), ( 8) and ( 9) 2. for all    do 3.

clause = False 4.

for all x, ysuch that x = y do 5.

clause = clause  ex,y 6. end for 7.

formula = formula  clause 8. end for 9. return call-solver(formula)

Checking Sequence Construction

The idea of the proposed method for checking sequence (trace) generation is to find an FSM that reacts as the given specification FSM to a current input sequence using passive inference and eliminate it by extending the sequence with a suffix distinguishing the two machines or forbidding the passive inference from further regeneration if they cannot be distinguished any further. This process iterates until no more conjectures distinguishable from the given FSM can be found. The procedure is implemented in Algorithm 2. Note that the Boolean formula used by the SAT solver is built incrementally by saving a current formula and adding only new clauses each time a trace  or a set of partitions  is augmented. Theorem 1. Given an FSM M with n states, Algorithm 2 returns a checking trace . Sketch of the proof. When Algorithm 2 terminates the resulting trace  is indeed a checking one, since by the post-condition of Infer_conjecture no conjecture exists that is distinguishable from the given FSM M, after having executed . Note that all complete conjectures equivalent to M are excluded because as soon as one if found (including possibly M itself), according to the Lemma, its partition is added to . Algorithm 2 always terminates, because the number of all possible conjectures with the fixed input alphabet within a given bound on the number of states n is finite.

Algorithm 2. Generating checking trace

Example. Consider the FSM in Fig. 1, it has no distinguishing sequence, its characterization set is {a, b}.

Fig.1. The FSM M

This example is used in [START_REF] Porto | Generation of checking sequences using identification sets[END_REF], where a method for checking sequence generation from a minimal FSM without distinguishing sequence is proposed. Using this example the authors of [START_REF] Porto | Generation of checking sequences using identification sets[END_REF] compare their method with those of [10][19] and report that the length of checking sequence obtained by their method is 120, while that of [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF] is 171 and 248 of [START_REF] Rezaki | Construction of checking sequences based on characterization sets[END_REF].

0 1 2 3 b/0 a/0 b/1 a/0 b/0 a/1
Algorithm 1 implemented in a prototype tool presented in Section 6 returns the checking sequence  = a0a1a0a1b0b1b0a0b0b1a0a1b0a0a1 of length 15. Fig. 2 shows intermediate complete -conjectures obtained executing Algorithm 1. Notice that the last but one conjecture is actually the FSM M, though, the same trace is also accepted by another conjecture, which is eliminated using the suffix b0a0a1. Note that the algorithm does not require the FSM to be minimal, moreover, it can be adapted to accept even a partial FSM. We are not aware of any method for checking sequence construction for FSMs which are partially defined and have compatible states, i.e., machines without characterization set. The only existing method which deals with such machines is [START_REF] Petrenko | Testing from partial deterministic FSM specifications[END_REF], but it relies on the usage of the reset operation, as opposed to the approach proposed here.

Active Inference Approach

The iterative approach of Algorithm 2, which relied on computing a checking experiment for an -conjecture that was consistent with the current prefix trace can be adapted to active inference. The trick is to find a checking experiment not between the reference 0 1 2

a/0 b/1 b/0 b/0 a/0 a/1 0 1 2 3 a/1 a/0 b/0 b/0 b/1 a/0  = a0a1a0a1b0b1b0a0b0  = a0a1a0a1b0b1b0a0b0b1  = a0a1a0a1b0b1b0a0b0b1a0 0 1 2 3 b/0 a/0 b/1 a/0 b/0 a/1 0 1 2 a/1 a/0 b/0 a/0 b/1 b/0  = a0a1a0a1b0b1b0a0b0b1a0a1b0a0a1 0 1 2 a/0 b/1 b/0 a/0 a/1 b/0  = a0a1a0a1b0b1b0a0b0b1a0a1
FSM M and the -conjecture, but between two possible -conjectures and retain the one that is consistent with the observations on the black box.

Given a black box BB, which behaves as an unknown minimal complete strongly connected FSM with the input alphabet I and a number of states equal to n, Algorithm 3 infers the FSM and constructs its checking trace. := tr(a), where tr(a) is the trace obtained by applying a to BB 10:

if TrC then 11:

C := Infer_conjecture(, n, ) 12:
end if 13: end if 14: end while 15: return C and  Theorem 2. If a black box behaves as a minimal complete strongly connected FSM with the input alphabet I and the number of states equal to n, Algorithm 3 infers it and constructs a checking sequence and trace for it.

Sketch of the proof. Algorithm 3 follows the steps of Algorithm 2, just replacing the FSM M by a current conjecture. This does not influence its termination since it only occurs when no more distinguishable conjecture can be found. And at some point, because the black box behaves as a FSM with n states, it will be returned by Infer_conjecture, so that the remaining conjecture is equivalent to the FSM of the black box initialized in some state. The resulting trace accepted by that state is a checking one, as in Theorem 1.

Example. Consider that the FSM M in Fig. 1 is a BB. Six intermediate complete conjectures shown in Fig. 3 are obtained executing Algorithm 3. The last two conjectures both accept  = a0a1a0b0b1b0b1a0a1b0a0a1a0a1. Both end up in state 2 from which they cannot be distinguished. The algorithm returns  as a checking trace and the last but one conjecture which is isomorphic to FSM M/2. The last conjecture is isomorphic to FSM M/0. Indeed this trace is accepted by M in two states, 0 and 2. The expected complexity of the proposed approach could be estimated by viewing it as a mutation-based technique which kills mutants. In our approach at each iteration only a mutant surviving a current trace can be generated and then killed, drastically reducing the complexity of mutation-based techniques. A naive worst-case estimation based on number of (potential) mutants would be grossly overestimated. This explains why we provide in the next section experimental results on the observed complexity with random machines.

Experiments

The prototype was developed on C++ depending only on a SAT Solver Cryptominisat [START_REF] Soos | CryptoMiniSata SAT solver for cryptographic problems[END_REF], as a backend. All the experiments were performed on a virtual machine (VirtualBox) with 8 GiB of RAM and one CPU used. The computer has the processor 7-3770 and 16 GiB of RAM.

Table 1 presents experimental results on randomly generated FSMs. The numbers of inputs as well as outputs are fixed to two, while the number of state is varied. For each state number, 101 complete strongly connected machines are generated; they are not necessarily minimal, since the approach does not require any state distinguishability. Each generated machine playing role of a specification FSM is used to construct checking sequence, and acting as a black box system is used for inference. Median values are collected for the length of resulting checking sequences ||, the number of times the solver is called (#solver), and execution time in seconds. The prototype scales for up to a dozen of states. This matches the state-of-the-art, see, e.g., [START_REF] Oliveira | Efficient algorithms for the inference of minimum size dfas[END_REF]. To assess the performance of the prototype to various numbers of inputs and outputs, another series of experiments reported in Table 2 were performed for machines with five states. Our experiments by varying their numbers separately show, unsurprisingly, that increasing number of inputs or outputs have opposite effects on the effectiveness, the more inputs the more complex the solutions (the search space is larger) but the more outputs the easier the solutions (more outputs increase distinguishability).

n
In addition, we performed another series of experiments using randomly generated lock machines (Table 3). A lock FSM (aka Moore lock, defined by him) with n states has a unique "unlocking" input sequence of length n which executes the "remotest" transition, the transitions not covered by this sequence all lead to the initial state resetting the lock. We consider lock machines as ultimate test for active inference and checking sequence generation methods. As before for each number of states we generate 101 random locks with two inputs and two outputs and collect the same parameters as above. Clearly, for a fixed number of states, locks differ only in labelling of unlocking sequences, which effects the performance of the prototype, since it chooses inputs completing and distinguishing conjectures following the lexicographical order. It is interesting to notice that active inference and checking sequence construction have comparable lengths of the resulting input sequences. After all, in both cases a checking sequence for the same machine is generated.

#inputs

We observe that the length of resulting sequences grows polynomially, the number of times the solver is called linearly and time exponentially with the number of states.

Conclusions

We have presented a method that can infer a model of a non-resettable black box FSM for which we only know an upper bound n on the number of states. It produces the model along with the input sequence that was used for inferring it. The algorithm terminates on a final model that is equivalent to the black-box FSM up to initialization, and since it identifies a unique machine such that the input sequence is a checking sequence for this FSM.

The main benefit of this approach is that it only requires a bound on the number of states, no other assumption is needed, and the system does not have to be reset. This implies that it may have a wide spectrum of applications. The performance of active inference methods is usually assessed through the number of interactions with a system that are needed to infer it. Experiments have shown that the length of the input sequence implied by our approach is quite good. Another issue comes from the internal computations needed by the inference algorithm to build the model of the system. The method relies on a SAT solver to propose conjecture FSMs that are consistent with an observed trace. Unfortunately, this induces an exponential growth in the number of states, and this has been the limiting factor in our experiments. However, being able to infer state machines of up to a dozen states is in itself interesting for a large range of applications (many systems have relatively small state-space for the control part of their computations).

The approach seems promising, and can be improved in several directions. First, we have encoded the constraints for passive inference in a straightforward way, which puts a high burden on the constraint solver. It should be possible to encode the problem with more elements from the trace and FSM-structure to help the solver, with some guidance. Another direction we are investigating is to extract more information from previous conjectures and observations so as to reduce the number of calls to the solver to a minimum. In many cases, the calls to the solver can be avoided because it is possible to derive further checking experiments from the structure of the past conjecture(s). Instead of calling the solver to identify a new conjecture, it could be possible to refine the current conjecture.

  at most n states and alphabets I and O, denoted ℑ(n, I, O). An FSM C = (S, s0, I, O, T), C  ℑ(n, I, O) is called an -conjecture, if   TrC. Let ℑ(n, I, O) be the set of all conjectures in the set ℑ(n, I, O). Clearly, the -machine is also an -conjecture, if || < n. The states of the -machine W = (X, x0, I, D) and an -conjecture C = (S, s0, I, O, T), C  ℑ(n, I, O) are closely related to each other.

  , xj  X : if xi ≇ xj then xi  xj and if a  I s.t. out(xi, a) = out(xj, a) = o then xi = xj ⇒ xi-after-ao = xj-after-ao (1) If the number of states in an -conjecture to be constructed should be at most n then each state variable xi  {0, …, n -1}. Then an assignment of values to variables in {x0, …, x||} such that the formula (

Fig. 2 .

 2 Fig. 2. The -conjectures generated by Algorithm 1 along with their versions of ; suffixes in bold show how  grows.

Algorithm 3 .

 3 Inferring BB and determining its checking trace Input A black box BB, input set I and integer n Output A minimal complete -conjecture with n states and a checking trace  1:  := 2:  :=  3: C := Infer_conjecture(, n, ) 4: while an -conjecture D is returned by Infer_conjecture(, n, ) do 5: if D/D-after- C/C-after- is complete in the input set I then 6: :=   {D} 7: else 8: Determine an input sequence a such that  is a shortest transfer sequence from the state C-after- to a state with the undefined input a in D/D-after- C/Cafter- 9:

Fig. 3 .

 3 Fig. 3. The -conjectures generated by Algorithm 3 along with their versions of ; suffixes in bold show how  grows.

  an input sequence , states s, s  S are equivalent w.r.t. , if out(s, ) =

	). States s and s are equivalent if they are equivalent w.r.t. all input sequences, thus
	Tr(s) = Tr(s), denoted s ≅ s. The equivalence and distinguishability relations between
	FSMs is similarly defined. Two FSMs are equivalent if their initial states are equivalent.
	A complete FSM is minimal, if it has no equivalent states.
	Given two FSMs M = (S, s0, I, O, T) and M′ = (S′, s′0, I, O, T′), their product M  M′
	is an FSM (P, p0, I, O, H), where p0 = (s0, s'0) is such that P and H are the smallest sets
	satisfying the following rule: If (s, s')  P, (s, x, o, t)  T, (s', x, o', t')  T', and o = o',
	then (t, t')  P and ((s, s'), x, o, (t, t'))  H.
	Lemma. If M and M′ are complete machines then they are equivalent iff the product
	M  M′ is complete in the input set I.
	out(s, ), denoted s ≅ sthey are distinguishable by , if out(s, )  out(s, ), de-
	noted s ≇ s or simply s ≇ s. A distinguishing sequence of M is an input sequence 
	for which the output sequence produced by M in response to  identifies the state of M:
	for all s, s  S, out(s, )  out(s, ). A characterization set of M is a set input sequences
	such that every s, s  S, there exists a sequence  in the set such that out(s, )  out(s,

  Algorithm 2 calls Infer_conjecture(, n, ), which in turn calls a SAT solver constraining it to avoid solutions of already considered conjectures.

	1.  :=
	2.  := 
	3. while an -conjecture C is returned by Infer_conjecture(, n, ) do
	4.	if C-after- M-after- is complete then
	5. 		:=   {C}
	6.	else
			Determine an input sequence a such that  is a shortest transfer se-
			quence from the state C-after- to a state with the undefined input a
			in C-after- M-after-
	8. 		:= tr(a), where tr(a) is the trace of M-after-
	9.	end if
	10. end while
	11. return 
	Input: A complete strongly-connected FSM M with n states
	Output: A checking trace 

Table 1 .

 1 Experimental results with randomly generated FSMs with two inputs and outputs.

				RANDOM FSMs
			Checking			Inferring
		||	#solver	time	||	#solver	time
	1	2	3	0.01	2	3	0.01
	2	7	8	0.01	7	9	0.01
	3	17	14	0.01	18	18	0.01
	4	26	20	0.01	30	24	0.01
	5	37	26	0.01	43	32	0.02
	6	47	32	0.03	57	39	0.05
	7	63	39	0.07	69	45	0.13
	8	76	44	0.17	83	54	0.32
	9	100	53	0.59	107	72	2.4
	10	118	58	1.7	119	70	9.0
	11 146	69	18.5	146	83	161

Table 2 .

 2 Experimental results with randomly generated arbitrary FSMs with five states.

					RANDOM FSMs
	=			Checking		Inferring
	#outputs		||	#solver	time	||	#solver	time
	2		37	26	0.01	43		32	0.02
	3		51	40	0.03	57		47	0.05
	4		68	53	0.04	70		58	0.09
	5		74	62	0.05	81		71	0.12
	6		88	73	0.07	95		85	0.2
	7		101	83	0.09	109	99	0.3
	8		113	95	0.12	121	111	0.38
	9		121	102	0.12	127	122	0.5
	10		138	114	0.18	145	136	0.72
	20		257	212	0.63	276	261	3.2
	30		377	312	1.3	425	391	10
	40		525	412	2.5	517	571	22
				RANDOM LOCKs
	n		Checking			Inferring
		||	#solver	time	||	#solver	time
	1	2	3		0.01	2	3	0.01
	2	7	8		0.01	7	7	0.01
	3	22	16		0.01	23	22	0.01
	4	57	28		0.04	58	61	0.05
	5 110	40		0.41	127	164	0.79
	6 255	58		7.8	269	514	21
	7 488	456	870	456	2202	970

Table 3 .

 3 Experimental results with randomly generated lock FSMs.

Acknowledgements. This work was partially supported by MESI (Ministère de l'Économie, Science et Innovation) of Gouvernement du Québec and NSERC of Canada.