Roland Groz
email: roland.groz@imag.fr

Adenilso Simao
email: adenilso@icmc.usp.br

Alexandre Petrenko
email: alexandre.petrenko@crim.ca

Catherine Oriat
email: catherine.oriat@imag.fr

Inferring Finite State Machines Without Reset Using State Identification Sequences

Keywords: Finite State Machines, model inference, testing

Identifying the (finite state) control structure of a black box system from the traces observed in finite interaction is of great interest for many model-based activities, such as model-based testing or model-driven engineering. There are several inference methods, but all those methods assume that the system can be reset whenever necessary. In this paper, we address the issue of inferring a finite state machine (FSM) that cannot be reset; we propose a method, inspired by FSM-based testing generation methods. We assume classical testing hypotheses, namely that we are given a bound n on the number of states and a set W of characterizing sequences to distinguish states. To the best of our knowledge, this is the first model inference method that does not require resetting the system, and does not require an external oracle to decide on equivalence. The length of the test sequence is polynomial in n and the exponent depends on the cardinal |W| of the characterization set.

Introduction

For model-driven software engineering, model-based testing including, it is important to rely on models of the software artefacts. It is also essential that the models are upto-date. In many contexts, however, such models are not available. In the last decade, interest has risen on methods to retrieve models from software artefacts, see, e.g., [START_REF] Aarts | Generating Models of Infinite-State Communication Protocols using Regular Inference with Abstraction[END_REF] [2] [4] [START_REF] Irfan | Angluin Style Finite State Machine Inference with Nonoptimal Counterexamples[END_REF] [10] [12] [START_REF] Steffen | Introduction to Active Automata Learning from a Practical Perspective[END_REF]. Depending on the context, goal and assumptions, various types of techniques have been considered for specification mining, reengineering or model inference. When source code is available, automated analysis of its structure can yield adequate models [START_REF] Corbett | Bandera: extracting finite-state models from Java source code[END_REF] [START_REF] Mihancea | jModex: Model Extraction for Verifying Security Properties of Web Applications[END_REF].

Various algorithms have been proposed for inference of finite state machines. Such methods have been used to retrieve finite state behavioural models of black box components by testing them [START_REF] Shahbaz | Inferring Mealy Machines[END_REF] [START_REF] Steffen | Introduction to Active Automata Learning from a Practical Perspective[END_REF]. Typically, such components could be accessed over a network, so that we do not even assume that the executable can be scrutinized: the system can only be observed at its interfaces [START_REF] Aarts | Generating Models of Infinite-State Communication Protocols using Regular Inference with Abstraction[END_REF]. This corresponds to a typical black box testing scenario, where the tester would send inputs to a system and observe its outputs. This scenario arises in many practical situations. For instance, a component has to be treated as a black box, when its internals cannot be available due to intellectual property constraints.

We assume that the System Under Test (SUT) can be modelled, at some level of abstraction on its inputs and outputs, as a Finite State Machine (FSM). FSM-based testing theory has shown that an FSM can be identified, i.e., the SUT can be tested to be proven equivalent to it, with the help of state identifying (distinguishing) sequences, constituting, e.g., a characterization set (W-set) of input sequences.

Existing inference algorithms assume that the black box can be reliably reset to its initial state. This makes the inference task somehow easier, because it is possible to start each new experiment from a known state, and explore progressively the neighbouring states. But there are cases where a black box cannot be reset, or where it is unsure that we can rely on it being restored to the same initial state. There are also cases where restarting the system completely might be very costly requiring a lot of time to reset the whole configuration (e.g., rebooting a machine, with possibly many software components to configure and reinitialize). Actually, our research was triggered by a case study from the SPaCIoS European project where we had to infer a software provided (as is common now) as a virtual machine. Although an i/o interaction in HTTP with it over the local network would require less than a millisecond, resetting the application would need more than a minute, around 10 5 more than an i/o.

In this paper, we propose an algorithm that can infer a black-box implementation without resetting it. This problem has similarities with classical testing methods, in particular the DS-method [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF] and the W-method [START_REF] Vasilevskii | Failure Diagnosis of Automata[END_REF]. In classical testing methods, we are provided with a characterization set, and we derive a checking sequence or experiment that identifies a black box. The key difference is that classical testing methods start from a known specification machine, and just check whether the black box is equivalent (or conformant) to this specification. Therefore, those methods heavily rely on transfer sequences that make it possible to test a new state through a path known to transfer to the right state in the specification. In our context, since no specification is available, we cannot rely on known transfer sequences. Although the absence of reset had already been addressed by Hennie [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF] and others in the case of a single distinguishing sequence, the task is made much harder in our context since we cannot return to a known state to compare the responses to a state of the specification. Moreover, we consider the case where the black box may not have a distinguishing sequence. This problem has been investigated in [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF] [8] [START_REF] Porto | Generation of Checking Sequences Using Identification Sets[END_REF] [START_REF] Rezaki | Construction of checking sequences based on characterization sets[END_REF], where a characterization set is used. It turns out that generating a checking sequence (without reset) from a known specification FSM with a characterization set is very costly, due to the fact that the sequences of this set have to be applied a number of times which is proportional to some exponential on the number of states in the specification [START_REF] Rezaki | Construction of checking sequences based on characterization sets[END_REF]. Recent work [START_REF] Jourdan | Reduced checking sequences using unreliable reset[END_REF] [13] has reduced the effort by some constant factor, which is a practical improvement; nonetheless, the complexity remains exponential.

As with other identification problems in FSM based testing, we rely on assumptions on the black box. First, we assume that an upper bound n on the number of states of the black box is known. Second, we are provided with a set W of input sequences that characterize the different states of the black box: each state produces a different set of output responses to these input sequences. Such a set could be derived from a previous version of the software or from domain-specific knowledge.

Rivest and Schapire [START_REF] Rivest | Inference of finite automata using homing sequences[END_REF] pioneered the inference of automata without reset, but their method was based on Angluin's L * algorithm [START_REF] Angluin | Learning Regular Sets from Queries and Counterexamples[END_REF] which assumes that an oracle can answer equivalence queries. In a typical software testing context, such an oracle cannot be provided. Our method does not require any equivalence query, and there is no oracle apart from the black box. In order to guarantee equivalence, we just assume we know an upper bound on the number of states, which is a much weaker assumption. Identifying states by their i/o responses to sequences of W is somehow similar to the set of suffixes in L * although we do not need suffix-closure contrary to L * .

Our method relies on a localizer, a procedure that can reliably bring the black box to the same state all over again to make sure that responses to all sequences from the W-set are observed from a single state. Therefore, it is possible to extend progressively the knowledge of the transitions starting from that state, while being sure that we actually come back to a known (previously learnt) state. This procedure is inspired by the construction of locating sequence used in [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF] [START_REF] Rezaki | Construction of checking sequences based on characterization sets[END_REF]. The algorithm uses the localizer to start from a known state, which becomes the first learnt state. Thus, it does not require the black box to be initially in a particular state. It then tries to characterize progressively the tail state reached after the application of the localizer by repeatedly applying the sequences from W. By doing so, it will often end up in unknown states, therefore the algorithm alternates between applications of sequences from W to get more knowledge and applications of the localizer to restart from some previously learnt state. The algorithm identifies a correct model in O(p(f + p) 2 p n p+2 ) inputs, where n is the number of states of the machine, f is the size of the input set and p is the size of the W-set. Hence, the length of the identification sequence is polynomial in the number of states, although the exponent depends on the number of characterizing sequences.

The paper is organized as follows. Section 2 provides definitions and notations for our method. Section 3 describes the inference procedure, while Section 4 is dedicated to the localizer subroutine. Section 5 illustrates the algorithm on a small example. Proofs of termination and correctness, as well as an upper bound on complexity are in Section 6. Section 7 discusses assumptions and Section 8 concludes.

Definitions

Basic definitions

A Finite State Machine is a complete deterministic Mealy machine. Formally, a Finite State Machine (FSM) M is a 6-tuple (S, s 0 , I, O, δ, λ), where

• S is a finite set of states with the initial state s 0 , • I is a finite set of inputs, and O is a finite set of outputs,

• δ : S × I → S is a transition function, and

• λ : S × I → O is an output function.
δ and λ are actually mappings, i.e., dom(δ) = dom(λ) = S × I since we only consider complete machines. As M is deterministic, a tuple (s, x) ∈ S × I uniquely determines a transition of M. For simplicity we use (s, x) to denote the transition, thus omitting its output and final state. We extend the transition and output functions from input symbols to input sequences, including the empty sequence ε, as usual: δ(s, ε) = s and λ(s, ε) = ε, for s ∈ S; for αx ∈ I + , δ(s, αx) = δ(δ(s, α), x) and λ(s, αx) = λ(s, α)λ( δ(s, α), x). An FSM M is said to be strongly connected, if for each pair of states s, s' ∈ S, there exists an input sequence α ∈ I * , such that δ(s, α) = s'; α is called a transfer sequence.

Two states s, sʹ′ ∈ S are distinguishable, if there exists γ ∈ I * , such that λ(s, γ) ≠ λ(sʹ′, γ). We say that γ distinguishes s and sʹ′. Given a set H ⊆ I * , states s and sʹ′ are Hequivalent, if λ(s, γ) = λ(sʹ′, γ) for all γ ∈ H. Otherwise, i.e., if there exists γ ∈ H such that λ(s, γ) ≠ λ(sʹ′, γ), the states are H-distinguishable. We define H-distinguishability and H-equivalence of machines as a corresponding relation between their initial states. An FSM M is minimal, if all states are pairwise distinguishable. In this paper, the machines are assumed to be minimal and strongly connected. A set of inputs W is a characterization set for an FSM M if each pair of states is W-distinguishable.

A sequence of input/output pairs α ∈ (IO)* is a trace. Given traces α, β, and ω, such that ω = αβ, we write ω \ β, when we need to refer to the result of deleting the suffix β from the trace ω, resulting in trace α. The notation α ≤ ω is used to refer to a prefix α of the trace ω; ω↓A, where A ⊆ I ∪ O, denotes the projection of ω to A, obtained by removing symbols that are not in A from the trace ω. Formally, ε↓A = ε; if x ∈ A, then (αx)↓A = (α↓A)x; if x ∉ A, then (αx)↓A = (α↓A).

Given a machine M = (S, s 0 , I, O, δ, λ) with a state s i and an input sequence α ∈ I * , we use tr i (α) to denote the trace from state s i such that tr i (α)↓I = α and tr i (α)↓O = λ( s i , α). Given a characterization set W, rather than naming or numbering states (such as "s i "), we may refer to a state by its state characterization Tr i (W) = {tr i (w) | w ∈ W}. A state characterization Tr i can be seen as a mapping q i from W to (IO)* such that q i (w) = tr i (w). The set of all mappings Q = {q 1 , q 2 , …, q n } corresponds to the set of states of the machine. Namely, for q ∈ Q and s ∈ S, we write q ↔ s if ∀w ∈ W, q(w)↓O = λ(s, w). Inferring an unknown FSM with the same characterization set, each mapping q ∈ Q can then be considered as its state. In the sequel, we use B (instead of the general M) to refer to a black-box machine, P (instead of S) to refer to its states, whereas the inferred model (also called "conjecture", in line with L * ) will have states denoted by Q.

Definitions for the inference method

Let B = (P, p 0 , I, O, δ, λ) denote an FSM modelling a given black-box (BB) with the characterization set W. As the BB cannot be reset, it is possible to observe only a single trace from it. We introduce the notion of labelling function C: (IO)* →Q ∪ {⊥}, which maps each prefix of an observed trace to a state q of Q, if it can be in-ferred that the machine B will be in state p such that q ↔ p after the observed trace; otherwise C maps the prefix to an unknown state, denoted ⊥.

Let ω be an observed trace. A labelling C is deterministic for ω if the following property holds:

For α, α' ∈ (IO)*, such that α ≤ ω, and α' ≤ ω, if C(α) = C(α') ≠ ⊥, then for any β, β' ∈ (IO)*, such that αβ ≤ ω, α'β' ≤ ω and β↓I = β'↓I, we have β = β' and C(αβ) = C(α'β').
Obviously, a labelling should be deterministic. It should also be consistent with the state characterizations, i.e., the following property should also hold:

For all α, γ ∈ (IO)* such that αγ ≤ ω, if C(α) = q ≠ ⊥ and γ↓I = w ∈ W, then q(w) = γ.
We capture the notion of known (or inferred) state by stating that a labelling C should be revealing. Let B = (P, p 0 , I, O, δ, λ), a labelling C is revealing w.r.t. B if, and only if ∀α ∈ (IO)* (∃p ∈ P s.t. ∀p' ∈ P (δ(p', α↓I)) = p) ⇒ ∃q s.t. C(α) = q and q ↔ p. In other words, this property forces C to be defined on any trace α that is "homing" [START_REF] Lee | Principles and Methods of Testing Finite State Machines -a Survey[END_REF], i.e., which leads unambiguously to a single state with a known state characterization in the FSM B, irrespective of the start state.

The labelling function and state characterizations are the main components of the proposed method. To ease the presentation and simplify the algorithm, we also introduce several auxiliary notations and definitions, derived from the labelling function.

A trace is verified if it is a subtrace of the observed trace ω and its start and end states are known (labelled by C). Each verified trace is the result of execution of several transitions between the known states of the FSM B. We define a set of tuples containing a verified trace together with its start and end states

V ⊆ Q × (IO)* × Q. Formally, V = {(q, α, q') | ∃σα ≤ ω, C(σ) = q, C(σα) = q'}.
Moreover, since we assume that C is deterministic, for all (q, α, q') ∈ V, and all χ ≤ ω, such that C(χ) = q, we have C(χα) = q'.

We will also use a subset of it to refer to single transitions, called verified transitions, and not to their sequences. Let T ⊆ V, T = {(q, xo, q') | x ∈ I, o ∈ O and ∃σxo ≤ ω, C(σ) = q, C(σxo) = q'} be the set of verified transitions. We will use as well the term of input verified in state when we do not need to refer to the end state of a verified transition. Thus R = {(q, x)

∈ Q × I | ∃o ∈ O, q' ∈ Q, (q, xo, q') ∈ T} is the set of inputs verified in corresponding states.
Moreover, since we will discover new states as the observed trace grows, we will have a set of known states associated with a current trace ω. Q C denotes a set of states discovered by ω such that q ∈ Q C iff C(α) = q, for some α ≤ ω.

We shall be able to derive from ω a complete conjecture, i.e., the FSM B, when for all q ∈ Q C , for all x ∈ I, (q, x) ∈ R.

We further assume that the set W is an ordered set of p sequences and use tr(w p ) to denote a subtrace produced by the BB when the last sequence of W viz. w p is applied.

Finally, K ⊆ Q × (IO) + × (IO)* is used to keep track of the applications of w ∈ W in a state q followed by either a transition or a trace of a sequence from W. (q, α, γ) ∈ K, if there exists a trace β, such that βαγ ≤ ω, C(β) = q , α↓I ∈ I ∪ W and γ↓I ∈ W.

Inference procedure

A localizer procedure L(ω, W) is used to ensure that we continue learning transitions from states visited before. The localizer procedure, given a current trace ω, produces an updated trace ω', a set of traces Tr(W), and the last appended trace tr(w p ) to label the state which has produced it and is thus identified with Tr(W). Recall that a state is defined by its answers to sequences from W, i.e., by Tr(W). At the end of the localizer, we know the BB is in state δ(Tr(W), w p ), and the state reached after ω\tr(w p ) can be labelled as Tr(W).

Before defining the localizer, we present the main algorithm that calls it.

Inference procedure

Initialize:

K = R = V = ∅ (ω, q 0 , tr(w p )) := L(ε, W) % Home into (or through) a known state C(ω \ tr(w p )) := q 0 Q C := {q 0 } while ∃q' ∈ Q C and x' ∈ I, such that (q', x') ∉ R do if C(ω) = q ≠ ⊥, then % If current state is known % move to unverified transition Find a shortest α = α 1 α 2 …α k , s.t. for all i (q i , α i , q i+1 ) ∈ V, q 1 = q, and x ∈ I s.t. (q k+1 , x) ∉ R Apply α↓I, observe α ω := ωα χ := ω Apply x,
χ := ω \ γ σ := γ end if q := C(χ)
% here ω is unknown Choose w ∈ W, such that there is no tr(w) s.t. (q, σ, tr(w)) ∈ K Apply w, observe tr(w) % improve characterization of (q, σ) ω := ωtr(w)

K := K ∪ {(q, σ, tr(w))} if {w ∈ W | (q, σ, tr(w)) ∈ K} = W, then % full characterization reached C(χσ) := {tr(w) | w ∈ W and (q, σ, tr(w)) ∈ K} Q C := Q C ∪ {C(χσ)} Update V, R, K and C end if if C(ω) = ⊥ then % move to an identified state (ω, q', tr(w p )) := L(ω, W) C(ω\tr(w p )) := q' Q C := Q C ∪ {q'} Update V, R, K and C end if end while Build the conjecture from Q C and T.
The sets K, V (hence T) and R should be updated to reflect the changes in C. The update is done by applying the following rules as long as possible (fix point iterations with monotonic increase of the sets):

Rule

1: If C(β) = q, C(βα) = q', βα ≤ ω, then (q, α, q') ∈ V. Rule 2: If C(β) = q, βα ≤ ω and (q, α, q') ∈ V then C(βα) = q'. Rule 3: If (q, x, q') ∈ V, for x ∈ I, then (q, x) ∈ R. Rule 4: If C(β) = q, βαγ ≤ ω, α↓I ∈ I ∪ W, γ↓I ∈ W, then (q, α, γ) ∈ K. Rule 5: If ∃α s.t. {w ∈ W | (q, α, tr(w)) ∈ K} = W then ∀βα ≤ ω s.t. C(β) = q, we have C(βα) = {γ | (q, α, γ) ∈ K}.
Notice that although in this definition of updates we derive V and K sets to be consistent with their definitions, we do not need to add all elements to them. Typically, V is transitively closed, but we only need a transitive reduction of it. If (q, α, q') ∈ V and (q', β, q'') ∈ V then in the implementation of the procedure we would not store (q, αβ, q'') in V because we use V to find a shortest concatenation of sequences that would themselves be in V or to verify transitions (sequences of length 1).

4

Localizer procedure

In our inference procedure, the main use of the localizer procedure is to ensure that when the BB is in an unknown state q, we can restart a test from a state q' of the BB for which we can be certain that we know all its traces for all sequences from the Wset, and thus we can identify state q' of the BB. Actually, we present a generalized procedure that can work with any set of sequences Z, where Z may not be a fully characterizing set, i.e., there could be non-equivalent states in the BB that are Zequivalent. The localizer procedure will be defined recursively with increasing subsets Z of W.

For the design of this localizer procedure, we extend an idea that had already been investigated by Hennie [START_REF] Hennie | Fault-Detecting Experiments for Sequential Circuits[END_REF]. The key idea is that since the number of states is finite and bounded by n, by repeatedly applying a given input sequence α we can observe at most n different output sequences. This implies that in the state reached applying n times α the BB must have reached a cycle, coming to one of the states visited after some α i . But we do not know which one because different states could still have the same output response to α. The length of the cycle is itself bounded by n. As the proof will show, it is enough to repeat α another n -1 times (so 2n -1 in total) in the worst case to identify the cycle and be able to know what would be the response from the BB to the 2n-th application and all subsequent applications of α.

This means that after 2n -1 applications of α, we are in a state p and we can apply another input sequence β, and be sure that we know the response of p to both α and β. If {α, β} is a W-set, we can continue a test from a state p that has been fully characterized, or at least from δ(p, β) which is a well-defined state. Jumping to more than two sequences is a bit more elaborate, but it is ensured by the recursive definition of the localizer. Actually, we build embedded cycles.

We illustrate the above discussion on the example in Figure 1.

Figure 1: An FSM to be inferred. This 3-state machine has no distinguishing sequence. However, states can be fully characterized by their traces for sequences from the set W = {a, b}. Suppose we start our experiment when the machine is in state 1 by sending an input a. We shall get an output 1. The localizer will repeatedly apply the input sequence a. The second and third outputs will be 0. Since we know the machine has no more than 3 states, after 3 applications of a, the fourth application will elicit an output which must be one of those previously seen, 0 or 1. In this case, it will be a 0. Now, since the last 3 outputs were 0s, we can be sure that the fifth application of a would elicit a 0. We can now apply a b, and we get 0 as output, since we were trapped in state 2. We know that just before applying the b, we were in a state that answers 0 to both a and b. Since we assume W to be a fully characterizing set, the state is distinguishable from all others. We shall call it the state {a0, b0}, which corresponds to state 2 in the example.

Note that at the end of the localizer procedure we are not in the state p that has been fully characterized, but past it: in the example of Figure 1 we are in state 1 instead of 2, and more generally with W = {α, β} we are actually in δ(p, β). This will also be the case for our generalized localizer: at the end of the procedure, the BB will be in a state that follows the application of the last input sequence w k of the Z set, and the state characterized with the set Z will be the state reached just before applying the last w k sequence. This is not an issue because our inference procedure handles this situation. Note that this means that the sequence built by the localizer is not a homing sequence [START_REF] Lee | Principles and Methods of Testing Finite State Machines -a Survey[END_REF], although it could easily be adapted to provide a kind of homing sequence, modulo the fact that the states are initially unknown, as we discover state characterization while applying the localizer. To make a homing sequence, we would just have to add an empty sequence ε as the last sequence w k+1 of Z.

The localizer procedure is formulated for fixed alphabets I and O, and an assumed bound on the number of states in the black box n. The procedure uses a given sequence ω that has already been observed from the BB and has left it in an unknown state, and given a non-empty ordered set Z of input sequences. It returns an updated ωʹ′ trace (ω concatenated with the new inputs applied by the localizer and observed outputs), the set of traces for Z that can be confirmed as the traces of the state p reached just before the last w k sequence of Z, and the trace suffix observed from the state p.

else let Z = (w 1 , … , w k ), (w 1 , …, w k-2 , w k-1 ) = Z 1 , (w 1 , …, w k-2 , w k ) = Z 2 for i from 0 to 2n -2 do (ω', Tr(Z 1 ), τ i ) := L(ω, Z 1 ) % τ i is tr(w k-1 ) ω := ω' end for Find greatest j, 0 ≤ j ≤ n -1 s.t. for all m ∈ [0, n -2] τ j+m = τ n+m (ω', Tr(Z 2 ), tr(w k )) := L(ω, Z 2 ) return (ω', Tr(Z 2 ) ∪ {τ j+n-1 }, tr(w k )) end if
Note that if k = 2, the list w 1 , …, w k-2 is empty, hence Z 1 = (w 1 ) and Z 2 = (w 2 ). In the for loop, we repeatedly apply the same localizer sequence L(ω, Z 1 ). We store in an array τ i the trace observed for the last element of Z 1 , i.e., tr(w k-1 ). After the n-th application, we must have reached a cycle, where τ n+1 must be equal to some previous τ i . But it could be equal to several τ i therefore we must continue another n -1 times to ensure that we have completed the cycle. In any case, after 2n -1 applications, even if the length of the cycle is unknown, since τ j+n-2 = τ n+n-2 is in the cycle, applying w k-1 instead of w k would have produced τ j+n-1 . Now we know what would be the answer of the state to w k-1 and we can apply w k instead.

We illustrate the localizer procedure on our example in Figure 1. We start from initial state 1, with ω = ε and Z = (a, b). We have Z 1 = (a) and Z 2 = (b). Since the for loop is executed 2n -1 = 5 times, we apply w 1 = a to BB 5 times and reach the 5th step of the trace. We get the trace a1a0a0a0a0, with τ 0 = a1, τ 1 = a0, τ 2 = a0, τ 3 = a0 and τ 4 = a0. At this point, we recognize the cycle τ 2 = τ 3 and τ 3 = τ 4 (j = 2) and we know that if we apply a, we would get 0. Subsequently we apply w 2 = b and get 0.

We identify the state q 0 = {a0, b0} The result of the localizer procedure is thus (a1a0a0a0a0b0, q 0 = {a0,b0}, b0).

The input sequence used by the localizer is a fixed sequence. In our small example, it is a 5 b. For a machine with at most n states and W = {w 1 , w 2 }, the input sequence is w 1 2n-1 w 2 ; with W = {w 1 ,w 2 ,w 3 }, it becomes (w 1 2n-1 w 2 ) 2n-1 (w 1 2n-1 w 3 ), and with W = {w 1 , w 2 , w 3 , w 4 }, it becomes [(w 1 2n-1 w 2 ) 2n-1 (w 1 2n-1 w 3 )] 2n-1 (w 1 2n-1 w 2 ) 2n-1 (w 1 2n-1 w 4 ) and so on.

Example of FSM inference

We now illustrate the proposed method on the example in Figure 1. As illustrated above, applying the localizer procedure allows us to identify a first state of the machine: C(ω \ b0) = q 0 = {a0, b0}. Thus, the prefix obtained in the 5th step is labelled by q 0 . C is updated in the third line of the inference procedure.

We then enter the main while loop in the inference procedure. As the last state of ω (6th step in the trace) is not yet labelled we proceed to the else part of the first if statement. Then γ = b0, χ = a1a0a0a0a0 and σ = b0.

After the first if statement, q = q 0 , K is empty, and we choose w = a. We apply a, observe a1 and arrive at the 7th step. We get K = {(q 0 , b0, a1)}, V = R = ∅.

Since the condition of the second if statement is false, we proceed with the third if statement, which is true. We apply again the localizer procedure, and label the state after a0a0a0a0a0 (12th step) with q 0 : C(12) = q 0 . We then restart the while loop.

We enter the else part of the if statement, with γ = σ = b0. Then q = q 0 , and we choose w = b. We apply b, observe b1 and arrive at the 14th step. We get K = {(q 0 , b0, a1), (q 0 , b0, b1)}.

The condition of the second if statement is now true, we have thus identified a new state q 1 = {a1, b1} and C(13) = q 1 . Then V = {(q 0 , b0, q 1 )}, R = {(q 0 , b)} and C(6) = q 1 . Thus K = {(q 0 , b0, a1), (q 0 , b0, b1), (q 1 , a1, a0)}.

We now execute the third if statement: we apply the localizer procedure and arrive at the 20th step. C(19) = q 0 and C(20) = q 1 . K is unchanged. We then restart the while loop. Since the last (20th) step is now labelled, we enter the then part of the first if statement. α = ε and we choose x = a. We apply a, observe a1 and arrive at step 21. We have σ = a1. Now q = q 1 , and we choose w = b. We apply b, observe b0 and arrive at step 22. We update K = {(q 0 , b0, a1), (q 0 , b0, b1), (q 1 , a1, a0), (q 1 , a1, b0)}.

Since the condition of the second if statement is true, we identify C(21) = q 0 = {a0, b0}. We update V, R, C and K: V = {(q 0 , b0, q 1 ), (q 1 , a1, q 0 )}, R = {(q 0 , b), (q 1 , a)}, C(7) = q 0 , C(22) = q 1 , K = {(q 0 , b0, a1), (q 0 , b0, b1), (q 1 , a1, a0), (q 1 , a1, b0), (q 0 , a0, a0), (q 1 , b1, a0)}. The trace at the last step ( 22) is labelled, and the condition of the third if statement is false.

We then restart the while loop, which allows us to identify a new state q 2 = {a0, b1} and label C(23) = q 2. We apply the localizer procedure and arrive at step 30. C(29) = q 0 , C(30) = q 1 . At this point, V = {(q 0 , b0, q 1 ), (q 1 , a1, q 0 ), (q 1 , b1, q 2 ), (q 2 , b1a0a0a0a0a0, q 0 )}, K = {(q 0 , b0, a1), (q 0 , b0, b1), (q 1 , a1, a0), (q 1 , a1, b0), (q 0 , a0, a0), (q 1 , b1, a0), (q 1 , b1, b1), (q 2 , b1, a0)}, R = {(q 0 , b), (q 1 , a), (q 1 , b)} and C( 14

) = q 2 .
We restart the while loop. As the last step (30) is labelled, we enter the then part of the first if statement. As all transitions from q 1 are now known, we must apply a transfer sequence to move to an unverified transition. We choose to go to q 0 with α = a1 and x = a. We apply a, observe a1, apply a again, observe a0 and arrive at step 32. σ = a0.

We choose w = b, apply b, observe b0, arrive at step 33 and add (q 0 , a0, b0) to K. The condition of the second if statement is true, we have C(32) = q 0 and we add (q 0 , a0, q 0 ) to V. Now R = {(q 0 , b), (q 1 , a), (q 1 , b), (q 0 , a)}, C [START_REF] Irfan | Angluin Style Finite State Machine Inference with Nonoptimal Counterexamples[END_REF]

= C(7) = …. = C(11) = q 0 , C(33) = q 1 .
After applying the while loop two more times, we obtain the trace below, with V = {(q 0 , b0, q 1 ), (q 1 , a1, q 0 ), (q 1 , b1, q 2 ), (q 0 , a0, q 0 ), (q 2 , a0, q 0 ), (q 2 , b1, q 2 )} and R = {(q 0 , b), (q 1 , a), (q 1 , b), (q 0 , a), (q 2 , a), (q 2 , b)}. All transitions are known and q1 We now exit from the while loop and V gives us the inferred finite state machine, which is isomorphic to the FSM in Figure 1.

C(38) = q 2 . 36 1 2 2 1 3 2 1 3 3 q2 b/1 q2 q0 q2 q1 b/1 b/0 a/0 b/1 b/0 a/

6

Proofs and complexity

Proof of localizer

The key theorem for our approach states that the localizer will ensure that the BB reached (before the application of the last sequence from W) a state that can be labelled with the mapping returned by the localizer.

Theorem 1. When Z = W, from any starting state, the localizer will return (ω', X, β) such that C(ω' \ β) = X and X↓I = W.

To prove this theorem, we first introduce notations and two lemmas.

Let IL be the input projection of a trace added by a localizer L(ω, Z), Z = (w 1 , … , w k ) returning ωʹ′ as the first element, i.e., ωʹ′↓I = ω↓I = IL(w 1 , … , w k ). We denote P = IL \ w k , thus, IL(w 1 , …, w k ) = P(w 1 , …, w k-1 ) w k .

Lemma 1. For all k ≥ 1, we have that

P(w 1 , …, w k ) = [P(w 1 , … , w k-1 ) w k ] 2n-1 P(w 1 , …, w k-1 ).
Proof. This lemma is proved by induction from k = 1 for P, accordingly we start with IL(w 1 , w 2 ). In the loop, Z 1 = (w 1 ) and Z 2 = (w 2 ) hence we apply w 1 2n-1 then w 2 . So IL(w 1 , w 2 ) = w 1 2n-1 w 2 , P(w 1 ) = w 1 2n-1 and P(w 1 ,w 0 ) is an empty sequence by definition of IL. Thus indeed P(w 1 ) = [P(w 1 , w 0 ) w 1 ] 2n-1 P(w 1 , w 0 ).

Assuming it is true for some k ≥ 1, then by definition of P we have:

IL(w 1 , …, w k+2 ) = P(w 1 , …, w k+1 )w k+2 .
And by the structure of the localizer, we have:

IL(w 1 , …, w k+2 ) = IL(w 1 , …, w k+1 ) 2n-1 IL(w 1 , …, w k , w k+2 ) = ([P(w 1 , …, w k )w k+1 ] 2n-1 P(w 1 , …, w k )w k+2 .
Using the induction hypothesis, we get:

P(w 1 , …, w k+1 ) = = ([P(w 1 , …, w k )w k+1 ] 2n-1 P(w 1 , …, w k ). QED.
Lemma 2. Let ω' be a trace returned by the localizer for Z = (w 1 , … , w k ) and B = (S, s 0 , I, O, δ, λ), then for all w ∈ Z, λ(s, w) = tr(w)↓O, where s = δ(s 0 , ωʹ′ \ tr(w k )↓I).

Proof. We prove this by induction on |Z|.

For |Z| = 1, tr(w) is the β just observed on applying w at the end of ω which was ωʹ′ \ β; thus λ(s, w) = β↓O = tr(w)↓O.

Let us assume the property holds for |Z| = k -1 ≥ 1. Since Z 2 has k -1 elements, we already have for all w ∈ Z 2 , λ(s, w) = tr(w)↓O (see how s is defined in Lemma 2). The only thing which we have to prove is that λ(s, w k-1 ) = tr(w k-1 )↓O = τ j+n-1 ↓O . Actually, (ωʹ′ \ tr(w k ))↓I = (ω↓I).P(w 1 , …, w k-1 ) by definition of P. Let us denote M = P(w 1 , …, w k-2 ), and q = δ(s 0 , ω↓I). Using lemma 1, we have s = δ(q, P(w

1 , …, w k-1 )) = δ(q, [Mw k-1 ] 2n-1 M) = δ(q, M[w k-1 M] 2n-1 ). Let q i = δ(q, M[w k-1 M] i
), and λ i = λ(q i , w k-1 ) for i ∈ [0, 2n -1]. Note that s = q 2n-1 and according to the notations of the algorithm, for all i ∈ [0, 2n -2] λ i = τ i ↓O. Since there are at most n distinct states, and we repeat the sequence w k-1 M, q n must be equal to one of the q j' for some j' < n. Then, for all m ∈ [0, n -1], λ j'+m = λ n+m . Hence there is at least one such j, as required by the algorithm.

• If q n = q p for some p > 0, then the length of the cycle is n -1 at most and for any j < n such that for all m ∈ [0, n -2], λ j+m = λ n+m then we have:

λ j+n-1 = λ n+n-1 = λ(s, w k-1
). • If the greatest j is 0, this means there is no cycle of output of length less than n, then q n = q, q n = q 0 and s = q 2n-1 = q n-1 and λ(s, w k-1 ) = λ j+n-1 since j = 0. • So in both cases we have λ(s, w k-1 ) = λ j+n-1 = τ j+n-1 ↓O.

QED.

It may be worth mentioning that taking the largest j means we identify the shortest cycle of outputs. The cycle of states entered by the implementation will have a length that is divisible by n-j: with the notation of the proof, n -j divides n -jʹ′.

We can now proceed to the proof of the Theorem 1. Recall that we denote states of the BB by their Tr(W).

Actually, in all cases, Tr(X)↓I = Z. This directly follows from the recursive definition: it holds for a singleton, and when we compute Tr for (w 1 , … , w k ) we produce a set of traces that adds some tr(w k-1 ) thus the set of traces is computed on Z 2 = (w 1 , …, w k-2 , w k ). If Z = W then by Lemma 2, the definition of C and the fact that C is revealing, we have C(ω' \ tr(w k )) = X and X↓I = W. QED.

Proof of the method

To prove the correctness of the method we need to demonstrate that the mappings correspond to the states of the BB. We will use the following theorem.

Theorem 2. If q ∈ Q C then ∃p ∈ P such that q ↔ p.
This theorem follows from the definitions of C and Q C . The proof of the method itself (captured by Theorem 3) proceeds in several steps following the structure of the algorithm. In particular we must prove that all the steps that rely on an existence ("find", "choose") are well defined and will find an element, and we show that the algorithm increases monotonically the set of known states and transitions, and terminates when a conjecture can be built which is equivalent to the FSM B = (P, p 0 , I, O, δ, λ).

1. On every entry in the while loop, either we are in a known state, i.e. the BB is in a state p such that C(ω) = q ↔ p or we are at the end of a localizer, i.e., C(ω \ tr(w p )) is defined (a known state). This is trivial on the first entry in the loop, since we just applied the localizer and did not move in the BB. And at the end of a cycle in the loop, we reach either after the case C(ω) = ⊥, in which case we reapply the localizer and are again at the end of it, or C(ω) is defined. 2. Find a shortest α: since we entered the while loop, we know that ∃qʹ′ ∈ Qω and

x ∈ I, such that (qʹ′, x) ∉ R. Moreover, we are in a state q. Then either ∃xʹ′ ∈ I, such that (q, xʹ′) ∉ R, and we just have to pick α = ε; or we know all successors of q. In that case, we build the connected graph reachable from q through verified transitions: if one of them has an unverified transition, we pick the one closest to q, i.e., that yields the shortest α. Otherwise, this would imply that there is a qʹ′ ∈ Q C such that there is a prefix ∃σ ≤ ω, C(σ) = qʹ′ which would be distinct from all the successor states of q that constitute a strongly connected component. Since all successor states and this state qʹ′ are all paired (through the ↔ relation) to states of the BB (by Theorem 2), this would contradict the assumption that the BB is strongly connected. 3. "Else find the shortest γ". In this else branch, we are in the case where C(ω) = ⊥ . The existence of γ follows from 1: γ = w p in this case. 4. "Choose w": this comes one line after the "end if". If we followed the "else" branch, state C(χσ) ∉ dom(C) and there is a w for which (q, σ, tr(w)) ∉ K. If we followed the "then" branch, then (q k+1 , x) ∉ R and σ := xo and by definition of R, we again have a w. 5. Progress: each loop iteration adds an element to K (by the structure of the loop), either at the end of a transition (xo) or at the end of a localizer. 6. Termination: there is a finite number of transitions in the BB (hence in the set Q C by Theorem 2), each one is followed by a finite number of traces from the (finite) set W. Hence the potential number of elements in K is finite, and the process will terminate. 7. Building the conjecture: based on Theorem 2, we can build a conjecture that is isomorphic to the BB by connecting all the transitions of R when the algorithm terminates. Theorem 3. The inference procedure terminates and yields a conjecture that is isomorphic to the minimal FSM modelling the BB.

Complexity

As in all testing procedures, interacting with the system under test contributes mostly to the cost. Therefore we analyse the worst case complexity as the length (number of inputs) of the test sequence created by the procedure. The key element is the length of the localizer. Let L be the length of L(ω, W) and |w i | the length of an element of W. As in the notations of the algorithm, p = |W| is the number of elements of the characterization set, n is the number of states, and f is the number of inputs (fan-out). Thus, L can be computed as follows.

L = ( ((|w 1 |) × (2n -1) + |w 2 |) × (2n -1) +… + |w p-1 |) × (2n -1) + ((|w 1 |) … × (2n -1) + |w p-2 |)+ |w p | . O(L) = |w 1 | (2n-1
) p since we can assume that for any i, we have |w i | < n: it is known that in a complete FSM with n states, any two states can be distinguished by a sequence of length no more than n. Thus, the length of the localizer is polynomial in n and exponential in p.

We apply the localizer at most once for each execution of the loop. The loop itself adds at least one element to K, thus the number of iterations of the loop is n(f + p)p. Within the loop, the extension to ω would be U = max(|α| + 1 + |w|, |γ|+|w|). |γ| + |w| is bounded by 2n, and |α| is bounded by n 2 . Then the overall complexity would be L+ n(f + p)p (L + U) bounded by (n(f + p)p + 1)(L + n 2 + n + 1). As a coarse bound, we have (n(f + p)p + 1)(n(2n -1) p + n 2 + n + 1) which is O(p(f + p) 2 p n p+2 ), again polynomial in n and exponential in p.

Of course, this is a coarse upper bound for a worst-case complexity, and it is unsure it could be reached or even approached. As can be seen from the example, as soon as states and transitions are added to Q and V, the number of uses of the localizer decreases. Given the structure of the localizer, the sequences in W would be ordered by increasing length. And the localizer could be shortened because we may recognize cycles before reaching 2n -1 iterations.

Our experiments with hundreds of randomly generated machines show that for n = 15, f = 10, inference is achieved in around 10 4 steps for p = 2 (around 7000 when |w 1 | = 1, and around 15000 when |w 1 | = 2), i.e., around 500 times (3 orders of magnitude) less than the theoretical bound. To put this in perspective, we had initially tried classical inference methods [START_REF] Petrenko | Inferring Approximated Models for Systems Engineering[END_REF] [16] on web applications, where a reset would typically take more than 1 minute (restarting a virtual machine and restoring data configuration), whereas interacting with it over a local network would take around 1ms per I/O pair. In such typical contexts, an inference sequence of length 10 5 would require no more time than a single reset.

Discussion

Our method assumes we know an upper bound n on the number of states of the BB and a characterization set W for it. We now discuss the impact of these assumptions. First let us remark that the localizer does not assume that W is characterizing. It can work with any set Z and just ensures that we characterize a state reached w.r.t. Zequivalence [START_REF] Petrenko | Inferring Approximated Models for Systems Engineering[END_REF]. However, an incorrect value for n could disrupt the localizer.

Actually, if either n or W is wrong (i.e., the assumptions for the BB are not satisfied), then two cases can occur:

1. The inference procedure runs to the end, but produces an FSM that is not isomorphic to a model of the BB. 2. The inference procedure detects an inconsistency (or fails to converge).

In the first case, we can either consider that the inference procedure provides a model that is approximate, and consistent with all observations: it will have produced an unrefined model of the BB that may be enough for the intended use of the model. Alternatively, we could now use the inferred model to check whether the BB conforms to this model, by some method of conformance testing, e.g., randomly walking through the model until we find a discrepancy or conclude on some level of confidence for the approximated model.

In the second case, let us first consider the case where n was an incorrect bound (too low), and this impacts the localizer. The only problem that can occur there is in the line "find the greatest j". We may fail to recognize a cycle in 2n -1 iterations. This can be easily addressed: first, we would continue iterating the for loop until we spot such an output cycle; then, we increase the value of n accordingly; at this point, we restart the whole inference procedure, because we cannot trust the previous equivalence of states.

Let us now consider the case where W would not be characterizing. This will not create any problem in the localizer, but in the main procedure. When we reapply a verified sequence α to go to a given state q k+1 or when we reapply an input x we may get a different output. This implies that the sequence we just applied distinguishes two states that we thought were equivalent. That sequence, or a part of it (up to the first divergence) could be added to W.

This can also be related to the initial assumption about W. The main issue is about how a characterizing set for a black box can be known. One possibility could be that we had such a set for a previous version of an implementation, and we take it as input of the method when we need to infer an updated implementation. It may also be possible to formulate domain-specific heuristics to identify candidate characterization sets.

Conclusion

We have presented a method that can infer a model of a non-resettable black box FSM for which we know an upper bound n on the number of states and a characterizing set W. The method is polynomial in n; the degree of the polynomial is bounded by the cardinality of W. It has now been implemented, and we are investigating its effectiveness under various settings. We are in particular interested in assessing the average complexity for various cases of characterization sets.

It might also be interesting to see how the algorithm proposed here could benefit from the improvements that have been proposed in the related problem of conformance testing for non-resettable machines. As mentioned in several parts of the paper, the algorithm lends itself to optimizations that could reduce the length of the sequence of inputs. In particular, the number of iterations in the localizer could be reduced when short cycles are recognized.

Another direction for research is on relaxing the assumptions, and providing adaptive heuristics. One direction could be to work towards inference of quotients [START_REF] Petrenko | Inferring Approximated Models for Systems Engineering[END_REF].

  Figure1: An FSM to be inferred. This 3-state machine has no distinguishing sequence. However, states can be fully characterized by their traces for sequences from the set W = {a, b}. Suppose we start our experiment when the machine is in state 1 by sending an input a. We shall get an output 1. The localizer will repeatedly apply the input sequence a. The second and third outputs will be 0. Since we know the machine has no more than 3 states, after 3 applications of a, the fourth application will elicit an output which must be one of those previously seen, 0 or 1. In this case, it will be a 0. Now, since the last 3 outputs were 0s, we can be sure that the fifth application of a would elicit a 0. We can now apply a b, and we get 0 as output, since we were trapped in state 2. We know that just before applying the b, we were in a state that answers 0 to both a and b. Since we assume W to be a fully characterizing set, the state is distinguishable from all others. We shall call it the state {a0, b0}, which corresponds to state 2 in the example.Note that at the end of the localizer procedure we are not in the state p that has been fully characterized, but past it: in the example of Figure1we are in state 1 instead of 2, and more generally with W = {α, β} we are actually in δ(p, β). This will also be the case for our generalized localizer: at the end of the procedure, the BB will be in a state that follows the application of the last input sequence w k of the Z set, and the state characterized with the set Z will be the state reached just before applying the last w k sequence. This is not an issue because our inference procedure handles this situation. Note that this means that the sequence built by the localizer is not a homing sequence[START_REF] Lee | Principles and Methods of Testing Finite State Machines -a Survey[END_REF], although it could easily be adapted to provide a kind of homing sequence, modulo the fact that the states are initially unknown, as we discover state characterization while applying the localizer. To make a homing sequence, we would just have to add an empty sequence ε as the last sequence w k+1 of Z.The localizer procedure is formulated for fixed alphabets I and O, and an assumed bound on the number of states in the black box n. The procedure uses a given sequence ω that has already been observed from the BB and has left it in an unknown state, and given a non-empty ordered set Z of input sequences. It returns an updated ωʹ′ trace (ω concatenated with the new inputs applied by the localizer and observed outputs), the set of traces for Z that can be confirmed as the traces of the state p reached just before the last w k sequence of Z, and the trace suffix observed from the state p.Localizer procedure Signature L: ((IO)* × (I*) + ) → ((IO)* × 2 (IO)* × (IO)*)

Acknowledgments

The authors acknowledge the work of Laurent Anadon, an intern from Ecole Polytechnique with whom we started this problem on the DS case. The implementation of the algorithm was carried out by Nicolas Brémond, an intern from Enseirb-Matmeca. A. Simao had financial support of Brazilian Funding Agencies, FAPESP and CNPq. A. Petrenko acknowledges financial support of NSERC via Discovery grant RGPIN/194381-2012.


Muhammad Waqar Aziz
email: mwaziz@uqu.edu.sa

Syed Abdul

Baqi Shah
email: sashah@uqu.edu.sa

Test-data Generation for Testing Parallel Real-Time Systems

Keywords: Test-data generation, Genetic Algorithm, Real-time systems, Measurement-based analysis, Worst-Case Execution Time analysis, End-to-end testing

The Worst-Case Execution Time (WCET) of real-time systems is mainly influenced by the program design, its execution environment and the input data. To cover the last factor in the context of WCET estimation, the objective of this work is to generate the test-data that maximize the execution times of the parallel real-time systems. In this paper, a test-data generation technique is proposed that uses Genetic Algorithms to automatically generate the input data, to be used for testing of parallel real-time systems. The proposed technique was applied to a parallel embedded application -Stringsearch. The result was an analysis that took as input the parallel program and generated the test-data that cause maximal execution times. The generated test-data showed improvements by exercising long execution times in comparison to randomly generated input data.

Introduction

With the wide use of multicore processors in desktop computers and embedded systems, and the growing demands of high performance real-time applications, it is expected that multicore processors will be increasingly used in real-time systems [START_REF] Yan | Wcet analysis for multi-core processors with shared l2 instruction caches[END_REF]. The deployment of real-time applications on multicore platforms with tens or hundreds of cores may become a reality very soon [START_REF] Calandrino | A hybrid real-time scheduling approach for large-scale multicore platforms[END_REF]. This demands special methods and techniques for the design and testing of future multicore embedded real-time systems, where the previous research mostly assumes sequential code running on single-core platforms.

The fundamental property to guarantee the performance of a real-time system is its Worst-Case Execution Time (WCET) testing. The worst-case bounds can be derived either by using static timing analysis [START_REF] Heckmann | Worst-case execution time prediction by static program analysis[END_REF], or by measuring the programs execution time on a given hardware or simulator using a set of inputs [START_REF] Wilhelm | The worst-case execution-time problemoverview of methods and survey of tools[END_REF]. The static timing analysis methods applied on hardware and software models of the system are very difficult to apply for parallel systems. For instance, the inter-thread interferences among shared resources, e.g., L2 caches are hard to analyze statically [START_REF] Yan | Wcet analysis for multi-core processors with shared l2 instruction caches[END_REF]. In contrast, measurement-based methods can be used for better estimating the execution time of parallel systems and therefore are widely used in the industry.

The problem of WCET testing is to find the test-data that causes execution of the longest path of the program, and thus causes the longest execution time. But to do so, a complete test with all possible inputs, generally cannot be carried out. Similarly, exhausting all the possible program paths, for a given input, is usually infeasible. To handle these problems, evolutionary testing can be utilized that automatically searches the test-data to estimate the WCET. For instance, if searching the worst-case inputs from the set of all possible inputs is considered as an optimization problem, Genetic Algorithms (GA) [START_REF] Berg | Requirements for and design of a processor with predictable timing[END_REF] can be utilized to automatically search the required test-data.

The current research efforts of WCET analysis for multicore systems are focused on performance enhancing hardware features [START_REF] Rochange | Wcet analysis of a parallel 3d multigrid solver executed on the merasa multi-core[END_REF][START_REF] Kästner | Meeting real-time requirements with multi-core processors[END_REF][START_REF] Liang | Timing analysis of concurrent programs running on shared cache multi-cores[END_REF], and application [START_REF] Ozaktas | Automatic wcet analysis of real-time parallel applications[END_REF][START_REF] Potop-Butucaru | Integrated worst-case response time evaluation of multicore non-preemptive applications[END_REF][START_REF] Ding | Multicore-aware code co-positioning to reduce wcet on dualcore processors with shared instruction caches[END_REF] or programming level [START_REF] Yip | Predictable Parallel Programming Using PRET-C[END_REF][START_REF] Yip | Programming and timing analysis of parallel programs on multicores[END_REF][START_REF] Gustavsson | Toward static timing analysis of parallel software[END_REF]. However, there is lack of research in test-data generation for WCET estimation of parallel real-time systems executing on multicore architectures. To fill this gap, this work proposes a Search-Based Software Engineering (SBSE) technique to generate test-data for testing parallel real-time systems. The proposed technique uses GA to sub-optimally evolve the worst-case inputs, with the objective to find those inputs that will cause the program to take longest execution time.

The proposed technique is applied by measuring the end-to-end execution time of the ParMiBench benchmark suite [START_REF] Liang | OpenMPBench-An Open-Source Benchmark for Multiprocessor Based Embedded Systems[END_REF]. ParMiBench is an open source parallel version of a subset of MiBench benchmark suite [START_REF] Guthaus | Mibench: A free, commercially representative embedded benchmark suite[END_REF] -many of whose benchmarks appear to be suitable candidates for WCET analysis [START_REF] Gustafsson | The mälardalen wcet benchmarks: Past, present and future[END_REF]. ParMiBench benchmark suite, actually designed to evaluate the performance of embedded multi-core systems, is implemented using C language and POSIX threads to achieve parallelism and supports Unix/Linux based platforms [START_REF] Liang | OpenMPBench-An Open-Source Benchmark for Multiprocessor Based Embedded Systems[END_REF]. The end-toend time was measured by gathering the execution traces of the parallel program using the Gem5 simulator [START_REF] Binkert | The gem5 simulator[END_REF].

This article is organized as follows. Section 2 explains the methodology followed in this work. Section 3 describes the method to approach the problem of test-data generation along with the details of the actions performed. Section 4 reports the experimental setup and the results obtained from the experiment. The evaluation of this work is provided in Sect. 5. Section 6 describes related work in measurement-based WCET analysis for parallel real-time systems. Section 7 contains concluding remarks and directions for future work.

Methodology

The ParMiBench benchmark suite, used in this work, is a set of embedded parallel benchmarks from various domains of the embedded applications which include, control and automation, networks, offices, and security. However, we have selected the Stringsearch benchmark from the suite that is related to searching a token (strings stored in a pattern file) from a text file, due to the following reasons:

-In this work, the benchmarks are seen as a black box that consumes input and generates timing information. However, for the testing process to be effective and the testing results to be meaningful, we need benchmarks with a rich input space. the current Gem5 framework forces to execute the benchmarks from within a disk image in the full system mode. This requires the benchmarks to have input parameters that can be easily fed, e.g., via command line.

In the initial experiment, the simulation was executed with the existing data set of Stringsearch benchmark. However, the initial experiment revealed that the text and pattern files in the existing data set consist of repeated contents. Consequently, any new pattern file generated, with tokens picked up randomly from the text file, had tokens that exist in every line of the file regardless of which line they have been picked. Thus, the existing data set of the benchmark was inappropriate to allow evolutionary testing, as the data set should not contain duplicate values. Therefore, a new text file with dissimilar tokens was generated that consists of 102400 random characters (file size ≈ 100 KB), and a pattern file containing 64 tokens each of five characters length. The token length was kept fixed (i.e., five characters, similar to the given benchmark) to observe the execution time variations unassociated with the input length. Additionally, fixed size inputs allow the easy alignment of parts during crossover operation.

In this work, Gem5 architecture simulator was used to measure the end-toend execution time of the parallel benchmark. Gem5 was selected as it provides full-system simulation to execute a program in the operating system environment, with support of several commercial Instruction Set Architectures (just as ARM, ALPHA). To get the execution traces of our interest, we performed some tweaking to the simulator. We applied a Kernel patch and made some custom modifications to the simulator to get the execution traces of the benchmark. 1These traces were then used to calculate the end-to-end execution time of the benchmark. Instead of manual calculation, the end-to-end execution time was calculated automatically by a Java application.

Proposed test-data generation technique

The technique proposed in this work for test-data generation, is based on SBSE approach, namely GA. GA mimics the process of natural selection and chooses the best from one generation to produce the next generation and attempts to reach the solution much faster than otherwise. The steps of the proposed testdata generation technique, as depicted in Fig. 1, are described is below:

Define the Initial Population

For applying GA, an initial population of individuals need to be defined which is evolved across a number of generations. Individuals are usually random guesses to the solution of a problem. Care should be given to maintain diversity in the population so that premature convergence towards a sub-optimal solution can be prevented. For instance, in case of Stringsearch, a good candidate for the best individual produced by the GA in the last generation is the input to the program where all tokens to be searched do not exist in the text file.

To achieve this, an intuition-based selection was made to start from a point where 50% of tokens exist in the text and 50% do not. An initial population of one hundred pattern files, to be used in GA, was generated using the following ways: a) By randomly picking up tokens from this newly generated text file b) By randomly generating totally new tokens Consequently, each file contained a set of tokens gathered from a mixture of 50% randomly generated tokens and 50% tokens picked up from the text. Thus, the chances of each token within a pattern file are equally likely to be in the text or not, making it a fair distribution to start with.

To conclude, there are (n*k)/2 tokens that exist in the text, and are randomly distributed among the total n*k tokens in n files (considering n pattern files, each having k patterns). This allows to give the 50-50 found/not found distribution without making individuals in the population biased. This set of one hundred pattern files collectively formed the genetic representation of the solution domain. Thus, the initial population in this experiment consists of one hundred chromosomes and 64 genes of each chromosome, in GA terminology.

End-to-End Time Calculation

In this work, it is proposed to use the end-to-end execution time of parallel program as fitness function. The end-to-end time was calculated from the traces obtained from the Gem5 simulator by executing the parallel application. Each trace was generated by detecting the starting and ending points of a thread execution. A Java application was written to automatically calculate the end-toend time from the obtained execution traces. In the initialization phase, the endto-end time was calculated for all the 100 files present in the initial population. The simulation was run one hundred times to generate one hundred traces, i.e., one time for each pattern file. However, in all the other iterations it was calculated for the new individuals of the next generation only.

Applying Genetic Algorithm

GA uses the concept of natural evolution to reach the desired solution from a given huge search space. The main idea of using GA, in this work, is to execute the program with sets of inputs throughout a number of generations. The process starts with generating k random vectors initially (first generation) and obtain their timing information. Then, the generated k random inputs with the timing information are used to produce the next k inputs (second generation). This process is repeated for n generations. The details of the steps of GA as followed in the proposed technique are given below.

Calculate the Fitness Value

The fitness of the individuals is a problem-dependent value that specifies the goodness of an individual in solving the problem at hand. The selection of an individual for the next generation depends on its fitness value, i.e., each individual in the population is evaluated by calculating its fitness. The fitness value is used to select the best of any generation to 'mate' them in order to produce the new generation. As already mentioned, the end-to-end time is considered as a fitness value, in this work. Thus, the longer the end-to-end time, the higher would be the fitness. The fitness value is generated in GA through fitness function. It means that calculating the fitness function requires the execution of the program to produce traces. The time taken by Stringsearch to execute each pattern file was considered as the fitness value of that pattern file. The use of GA is suppose to search the inputs with higher fitness values in each generation. In this way, the program execution using GA would lead towards inputs having larger fitness values. It is worth mentioning here that cache hits or misses, thread conflicts or any other parameters were not considered to evaluate the fitness. Because considering these parameters is a huge research in its own and requires more effort and time. In addition, Gem5 simulator does not provide much information about these parameters which can be useful at this level.

Select the Individuals

A selection strategy is applied to the individuals of a population in a given generation to decide which ones are allowed to proceed to the next generation. To make a rank based selection, the individual need to be sorted based on their fitness values. It is proposed to select only five individuals, as selecting more individuals would take more time in the remaining steps and also in calculating their fitness in next generation. In this experiment, the pattern files were sorted based on their fitness values. The top five pattern files were selected as chromosomes for the next generation. Top five files were selected because selecting 50 files, for instance, will be a big enough number as it will make 100 files for the next generation which will take too long to calculate their fitness.

Crossover

The evolution of the population involves the exchange of genetic material between the individuals through crossover operation. Traditionally, this is achieved by choosing a point along two bit strings at random and swapping the tails. To produce new files, a crossover was made amongst the top five selected pattern files, by merging two lists of tokens picked up from randomly selected pattern files. This crossover resulted in ten new chromosomes. In crossover, one part of a file was concatenated with another part of the second file, where the size of selected parts may not be the same, e.g., 2 tokens picked from one file were concatenated with 62 tokens from the other file. This selection is based on cutting one chromosome at a random location and concatenating it with the remaining part of the second chromosome cut at the same location.

Mutation

The evolution of the population also involves the alteration of the genetic material of a single individual through mutation operation. Mutation is achieved by picking a bit at random and flipping its value. Mutation was applied to the results of crossover to produce and further improve the next generation. It was done by randomly picking a token from a pattern file and replacing its any letter with another random character. This process was repeated until the desired percentage of mutation was achieved. In this way, the next generation of 10 chromosomes was produced.

The above process was repeated for a set of ten chromosomes, which was reproduced after each generation. The evolution continues until a good-enough individual that solves the problem adequately is found, or until a maximum number of generations is reached. Opting for the latter case, the whole process was repeated for 50 generations, as the probability of improving over several generations is high.

With the above modeled parameters, a Java application was developed that implemented GA in the experiment. The implementation used the given pattern files composed of tokens without converting them into binary strings. This simplified the complex problem of coding and decoding of inputs for this specific case.

Experimentation

Experimental Setup

The Gem5 configurations, as used in this experiment, included four cores of ARM detailed architecture as specified by Gem5 (ARMv7-A ISA based) with default size of L2 cache (2MB) and 256 MB of Memory. The disk image contained ARM embedded Linux (AEL) as the guest operating system for the simulator. We used Gem5 to run the simulations and execute benchmarks for collecting the kernel level thread traces and computing the end-to-end times. We had Xeon processor with twelve logical cores and enough memory (48GB) available in our machine to accommodate multiple instances of simulator running in parallel.

Experimental Results

To observe the effects of applying GA using visual representation, graphs of the calculated end-to-end times were plotted for each generation. In each graph, the length of the execution time is represented on the vertical axis in terms of CPU ticks, whereas the ten pattern files of each generation are represented horizontally. For example, in first generation the highest and the lowest values were found as 59843433000 and 59603617500 ticks for 4th and 8th pattern files respectively, as shown in Fig. 2a. Some other results produced during fifty generations are depicted in the remaining parts of Fig. 2.

From the plotted graphs, i.e., the measured end-to-end times, it is observed that by using GA an overall improvement can be achieved in the fitness values corresponding to the pattern files. For instance, in first and third generations (Fig. 2a and2b) there are only three pattern files which caused the program to execute for a period longer than 5.98e+10 ticks. In comparison, the number of pattern files, which execute longer than this number of ticks, is increased to eight pattern files in 25th generation and nine pattern files in 50th generation (Fig. 2c and2d). This increase in the number of input files after applying several generations shows that the inputs are taking longer time. This is a clear indication that the proposed technique has improved the inputs, i.e., those inputs are generated that cause the longest time to execute.

Table 1 shows the WCET measured during the experiments in different generations for five character length input token. A threshold value of 5.98e+10 was defined to analyze the improvement in the inputs over all generations. The number of files taking greater or equal time than the threshold value was counted, as represented by Above (Th.5.98) column in Table 1. An increasing number of input files above the threshold can be observed, in Table 1, except for 30th generation. This is due to the very nature of GA where results can degrade even after reaching to an improved position. However, an overall improvement is achieved across 50 generations.

Evaluation

In order to evaluate the scalability of the proposed technique, the experiment was repeated with other input files as given with the benchmark. To this end, the complete process was re-performed for tokens with a length of 10 characters; compared to the original experiment where five characters input token was used. Some of the graphs, representing different generations produced using 10 characters length are depicted in Fig. 3. The WCET measured for input tokens of 10 characters length are displayed in Table 2. The threshold value, in this case, was defined as 5.9e+10 with the same purpose of analyzing the inputs over all generations.

From Table 2, it can be observed that the number of input files increased with the number of generations. Although the number of files slightly increased and decreased due to GA, an overall steady increase in the number of files was observed after 50th generations.

Related Work and Discussion

Most of WCET-analysis research is performed for sequential software and singlecore hardware. Recently, research on WCET analysis of sequential code on multicore processors has been a main focus. The work that has been done in this area so far can be divided into two parts (1) static hardware modeling for WCET analysis on multi-core architectures [START_REF] Gustavsson | Towards wcet analysis of multicore architectures using uppaal[END_REF][START_REF] Wu | Bounding worst-case execution time for multicore processors through model checking[END_REF][START_REF] Yan | Wcet analysis for multi-core processors with shared l2 instruction caches[END_REF][START_REF] Zhang | Accurately estimating worst-case execution time for multicore processors with shared direct-mapped instruction caches[END_REF], and (2) design of analyzable multi-core computers that favor timing predictability over performance [START_REF] Guan | Cache-aware scheduling and analysis for multicores[END_REF][START_REF] Pitter | A real-time java chip-multiprocessor[END_REF][START_REF] Rosen | Bus access optimization for predictable implementation of real-time applications on multiprocessor systems-on-chip[END_REF][START_REF]Merasa: Multicore execution of hard real-time applications supporting analyzability[END_REF]. In relation to this work, research on parallel applications running on multicore architectures is very limited. For instance, Rochange et al. [START_REF] Rochange | Wcet analysis of a parallel 3d multigrid solver executed on the merasa multi-core[END_REF] highlights the problem of analyzing the timing behavior of non-sequential software on a multi-core architecture. They report a manual analysis of a parallel application, which determines the synchronization and communication between its executing threads.

In contrast, we have used GA to heuristically search the input from a huge search space of tokens that would cause the program to execute for the longest period of time. It was observed that the execution time of the search tends to decrease with the increase in size of the input text (see e.g., WCET of 5 and 10 characters). In general, the proposed technique is applicable to any parallel realtime system where optimization is needed. This further requires that the system under consideration can be genetically represented and has a fitness function for its evaluation. However, the proposed technique should be complemented with Evolutionary search (more specifically GA) has been employed in the literature [START_REF] Gross | An evaluation of dynamic, optimisation-based worst-case execution time analysis[END_REF][START_REF] Khan | Wcet analysis of modern processors using multi-criteria optimisation[END_REF][START_REF] Wegener | A comparison of static analysis and evolutionary testing for the verification of timing constraints[END_REF] to find long execution times of real-time programs. Although, research on using GA for testing real-time systems dates back to 90s [START_REF] Wegener | Testing real-time systems using genetic algorithms[END_REF], it has not been used for WCET analysis of parallel programs running on multi-core hardware, to the best of our knowledge. The fitness function used in this work considered the end-to-end time for the execution of a program as the fitness value. This consideration has helped us to produce good enough results by using GA that maximized the fitness value.

Conclusion

In this paper, a measurement-based technique is proposed for automatic testdata generation for parallel real-time systems running on a multicore architecture. The technique uses Genetic Algorithm to generate test data that maximize the execution times of the parallel application. It evolves input vectors that cause long execution times of the program using evolutionary testing. The results of the experiment showed a significant improvement in the execution times of input files after applying the proposed technique. Thus, the aim of producing large execution times, which are either the WCET or close to it, was achieved.

In the future, we aim to use a real-life, real-time application to evaluate our work. In case of publicly-unavailability of such applications, the method can be tested with other benchmarks of ParMiBench. Moreover, the static timing analysis is planned to be performed to evaluate the safeness and tightness of the proposed technique. Although, the end-to-end time is considered as an output to the fitness function, it is also planned to consider a richer multi-objective fitness function in future that might include thread conflicts, cache misses/hits and cache sizes.

Fig. 1 :

 1 Fig. 1: GA based test-data generation technique proposed for parallel real-time systems

Fig. 2 :

 2 Fig. 2: End-to-End times (fitness values) in different generations for the pattern files with five characters long tokens

Fig. 3 :

 3 Fig. 3: End-to-End times (fitness values) in different generations for the pattern files with ten character long tokens

Table 1 :

 1 Measured WCET across different generations for 5 characters length token

	Input token size Generation No.	WCET	Above (Th.5.98)
		1	59843433000	3
		10	59878900000	5
		20	59895367000	8
	5 characters	30	59898941500	6
		40	59896569500	7
		50	59898461000	9

Table 2 :

 2 Measured WCET across different generations for 10 characters length token

	Input token size Generation No.	WCET	Above (Th.5.90)
		1	59102869500	4
		10	59134277000	5
		20	59097647500	6
	10 characters	30	59100034000	6
		40	59181076000	7
		50	59181090000	9

Interested readers can visit our technical report for more configuration details, http://bit.ly/1JqheNS.

Acknowledgments. This research is funded by the program of strategic technologies of the National Science, Technology, and Innovation plan in Saudi Arabia (Grant No. 11-INF1705-10). We acknowledge KACST (King Abdulaziz City for Science and Technology) for funding this research and STU (Science and Technology Unit), Umm Al-Qura University, Makkah for providing necessary support.