Matthieu Renard

Antoine Rollet

Yliès Falcone
email: ylies.falcone@univ-grenoble-alpes.fr

GREP: Games for the Runtime Enforcement of Properties

We present GREP, a tool for the runtime enforcement of (timed) properties. GREP takes an execution sequence as input (stdin), and modifies it (stdout) as necessary to enforce the desired property, when possible. GREP can enforce any regular timed property described by a deterministic and complete Timed Automaton. The main novelties of GREP are twofold: it uses game theory to improve the synthesis of enforcement mechanisms, and it accounts for uncontrollable events, i.e. events that cannot be controlled by the enforcement mechanisms and thus have to be released immediately. We present an overview of GREP and validate its usability with a performance evaluation.

Runtime Enforcement of Timed Properties with Uncontrollable Events

Runtime Verification (RV, [START_REF] Leucker | A brief account of runtime verification[END_REF][START_REF] Falcone | A tutorial on runtime verification[END_REF][START_REF] Bartocci | First international competition on runtime verification: rules, benchmarks, tools, and final results of crv[END_REF]), also referred to as passive testing ( [START_REF] Cavalli | New approaches for passive testing using an extended finite state machine specification[END_REF][START_REF] Alcalde | Network protocol system passive testing for fault management: A backward checking approach[END_REF]), consists in checking if the execution of a running system satisfies some given specification. Unlike static verification, RV studies a real execution of a system, possibly after deployment. This paper deals with runtime enforcement (RE, [START_REF] Schneider | Enforceable security policies[END_REF][START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF][START_REF] Basin | Enforceable security policies revisited[END_REF]), an extension of runtime verification where executions are corrected when they violate the desired property (see [START_REF] Falcone | You should better enforce than verify[END_REF] for an overview). An enforcement mechanism (EM) modifies the execution of a running system: it takes an execution as input and outputs a possibly-different execution. One of the advantages of RE is that the whole specification of the system under scrutiny is not necessary to generate an EM, only a property that should be satisfied by its output is needed. The general scheme is given in Fig. 1. We distinguish two categories of actions: controllable actions which can be modified by an enforcement mechanism, and uncontrollable actions which can only be observed by the enforcement

S σ E E(σ) ϕ
Fig. 1: Schematic description of an enforcement mechanism E, modifying the execution σ of the system S to E(σ), so that it satisfies the property ϕ.

Write

x < 2 Write Σ Fig. 2: Property ϕ t modelling writes on a shared storage device ( [START_REF] Renard | Enforcement of (timed) properties with uncontrollable events[END_REF]) mechanism. Enforcement mechanisms should be sound, compliant and optimal, meaning that the output should satisfy the specification when possible, the output should be as close to the input as possible, and the output should be maximal, respectively. In [START_REF] Renard | Enforcement of (timed) properties with uncontrollable events[END_REF][START_REF] Renard | Optimal enforcement of (timed) properties with uncontrollable events[END_REF], we introduce runtime enforcement for timed properties with uncontrollable events, and we propose a game approach for generating the EM in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF]. A comparison of this approach with related work may also be found in [START_REF] Renard | Optimal enforcement of (timed) properties with uncontrollable events[END_REF]. GREP implements the game approach of [START_REF] Renard | Runtime enforcement using Büchi games[END_REF] extended to timed properties.

Timed Properties and Automata

In this paper, properties are modelled with regular timed properties described by Timed Automata (TA) [START_REF] Alur | The theory of timed automata[END_REF]. Consider the following property on a simple shared storage device: after Authentication, a user can write a value only if the storage has been unlocked for at least 2 time units. (Un)locking the device is decided by another party, meaning that it is not controllable by the user. This property is formalised by the TA ϕ t given in Fig. 2, with the alphabet of uncontrollable actions {LockOn, LockOff, Auth}. In ϕ t , the set of locations is L = {l 0 , l 1 , l 2 , l 3 }; the initial location is l 0 ; the set X = {x} made of a single clock x is used to model time; the alphabet of all actions is Σ = {Auth, LockOn, LockOff, Write}; the set of accepting locations is G = {l 1 , l 2 }; and the set of transitions ∆ contains, for example, (l 1 , x ≥ 2, Write, ∅, l 1 ). A transition is composed of an initial location, a guard, an action, a set of clocks to reset, and a target location. For instance, the transition (l 1 , x ≥ 2, Write, ∅, l 1 ) means that location l 1 is reached from location l 1 if the Write action occurs when the clock x is greater than or equal to 2, with no clock to reset; and (l 2 , , LockOff, {x}, l 1 ), means that l 1 is reached from l 2 when the LockOff action occurs, resetting clock x while taking the transition.

Description of the approach

The strategy of GREP is based on the enforcement approach proposed in [START_REF] Renard | Optimal enforcement of (timed) properties with uncontrollable events[END_REF][START_REF] Renard | Runtime enforcement using Büchi games[END_REF]. As shown in Fig. 1, an EM may be seen as a function from timed words to timed words, with the ability to delay some controllable actions using a memory, but with no possibility to act on uncontrollable actions. This mechanism should ensure the correctness of the output sequence (soundness), that the order of controllable actions is preserved and that uncontrollable actions are immediately released (compliance), and that the output is maximal (optimality). All these definitions, as well as the proofs of correctness and details of the EM generation, at two levels of abstraction (functional and operational), are provided in [START_REF] Renard | Optimal enforcement of (timed) properties with uncontrollable events[END_REF]. Notice that unlike the approach in [START_REF] Pinisetty | Runtime enforcement of timed properties[END_REF], there could be some situations where the property may not be enforceable, since uncontrollable actions cannot be retained.

Let us provide the intuition of the approach on an example. Consider the required property ϕ t given in Fig. 2, and the input sequence 1 gives the evolution of the system at different time instants, providing the output of the EM at a given date, its complete expected output if no other event is received (the output at an infinite date), and the state of the memory (the stored controllable actions) at an infinite date. At t = 1 and t = 2 respectively, Auth and LockOn actions are received. Since they are uncontrollable actions, they are released immediately. At t = 4, action Write is received. Since it is controllable and in order to avoid to reach a bad state, it is stored in the memory. At t = 5, the uncontrollable action LockOff is received and immediately released. Now it is possible to emit the stored Write action, but only after 2 time units. For this reason, (2, Write) is added at the end of σ s meaning that Write should be emitted in 2 time units, and it is removed from σ c . At t = 6, another uncontrollable LockOn action is received and immediately released. At this step, it is not possible to emit Write anymore, then it is removed from the end of σ s and put back at the beginning of σ c . At t = 7, another controllable Write action is received and stored (added at the end of σ c ). At t = 8, the last uncontrollable LockOff action is received, allowing to emit the two Write actions after 2 time units. Thus, they are placed at the end of σ s and removed from σ c . Since no other action is received afterwards, the two Write actions are released at t = 10.

(1, Auth) (1, LockOn) (2, Write) (1, LockOff) (1, LockOn) (1, Write) (1, LockOff). Table

Games

In order to improve the computation time of the EM at runtime, it is possible to precompute the behaviour of the EM ahead of the execution and storing it. For this purpose, we use game theory. GREP builds a two-player game graph representing the possible actions of the EM and the system under scrutiny (that acts as the environment). Each vertex of the graph belongs to one of these two players, and each edge represents a possible action of the player that owns the source vertex. GREP then solves a Büchi game by computing a set of nodes of the graph from which there exists a winning strategy. More details may be found in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF]. Using this approach allows us to avoid the exploration of the whole execution tree at runtime. More precisely, GREP proceeds in three steps: first, it computes a symbolic graph, which is a finite abstraction of the (infinite) semantics of the TA; then it computes the game graph and the winning strategy for the EM; finally the EM follows the strategy to enforce the property.

(1, Auth) (1, LockOn) (2, Write) (1, LockOff) (1, LockOn) (1, Write) (1, LockOff) over time. t Output Complete Expected Output Buffer 1 (1, Auth) (1, Auth) 2 (1, Auth) (1, LockOn) (1, Auth) (1, LockOn) 4 (1, Auth) (1, LockOn) (1, Auth) (1, LockOn) Write 5 (1, Auth) (1, LockOn) (3, LockOff) (1, Auth) (1, LockOn) (3, LockOff) (2, Write) 6 (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) Write 7 (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) Write Write 8 (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) (2, LockOff) (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) (2, LockOff) (2, Write) (0, Write) 10 (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) (2, LockOff) (2, Write) (0, Write) (1, Auth) (1, LockOn) (3, LockOff) (1, LockOn) (2, LockOff) (2, Write) (0, Write)
The symbolic graph abstracting the semantics of the TA is similar to the usual zone graph used to compute reachability on TAs (see for example [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF]), except that the successor relation is more constraining. In the usual zone graph, it is only required that a state in a vertex (vertices can be seen as sets of states of the semantics of the TA that share the same location) can reach a state in the successor vertex, whereas for our purpose it is required that all the states in a vertex can reach a state in the successor vertex. This holds for delay transitions (transitions representing elapse of time) and action transitions (representing a transition in the TA) which are built in the same way. We also require that each vertex has at most only one time successor (i.e. a node reached by letting time elapse, as opposed to nodes reached by outputting events (action successors)). An algorithm to compute such a graph is given in [START_REF] Alur | Minimization of timed transition systems[END_REF], for example.

The game graph is then built upon this symbolic abstraction graph. Each vertex of the symbolic abstraction graph is duplicated, one of the resulting vertices belongs to player 0 (the EM), and the other to player 1 (the environment). Each of these vertices is then associated with words taken from a finite, prefix-closed set of controllable words, each vertex being duplicated again for every word from this set. This set of controllable words is computed to ensure that the strategy is always the best one (the one outputting the maximal word) using only these vertices. For a formal description of this set in case of untimed properties, see [START_REF] Renard | Runtime enforcement using Büchi games[END_REF]. The edges of the game graph represent the actions of the player: an edge leaving a node belonging to player 0 represents either the emission of the first event of the associated word (which represents the stored controllable actions), leading to a vertex belonging to player 0 again, since an EM can output multiple events at the same time, or to the same node which belongs to player 1, meaning that the EM decides not to emit for the moment and lets the environment play. An edge leaving a vertex belonging to player 1 leads to a vertex belonging to player 0, and represents either the reception of an uncontrollable event (changing the symbolic state to an action successor), the reception of a controllable event (changing the associated word), or the elapse of time (changing the symbolic state to the time successor). Nodes that are their own time successor (i.e. that contain all the valuations reached by letting time elapse) have their corresponding edge replaced by an edge leading to the same vertex which belongs to player 0. This corresponds to receiving no more event, thus allowing us to consider finite inputs, but with infinite plays over the graph (since there will be a loop between a node belonging to player 0 where the EM will decide not to emit anything, and the environment not receiving any event and being stable by elapse of time). A formal definition of the game graph for untimed properties can be found in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF] too. GREP builds a game graph which is similar, except that some nodes have time successors.

After having constructed the game graph, GREP computes the winning set of nodes of the Büchi game with Büchi nodes (the nodes to be always reachable) defined as all the vertices of the game graph whose symbolic location of a vertex is an accepting location of the TA for player 0.

Then, GREP can follow a real execution on the game graph, by watching the node that has been reached so far by its output, and the nodes that can be reached by emitting stored controllable actions (i.e. following the corresponding edges in the game graph). Whenever a winning node is reached by player 0, the strategy is to emit as many events as possible, remaining in a winning node all the time. Since the winning nodes are winning a Büchi game, it is always possible for player 0 to stay in a winning node whenever one is reached. Whenever a winning node is reached, the output of the EM is then guaranteed to satisfy the property.

An example of game graph associated with property ϕ t given in Fig. 2 is provided in Fig. 3. In this graph, nodes are labelled with a tuple (l, z, w, p), where l is the location of the TA associated with the node, z is the zone (set of clock constraints), w is the word of controllable actions as described previously, and p is the player: 0 for the enforcement mechanism, and 1 for the environment. The square node is the initial node, the blue (rectangular) ones are the winning nodes, and the nodes that are double-circled are the nodes whose locations are accepting. Note that in our example, all the accepting nodes (double-circled) are winning (blue, rectangular). The edges have different colours and heads, depending on their role: green edges (filled triangular heads) correspond to the enforcer emitting its first stored controllable action, blue ones (empty triangular heads) to the enforcer not emitting (thus letting the environment play), red (filled diamond heads) and orange (empty diamond heads) edges correspond to the reception of an uncontrollable event and a controllable one, respectively, and purple ("vee" heads) edges represent the elapse of time (they lead to the time successor).

General Description of GREP

GREP is a tool of about 6,000 lines of code 3 developed using the C language, available at https://github.com/matthieurenard/GREP. GREP is essentially composed of 2 modules (cf Fig. 4): Symbolic Computing Module (SCM) and Enforcement Monitor Module (EMM). It loads a TA file describing the desired property, and reads the inputs directly from stdin. The output of the EM is sent to stdout. This approach allows one to use GREP with off-the-shelf applications. The Symbolic Computing Module is composed of three main components: a TA loader, the zone graph generator, and the game graph generator.

TA Loader

The TA loader is the component that parses a file containing the description of a timed automaton and loads it into a C structure. The file of the automaton is a textual description following a grammar designed for this purpose. The automaton must be also deterministic and complete (see [START_REF] Alur | The theory of timed automata[END_REF]). If the automaton is not deterministic, the behaviour is undefined. Once the timed automaton is loaded, a symbolic graph is computed by the Zone Graph Generator to abstract its infinite semantics into a finite graph.

Zone Graph Generator From the timed automaton, a symbolic graph is constructed using zones. Compared to a classical zone graph (used to compute reachability), this symbolic graph satisfies additional constraints. (A zone graph usually requires that, between a node and its successor, there exists a state of the semantics of the timed automaton in the first node that leads to a state in its successor). In this symbolic graph, all states in a node must lead to the successor. An algorithm to compute this symbolic graph satisfying these constraints is given in [START_REF] Alur | Minimization of timed transition systems[END_REF]. This algorithm has been implemented to compute the symbolic graph in this module. In GREP, zones are represented by Difference Bound Matrices (DBMs), using the UPPAAL DBM library (udbm, [START_REF]Uppaal DBM Library[END_REF]), and its C API. The algorithm requires some functionality that is not provided by this C API (some of them exist in some higher-level wrappers), such as complementing zones into a list of zones. This functionality was added to our own wrapper of udbm. No other third-party library was needed to compute the symbolic graph. This symbolic graph is used to build the final game graph, that will be used by the enforcement monitor.

Game Graph Generator Using the symbolic graph, the Game Graph Generator builds a graph over which to play a Büchi game whose strategy is the one to be followed by the enforcement monitor. The graph is constructed as described in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF], adding some edges to represent the elapse of time (that changes zones). Once the graph is constructed, the Büchi game is solved for player 0 (the enforcement monitor), with the set of Büchi nodes being the set of nodes whose location is accepting. The winning nodes are the nodes from which the enforcement monitor ensures that its output will satisfy the property. Following a path of winning nodes in the graph gives a strategy to follow such that the final output satisfies the property. This is how the EM uses the graph to actually enforce the property.

Enforcement Monitor Module (EMM)

The EMM module uses SCM to compute the output for a given input. It has five main public functions: init(G), getStrat(), delay(t), eventRcvd(e), and emit(). Function init(G) initialises the EMM following the strategy from graph G. Function getStrat() gives the strategy to follow, i.e. whether the first action of the buffer should be output or not. Since time is abstracted by the zone graph for the SCM, the SCM needs to be notified that some time has passed, which is done by the use of function delay(t), where t is the number of time units that have elapsed since the last call to delay, or the creation of the enforcement mechanism for the first call. Time units only need to be consistent with the ones used in the property. Function eventRcvd(e) is used to inform the EMM that an event e has been read from the input. In this case, the EMM acts differently depending on the controllability of the event. Function emit() is used to output the first action of the buffer (uncontrollable events are output by function eventRcvd(), as required by compliance).

Note that these functions allow to use the EMM in both online (real-time) and offline (with a trace as input) settings. All these functions, except function getStrat(), return the number of time units required to reach the time successor of the current node (∞ if there is no time successor). It is the number of time units given to function delay() if no event is received before and the strategy is not to emit.

Thus, the general algorithm to use the EMM in the offline setting is given in Algorithm 1. Basically, the EMM follows a path in the game graph. Thus, it considers the current node as the node reached by its output, and explores the strategy tree from this node. The EMM also stores the controllable actions that have not been output yet, and uses them to compute the possible output. Since the output should be the longest possible, with minimal possible delays, computing the strategy requires to explore the tree of all possible strategies. This is done by exploring the game graph, simulating the emission of the controllable actions of the buffer at all possible time instants. In each node belonging to player 0, if the successor by emitting (green, empty triangular head input : The game graph G, the input sequence of events, through function read () output: The output of the enforcer mechanism, through function emit() Algorithm 1: Main algorithm to enforce a property in offline mode arrow in the game graph) is winning, then it is explored, and if the time successor is also winning, it is explored as well, since waiting before emitting could allow the EMM to output more events. Each node is then associated with a score, corresponding to the number of actions that have been emitted to reach the node. Then, the EMM stores the node that has the biggest score, and the strategy to follow to reach it. If two nodes have the same score, then the lowest common ancestor is computed, and the one node that can be reached by emitting from this ancestor (the other node can be reached from this ancestor by waiting) is kept as the node to reach (this corresponds to computing the lexicographical order). This process is repeated for each node with the same score, with the previous stored node, such that in the end the stored node is the minimal node (for the lexicographic order) of all the nodes with the highest score.

1 init(G); 2 del ← ∞;
Note that computing an output such that all actions are emitted whenever it is possible to emit them does not require to explore the strategy tree. Depending on the property, the two outputs could be the same (i.e. if the property is such that letting time elapse never enables a transition that eventually allows the EMM to output more events), thus the EMM can work faster by using an optimisation that does not compute any tree, but outputs actions whenever possible (i.e. when the successor node by emitting is winning) if it is specified to do so.

User Interface

GREP is shipped with two executables: one to use the enforcement mechanism in offline mode, and the other in the online mode. Both of them take their input on the standard input. In the offline mode, the input is composed of events in the form (t, a), where t is a date and a is an action, controllable or uncontrollable. In the online mode, only the action is given, the date is computed from the real time through a call to gettimeofday(). Note that these executables may build only on UNIX-like systems because of some system calls such as gettimeofday() and clock_gettime(). Excepting this, the tool is not system-dependent. The output (events with their dates) is printed on the standard output. Several options may be used:

-One of the two options -a <automatonFile> or -g <graphFile> must be passed to specify the property. The file <automatonFile> should be in the same format as the file shown in appendix A. The file <graphFile> should be a file saved by this executable (see option -s), loading this kind of file should be faster than loading an automaton file since it contains the graph, which does not need to be computed again. --s <graphFile> saves the game graph in <graphFile>, to be loaded in another execution (see option -g). --z <zoneGraphFile> draws the zone graph using graphviz and store it (as PDF) in <zoneGraphFile>. --d <gameGraphFile> draws the game graph using graphviz and store it (as PDF) in <gameGraphFile>. --t <timeFile> logs times between the reception of two events in the file <timeFile>. This option is used to benchmark the program. --l <logFile> prints all the logs in <logFile>.

--f (fast) use the optimised version, where actions are output whenever they can be instead of outputting the longest word possible with minimal dates.

If options -s, -z, -d, or -t are not given, then the corresponding action will just not happen. For example, without -z, the zone graph will not be saved. If none of the options among -a and -g is given, the program will print an error and abort. If both are given, then the automaton file is used. If option -l is not given, then the standard error is used as log file, which is not recommended (we recommend always using the option -l). If the option -f is not given, then the enforcement mechanism will output as many events as possible, with the lowest possible dates; enabling the option will make it output actions if it is possible to output them (i.e. if the node of the game graph reached by outputting is winning). Using option -f is usually faster, but the outputs might differ depending on the property. Example usage: game_enf_offline -a phiext.tmtn -l log \ -d gameGraph.pdf < input will enforce the property described in the file phiext.tmtn, logging in the file log, reading its events from the file input. It will also draw the game graph in the file gameGraph.pdf.

The enforcement mechanism logs the mode in which it runs (default or fast) at the beginning, and when it stops, it logs the input, its output, the controllable actions that have not been output (what remains in its buffer), and a verdict that is WIN if its output satisfies the property, or LOSS otherwise (some properties might not be enforced as explained in [START_REF] Renard | Enforcement of (timed) properties with uncontrollable events[END_REF]).

E n f o r c e r i n i t i a l i z e d i n d e f a u l t mode . S h u t t i n g down t h e e n f o r c e r . . . Summary o f t h e e x e c u t i o n : I n p u t : ( 0 , W r i t e ) ( Listing 1.1: Example log file produced by GREP For example, considering that phiext.tmtn is the file given in appendix A, the previous command with the input file containing the sequence:

(0, Write) (1, Auth) (2, Write) (3, LockOn) (4, Write) (5, LockOff) (6, LockOn) (7, LockOff), produces the output: (1, Auth) (2, Write) (2, Write) (3, LockOn) (5, LockOff) (6, LockOn) (7, LockOff) (9, Write).
The produced log file is given in Listing 1.1.

Performance Evaluation

The performance of GREP has been evaluated on three properties that come along with TiPEX, the tool to which we compare. TiPEX (see [START_REF] Pinisetty | TiPEX: A Tool Chain for Timed Property Enforcement During eXecution[END_REF]) is, to our knowledge, the only other tool that acts as an enforcement mechanism for timed regular properties. These properties are described in Fig. 5. The safety property states that there should always be 5 time units between two r actions. The co-safety property states that the first r action should be followed by a g action, with a delay of at least 6 time units. The response property states that every grant (g) action should be followed by a release (r) action within 15 to 20 time units, without any grant action occurring between them.

For each of these properties, GREP has been run 100 times on every input among 100 inputs of 1000 events randomly generated. The time between the reception of two events has been saved for all of these executions. The same times have been computed for TiPEX 4 , reducing the number of inputs and iterations to have the benchmarks run in a reasonable amount of time. Figures 6 and7 give a graphical visualisation of the performances of GREP and TiPEX.

Figures 6 and7 are obtained as follows: each input is iterated several times (100 for GREP, less for TiPEX), and the computation times of the tool between the reads of two consecutive events of the input are stored. Then, the median time is computed for each of these times between all the iterations. We then plot the logarithm (in base 10) of these times against the reads of the events. We use a logarithmic scale in nanoseconds because many values are low, and they would be merged in a line when using a linear scale. The results for GREP with option -f are given only for the safety property because they are similar to the results without the option for the two other properties. We can see that GREP is faster than TiPEX by several orders of magnitude. GREP outputs many events in less than 10 µs (4 on the graphs), whereas TiPEX takes at least 1 ms (6 on the graph) to output them. For the safety property, we can see that for some inputs, GREP takes an increasing amount of time to compute the strategy. This is due to the exploration of the strategy tree, which grows with the number of stored controllable actions. Using the optimised setting (-f) allows GREP to compute its output faster, as shown in Fig. 6b. The last vertical line has also many high values, because it represents the time to emit all the remaining actions after the last event from the input was read. For the co-safety and response properties, GREP is less variable than for the safety property, mainly because its strategy is simpler: it consists in either emitting everything in the co-safety (once state s 3 is reached) or emitting nothing for the response property, if the first stored controllable is an r while in state s 1 . TiPEX, on the other hand, takes a linearly-increasing amount of time to emit some events.

Discussion and Concluding Remarks

As shown in Section 3, GREP provides better computing times than TiPEX. There are several factors that can explain this. The implementation language is one of these factors: GREP is implemented in C, which produces assembly code that is fast to execute, whereas TiPEX is implemented in Python, which is a higher-level language that can introduce some overhead in the execution time. Another factor is the use of games to enforce the properties, that allows the EMM to compute the output faster. Indeed, the game graph allows us to know if a node is winning in very little time, where the same computation not using graph needs to consider all the reachable states with the buffer.

Note that our tool was designed primarily to handle uncontrollable events. The properties used in our evaluation/comparison do not feature uncontrollable events because TiPEX only supports controllable events. To our knowledge, there is no other tool that

3Fig. 3 :

 3 Fig. 3: Game graph associated with property ϕ t

Fig. 4 :

 4 Fig. 4: General architecture of GREP

3 while 5 while del ≤ δ do 6 δ 13 del 17 emit

 3561317 The input sequence has not been read entirely do 4 (δ, a) ← read(); ← δ -del; 7 del ← delay(del); ← eventRcvd(a); 14 end 15 while del < ∞ or getStrat() = EMIT do 16 while getStrat() = EMIT do

Fig. 5 :

 5 Fig. 5: Properties used to benchmark GREP

Table 1 :

 1 Table showing the evolution of the enforcement mechanism with input

We patched TiPEX to retrieve the times as we do in our tool, only modifying it to get times properly, and did not change the behaviour inside the part that is being measured.

(b) GREP fast -safety 0 200 400 600 800 1000 6.4 6.5 6.6 6.7 6.8 6.9 7.0 (c) TiPEX -safety Fig. 6: Comparison of timings of GREP and TiPEX on the safety property. "GREP fast" means that option -f is used. The x axis corresponds to the events of the input (from 1 to 1000), and the y axis corresponds to the logarithm of the timings (in nanoseconds) between the reads of the events. acts as an enforcement mechanism for timed properties with uncontrollable events. We initially used games to precompute (with the game graph) the behaviour of the enforcement mechanism upon the reception of uncontrollable events, but it has also improved the computation time of the output even without any uncontrollable event.

Depending on the property, there could be an exponential blow-up in the number of nodes that have to be visited. The -f option allows the enforcement mechanism to use a strategy (where each event is output as soon as possible) that prevents this blowup. To further improve the performance of GREP and avoid the blow-up when using the strategy outputting the longest words, we aim at i) computing a better set of controllable words to be associated with nodes, and having a better representation of controllable words. A (more theoretical) possible extension to this work is to determine under which conditions the two strategies (using the optimised version or not) are equivalent. (d) TiPEX -response Fig. 7: Timings of GREP and TiPEX on the response and co-safety properties. The x axis corresponds to the events of the input (from 1 to 1000), and the y axis corresponds to the logarithm of the timings (in nanoseconds) between the reads of the events.

A Automaton File

The automaton file describing ϕ t (see Fig. 2) follows: l 0 ->{Auth }{}{} l 1 ; l 0 ->{ W r i t e }{}{} l 3 ; l 0 ->{LockOn }{}{} l 3 ; l 0 ->{LockOff }{}{} l 3 ; l 1 ->{LockOn }{}{} l 2 ; l 1 ->{ W r i t e }{}{ x >= 2} l 1 ; l 1 ->{LockOff }{ x }{} l 1 ; l 1 ->{Auth }{}{} l 1 ; l 1 ->{ W r i t e }{}{ x < 2} l 3 ; l 2 ->{Auth }{}{} l 2 ; l 2 ->{LockOn }{}{} l 2 ; l 2 ->{LockOff }{ x }{} l 1 ; l 2 ->{ W r i t e }{}{} l 3 ; l 3 ->{ W r i t e }{}{} l 3 ; l 3 ->{Auth }{}{} l 3 ; l 3 ->{LockOn }{}{} l 3 ; l 3 ->{LockOff }{}{} l 3 ; } }


Omer Nguena Timo

Alexandre Petrenko
email: petrenko@crim.ca

S Ramesh
email: ramesh.s@gm.com

Omer Nguena Timo
email: omer.nguena-timo@crim.ca

Multiple Mutation Testing from Finite State Machines with Symbolic Inputs

Keywords: Extended FSM, Symbolic inputs, Conformance testing, Mutation testing Fault modelling, Fault model-based test generation, Constraint solving

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

Introduction

Detecting nonconforming implementations is a major challenge during the design and the maintenance of systems, which motivates the elaboration of innovative and efficient testing [START_REF] Pȃsȃreanu | A survey of new trends in symbolic execution for software testing and analysis[END_REF][START_REF] Utting | A taxonomy of model-based testing approaches[END_REF], model-checking [START_REF] Kroening | A survey of automated techniques for formal software verification[END_REF] and runtime verification techniques [START_REF] Leucker | A brief account of runtime verification[END_REF]. Testing techniques [START_REF] Utting | A taxonomy of model-based testing approaches[END_REF] not only aim at exercising a system with adequate test cases to reveal failures and ideally to identify and to repair faults causing the failures. They may also target evaluating the adequacy of test cases and the generation of test cases to cover artefacts that can conceal faults [START_REF] Demillo | Hints on test data selection: Help for the practicing programmer[END_REF][START_REF] Jia | An analysis and survey of the development of mutation testing[END_REF][START_REF] Delamaro | Interface mutation test adequacy criterion: An empirical evaluation[END_REF][START_REF] Bessayah | A fault injection tool for testing web services composition[END_REF], e.g., statements, branches, interfaces, requirements, mutants. Mutants which are versions of a specification of a system seeded with undesired faults can be used to generate test cases or to determine the adequacy of given test cases to reveal the faults. A fault domain can be specified with a set of mutants and test cases detecting the mutants which do not conform to the specification can be applied to detect faulty implementations of a system. Classical FSM model is often used in developing fault model based testing approaches for detecting nonconforming implementations. Recently we proposed an approach for this model to evaluate the adequacy of test cases in a given fault domain [START_REF] Petrenko | Multiple mutation testing from fsm[END_REF] and to generate test cases detecting all nonconforming mutants [START_REF] Petrenko | Test generation by constraint solving and fsm mutant killing[END_REF].

In case the testers need to deal with inputs with infinite domains, the finite input alphabets which is used in classical FSM to represent the inputs of a system becomes ineffective along with FSM-based testing approaches. In the automotive applications, the behaviors of some controllers [START_REF] Petrenko | A method and tool for test optimization for automotive controllers[END_REF] depend on the truth values of predicates defined over input variables with infinite domains. Extensions of FSMs with symbolic inputs and arithmetic operations on variables have been proposed [START_REF] Cheng | Automatic functional test generation using the extended finite state machine model[END_REF][START_REF] Petrenko | Checking experiments for finite state machines with symbolic inputs[END_REF][START_REF] Nguena Timo | Conformance testing of variable driven automata[END_REF] to relax limitations of the classical FSM and used in developing testing methods [START_REF] El-Fakih | Distinguishing extended finite state machine configurations using predicate abstraction[END_REF][START_REF] Petrenko | Checking experiments for finite state machines with symbolic inputs[END_REF][START_REF] Nguena Timo | Conformance testing of variable driven automata[END_REF]. Following the same trend, our test generation method by constraint solving from FSM in [START_REF] Petrenko | Multiple mutation testing from fsm[END_REF][START_REF] Petrenko | Test generation by constraint solving and fsm mutant killing[END_REF] could be enhanced to extended FSM. The work of [START_REF] El-Fakih | Extended finite state machine based test derivation driven by user defined faults[END_REF] also uses an EFSM model and a mutation machine to model transition and output faults. Test generation requires (partial) unfolding of the specification, which we completely avoid. A test suite complete for used defined faults can only be generated if they satisfy certain sufficient conditions, which severely restrict types of detectable transition and output faults. Moreover, faults in transition predicates are not considered, as opposed to our approach.

In this paper, we lift the mutation testing approach from classical FSM in [START_REF] Petrenko | Multiple mutation testing from fsm[END_REF][START_REF] Petrenko | Test generation by constraint solving and fsm mutant killing[END_REF] to symbolic input finite state machine (SIFSM). SIFSM [START_REF] Petrenko | Checking experiments for finite state machines with symbolic inputs[END_REF] is an extension of FSM with inputs specified with predicates on input variables possibly having infinite domains, which permits a more compact representation of data, data-flow relations and control-flow for determining outputs depending on the values of the predicates and states. Examples of realistic systems which can be specified with SIFSM can be found in [START_REF] Petrenko | A method and tool for test optimization for automotive controllers[END_REF][START_REF] Huang | Exhaustive model-based equivalence class testing[END_REF]. The contribution is three-fold. First, we define mutation operations for building well-formed mutation machines specifying mutants in fault domains. New mutation operations may change predicates used in the specification or introduce new predicates. Secondly, we propose a method for evaluating the completeness of a test suite, i.e., the adequacy of a test suite to detect all nonconforming mutants. Finally we propose a method for generating complete test suites. Following the ideas in our previous work [START_REF] Petrenko | Multiple mutation testing from fsm[END_REF][START_REF] Petrenko | Test generation by constraint solving and fsm mutant killing[END_REF], the methods rely on building and resolving constraints specifying the mutants undetected by given test cases. However, in this work the constraints differ from those in our previous work; they are represented with Boolean expressions for expressing both undetected mutants and the input-completeness property of the mutants. The latter property is formalized with a notion of cluster for state. This is needed because predicates cannot be mutated independently. We evaluate the methods with a prototype tool applied to a SIFSM model of a component from the automotive domain.

The remaining of the paper is organized as follows. Section 2 introduces mutation SIFSM and mutation operations used for its creation. In Section 3 we present an approach for determining the mutants undetected by a test, which leads to a method for completeness checking of a given test suite in Section 4. In Section 5 we develop a method for complete test suite generation. Section 6 reports some experimental evaluation of the approach. We summarize our contributions in Section 7.

Background

Preliminaries

Let G denote the universe of inputs that are predicates over variables in a fixed set V for which a decision theory, e.g., an SMT solver, exists, excluding the predicates that are always false. G * denotes the universe of input sequences and ε denotes the empty sequence. Later in the paper, a test is just an input sequence. Let I V denote the set of all the valuations of the input variables in the set V , called concrete inputs. A set of concrete inputs is called a symbolic input; both, concrete and symbolic inputs are represented by predicates in G. Henceforth, we use set-theoretical operations on inputs. In particular, we say that concrete input x satisfies symbolic input g if x ∈ g. We also have that

I V ⊆ G. A set of inputs H is a tautology if each concrete input x ∈ I V satisfies at least one input in it, i.e., {x ∈ g | g ∈ H} = I V .
We define some relations between input sequences in G * . Given two input sequences α, β ∈ G * of the same length k, α = g 1 g 2 . . . g k , β = g 1 g 2 . . . g k , we let α ∩ β = g 1 ∩ g 1 . . . g k ∩ g k denote the sequence of intersections of inputs in sequences α and β; α and β are compatible, if for all i = 1, . . . , k, g i ∩ g i = ∅. We say that α is a reduction of β, denoted α ⊆ β, if α = α ∩ β. If α is a sequence of concrete inputs as well as a reduction of β then it is called an instance of β; given a finite set of input sequences E ⊆ G * , a set of concrete input sequences is called an instance of the set E, if it contains at least one instance for each input sequence in E.

Given a finite set of outputs O, a trace is a sequence of input-output pairs in (G × O) * . A trace is concrete if every input in it is concrete; otherwise it is symbolic. Given a trace β ∈ (G × O) * , the input (resp. output) projection of β, denoted β ↓G (resp. β ↓O ), is a sequence obtained from β by erasing symbols in O (resp. G).

We consider an extension of FSM called symbolic input finite state machine (SIFSM) [START_REF] Petrenko | Checking experiments for finite state machines with symbolic inputs[END_REF], which operates in discrete time as a synchronous machine reading values of input variables and setting up the values of output variables. Output variables are assumed to have a finite number of valuations and form a finite output alphabet. On the other hand, the set of input valuations can be infinite. Definition 1. A symbolic input finite state machine S (or machine, for short) is a 5tuple (S, s 0 , V, O, T ), where -S is a finite set of states with the initial state s 0 , -V is a finite set of input variables over which inputs in G are defined, -O is a finite set of outputs,

-T ⊆ S × G × O × S is a finite transition relation, (s, g, o, s ) ∈ T is a transition.
The semantics of SIFSM is defined by a Mealy state machine with a possibly infinite input set, where the state and output sets remain finite. The set of transitions outgoing from state s is denoted by T (s). We say that input g is defined in state s if g is the input of a transition in T (s). Then, G(s) denotes the sets of all the inputs defined in s. We say that transition (s, g, o, s ) is triggered by input g if g is a reduction of g. Several transitions in T (s) are nondeterministic if they can be triggered by the same input. If a set of transitions T (s) includes nondeterministic transitions, the set is said to be nondeterministic; otherwise it is deterministic.

An execution of S from state s is a sequence of transitions t 1 t 2 . . . t n forming a path from s in the state transition diagram of S. A deterministic execution is an execution such that its set of transitions is deterministic; otherwise, i.e., if for some state s and some transition in the execution there exists another transition such that both transitions belong to T (s) and are triggered by an identical input, the execution is nondeterministic.

A symbolic trace of S in state s is the projection of an execution from s on the inputoutput pairs in (G × O). A trace obtained from a symbolic trace in s by substituting every inputs by an instance of it is called a concrete trace of S in s. Let Tr S (s) (resp. STr S (s)) denote the set of all concrete (resp. symbolic) traces of S in state s and Tr S (resp. STr S ) denote the set of concrete (resp. symbolic) traces of S in the initial state.

We say that an input sequence triggers an execution of S (in state s) if it is a reduction of the input projection of a trace of the execution of S (in state s). Given an input sequence α, let out S (s, α) denote the set of all output sequences which can be produced by S in response to α at state s, that is out S (s, α) = {β ↓O | β ∈ STr S (s) and α ⊆ β ↓G }. We observe that out S (s, α) = out S (s, γ) whenever γ is a reduction of input α.

The machine S is deterministic (DSIFSM), if for every state s, T (s) is deterministic; otherwise S is a nondeterministic SIFSM (NSIFSM). Clearly, a DSIFSM has only deterministic executions, while an NSIFSM can have both. State s of S is completely specified, if G(s) is a tautology, i.e., each concrete input x ∈ I V satisfies at least one input defined at s. The machine S is completely specified, if each state is completely specified. The machine S is initially connected, if for any state s ∈ S there exists an execution from s 0 to s. Henceforth, we assume that all SIFSM are initially connected and completely specified.

We adapt several relations introduced in [START_REF] Petrenko | Multiple mutation testing from fsm[END_REF][START_REF] Petrenko | Test generation by constraint solving and fsm mutant killing[END_REF] for FSM to SIFSM and use tracebased definitions of the relations introduced in [START_REF] Petrenko | Checking experiments for finite state machines with symbolic inputs[END_REF]

]. Given states s 1 , s 2 of a SIFSM S = (S, s 0 , V, O, T ), s 1 and s 2 are (trace-) equivalent, s 1 s 2 , if Tr S (s 1 ) = Tr S (s 2 ); s 1 and s 2 are distinguishable, s 1 s 2 , if Tr S (s 1 ) = Tr S (s 2 ); s 2 is trace-included into (is a reduction of) s 1 , s 2 ≤ s 1 , if Tr S (s 2 ) ⊆ Tr S (s 1 )
. S is reduced if any pair of its states is distinguishable. Given two distinguishable states s 1 and s 2 , there exists a sequence α ∈ G * such that out S (s 1 , α) = out S (s 2 , α); α is called a distinguishing input sequence for states s 1 and s 2 , this is denoted s 1 α s 2 .

We also use relations between machines. Given SIFSM S = (S, s 0 , V, O, T ) and P = (P, p 0 , V, O, N ), P ≤ S if p 0 ≤ s 0 ; P S if p 0 s 0 ; P α S if p 0 α s 0 with α ∈ G * ; and P S if P α S for some distinguishing input sequence α for p 0 and s 0 . Later, we use equivalence relation between machines as a conformance relation between implementation and specification machines.

Given a NSIFSM S = (S, s 0 , V, O, T ), a machine P = (P, p 0 , V, O, N ) is a submachine of S if p 0 = s 0 , P ⊆ S and N ⊆ T .

Mutation machine

Let S = (S, s 0 , V, O, N ) be a DSIFSM, called the specification machine.

Definition 2. A NSIFSM M = (S, s 0 , V, O, T ) is a mutation machine of S, if S is a submachine of M.
Transitions of M that are also transitions of S are called unaltered, while the others, in the set T \N , are mutated transitions. A transition of M is suspicious if it belongs to a nondeterministic set of transitions, let Susp(s) denote the set of all suspicious transitions in state s and Susp(M) denote the set of all suspicious transitions of M. An unaltered transition is trusted if it is not suspicious; otherwise it is untrusted and belongs to the set Untr(S) = Susp(M) ∩ N . Given state s, a subset of T (s) is called a cluster of s if

1 2 3 4 v 1 v 3 (1) /0 v 1 ∨ v 3 (2) /0 v 1 v 2 (4) /0 v 1 ∨ v 2 (3) /0 v 2 ∨ v 3 (9) /0 v 2 v 3 ( 5 ) / 0 v 2 ∨ v 3 [8] /1 v 1 v 2 v 3 [7] /0 v 1 v 2 v 3 [6] /0 v 1 v 2 (13) /0 v 1 ∨ v 2 ( 1 0 ) / 1 (v 1 ∨ v 2 )v 3 [11] /1 (v 1 ∨ v 2 )v 3 [12] /1
Fig. 1: A mutation SIFSM, state 1 is initial.

it is deterministic and the inputs of its transitions constitute a tautology, in other words, the transitions of the cluster have a complete system of guards so that each concrete input enables a transition. Let Z(s) denote the set of all clusters of s. State s is said to be suspicious if |Z(s)| > 1. We use S susp to denote the set of all suspicious states of M.

In a mutation machine, untrusted transitions can be seen as the result of applying mutation operations transforming the specification into mutants. Mutation operations may also be considered as fault seeding in the specification. For an untrusted transition to belong to a mutant, it must participate in clusters. We say that a mutation machine is well-formed if each of its suspicious transitions belongs to a cluster. In what follows, we consider only well-formed mutation machines.

We assume that only completely specified deterministic submachines of M are possible implementation machines for the specification machine S. The set of all such submachines is called a fault domain for S, denoted Sub(M). If M is deterministic then Sub(M) contains just S. Since each implementation machine in Sub(M) is deterministic, each state of an implementation machine has only one cluster. The size of Sub(M) is the product of the sizes of the clusters of the states, i.e., |Sub(M)| = s∈S |Z(s)|. A DSIFSM P ∈ Sub(M), such that P = S, is called a mutant. Each mutant P has all the trusted transitions of M and the set of suspicious transitions Susp(P). It holds that for all P, P ∈ Sub(M), if P = P then Susp(P) = Susp(P ).

Fig. 1 presents an example of an NSIFSM which is a well-formed mutation machine with three Boolean input variables v 1 , v 2 and v 3 and two outputs in {0, 1}. The mutation machine has five mutated transitions depicted with dashed lines. The solid lines represent the unaltered transitions of the specification machine. Identifiers of transitions are presented in brackets and parentheses for mutated and unaltered transition, respectively. There are eight suspicious transitions t Let e be an execution of M and Susp(e) denote the set of suspicious transitions in e. We say that a (possibly nondeterministic or partially specified) submachine P is involved in e if Susp(e) ⊆ Susp(P). An execution of any submachine of M is an execution of M, but only deterministic executions of M are executions of submachines in Sub(M). P ∈ Sub(M) is the only mutant involved in e if Susp(e) = Susp(P).

Since the specification and mutants are completely specified and deterministic SIFSM, we use equivalence as a conformance relation for testing. A mutant P is nonconforming (faulty) if P S, otherwise, it is called a conforming mutant. We say that a distinguishing input sequence α ∈ G * such that P α S detects or kills the mutant P.

The tuple S, , Sub(M) is a fault model following [START_REF] Petrenko | Multiple mutation testing from fsm[END_REF][START_REF] Petrenko | Test generation by constraint solving and fsm mutant killing[END_REF][START_REF] Petrenko | Checking experiments for finite state machines with symbolic inputs[END_REF]. For a given specification machine S the equivalence partitions the set Sub(M) into conforming implementations and nonconforming ones. In this paper, we do not require the DSIFSM S to be reduced, this implies that a conforming mutant may have fewer states than the specification S; on the other hand, we assume that no fault creates new states in implementations, hence mutants with more states than the specification are not in Sub(M).

Mutation Operations for Building Well-formed Mutation Machines

Mutation operations permit seeding different types of faults including output, transition and other types of faults which cannot be represented with classical FSM. Considering for instance nondeterministic Simulink/Stateflow models, priorities which are automatically assigned to transitions based on the graphical layout may vary upon changes in the layout [START_REF] Scaife | Defining and translating a safe subset of simulink/stateflow into lustre[END_REF]. The variation of the priorities causes transition faults which can be represented with mutated transitions. We consider mutation operations adding mutated transitions to well-formed mutation machines to build new well-formed mutation machines. Every mutated transition introduced by a mutation operation must belong to a cluster of a state. Let M = (S, s 0 , V, O, T ), M = (S, s 0 , V, O, T ) be two well-formed mutation machines, s ∈ S be a state, A ⊆ T (s) be a subset of unaltered transitions from state s in M and B ⊆ T (s) be a subset of mutated transitions from state s in M . We say that M is a mutation of M w.r.t A and B if the following four conditions hold: A ∩ B = ∅, T = T ∪ B, the union of the inputs of the transitions in A is equivalent to the union of the inputs of the transitions in B and there are t ∈ A and t ∈ B having compatible guards but different outputs or target states. We specify a mutation operation with a tuple (M, A, B) such that there exists a mutation of M w.r.t. A and B. The set B can be obtained from the transitions in A by changing target states or outputs, merging/splitting inputs of transitions, replacing variables with default values, swapping occurrences of variables in inputs, substituting a variable for another, modifying arithmetic/logical operations in guards. These operations introduce faults which cannot be represented in classical FSM; some of these faults are considered in [START_REF] Jia | An analysis and survey of the development of mutation testing[END_REF][START_REF] Delamaro | Interface mutation test adequacy criterion: An empirical evaluation[END_REF][START_REF] Bessayah | A fault injection tool for testing web services composition[END_REF]. Any well-formed mutation machine for a specification can be obtained by iterative application of mutation operations on the specification.

Boolean Expressions Specifying Mutants (un)Detected by Tests

Let S, , Sub(M) be a fault model. In the context of testing SIFSM, we consider that a test is just an input sequence. Tests detecting mutants can be determined using a distinguishing automaton obtained by composing the transitions of the specification and mutation machines as follows. A test α ∈ L D triggers several executions in the distinguishing automaton defined by executions of the specification and mutation machine M which are the respective projections of the distinguishing automaton's executions; a deterministic execution of M defining an execution of the distinguishing automaton D to the sink state is called α-revealing if it is triggered by any prefix of the test α. An α-revealing execution may belong to several mutants. As discussed above, given a deterministic execution e of M which has the set of suspicious transitions Susp(e), a mutant P is involved in the execution e, if Susp(e) ⊆ Susp(P). Since an α-revealing execution defines an accepted execution of the distinguishing automaton, each involved mutant is killed. Thus the sets of suspicious transitions in all α-revealing executions represent all the mutants killed by test α; on the other hand, it does not detect mutants which are not involved in these executions. To elaborate a mutant killing test generation procedure we need first to determine all the sets of suspicious transitions of the revealing executions for a given test. Let E α be the finite set of α-revealing executions of M. We use Boolean expressions for encoding of suspicious transitions of executions in E α . A solution of a Boolean expression c over a set of variables is an assignment to True or False of every variable which makes c True. A solution of c can be obtained with solvers [START_REF] Eén | An extensible SAT-solver[END_REF][START_REF] De Moura | Z3: An efficient smt solver[END_REF] which return null in case c has no solution. Given the set of suspicious transitions Susp(M), v1v3 (1) .v1v3 (1) v1 ∨ v2 (3) .v1 ∨ v2 (3) v2 ∨ v3 (9) .v2 ∨ v3 [8] v2v3 (5) .v2v3 (5) v2v3 (5) .v1v2v3 [6] v2v3 (5) .v1v2v3 [7] v1v2 (13) .v2v3 (5) v1v2 (13) .v2 ∨ v3 [8] v1 ∨ v2 (10) .v2 ∨ v3 [8] v1 ∨ v2 (10) .v2v3 (5) v1 ∨ v2 (10) .v1v2v3 [6] v1 ∨ v2 (10) .v2 ∨ v3 [8] v1 ∨ v2 (10) .v1 ∨ v2 (10) v1 ∨ v2 (10) .(v1 ∨ v2)v3 [11] v1 ∨ v2 (10) .(v1 ∨ v2)v3 [12] v1 ∨ v3 (2) .v1 ∨ v2 (10) v1 ∨ v3 (2) .(v1 ∨ v2)v3 [11] v1 ∨ v3 (2) .(v1 ∨ v2)v3 [12] v1v3 (1) .v1 ∨ v2 (10) v1v3 (1) .(v1 ∨ v2)v3 [11] v1 ∨ v3 (2) .v1 ∨ v2 (3) v1v3 (1) .v1 ∨ v2 (3) v1 ∨ v3 (2) .v2 ∨ v3 [8] v1v3 (1) .v2 ∨ v3 [8] v1 ∨ v3 (2) .v2v3 (5) v1 ∨ v3 (2) .v1v2v3 [6] v1v3 (1) .v1v2v3 [7] v1v3 (1) .v2 ∨ v3 (9) v1v3 (1) .v2v3 (5) v1 ∨ v2 (3) .v2 ∨ v3 [8] v1v2 (4) .v2 ∨ v3 [8] v1v2 (4) .v2v3 (5) v1v2 (4) .v1v2v3 [6] v1 ∨ v2 (3) .v2v3 (5) v1 ∨ v2 (3) .v2 ∨ v3 (9) v1 ∨ v2 (3) .v1v2v3 [7] v1 ∨ v2 (3) .(v1 ∨ v2)v3 [11] v1v2 (4) .(v1 ∨ v2)v3 [11] v1 ∨ v2 (3) .v1 ∨ v2 (10) v1v2 (4) .v1 ∨ v2 (10) v1v2 (4) .(v1 ∨ v2)v3 [12] v1 ∨ v2 (3) .(v1 ∨ v2)v3 [12] v1 ∨ v2 (3) .v1v2 (13) v2 ∨ v3 (9) .(v1 ∨ v2)v3 [11] v2 ∨ v3 (9) .v1 ∨ v2 (10) v2 ∨ v3 (9) .(v1 ∨ v2)v3 [12] v2v3 (5) .v1 ∨ v2 (10) v2v3 (5) .(v1 ∨ v2)v3 [11]

-d 0 = (s 0 , s 0 ) is the initial state in D -For any (s, t) ∈ D • ((s, t), g ∩ h, (s , t )) ∈ Θ, if there exist (s, g, o, s ) ∈ N , (t, h, o , t ) ∈ T , such that o = o and g ∩ h = ∅ • ((s, t), g ∩ h, ∇) ∈ Θ, if there exist (s, g, o, s ) ∈ N , (t, h, o , t ) ∈ T , such that o = o and g ∩ h = ∅
v 2 v 3 (5) .v 1 v 2 (13 )
Fig. 2: The distinguishing automaton for machines in Fig. 1, state 11 is initial.

we introduce |Susp(M)| Boolean variables each of which represents a suspicious transition of the mutation machine. From now on we will use t to refer to both a suspicious transition and the variable which represents it. Then the conjunction c e def = t∈Susp(e) t of variables of transitions in Susp(e) specifies the submachines involved in the revealing execution e. Moreover, the disjunction of conjunctions of all executions in E α gives Boolean expression c α def = e∈Eα c e specifying all the submachines which are involved in all executions in E α and killed by the test α. As usual, the disjunction over the empty set is False and the conjunction over the empty set is True. Boolean expression c α is satisfiable whenever E α = ∅, since an α-revealing execution of M is a projection of the execution of the distinguishing machine. A witness solution of c α provides all the variables evaluated to True and defines a corresponding subset of Susp(M) which together with the trusted transitions of M determines (the transition relation of) a submachine of M involved in α-revealing executions.

Let

α = (v 1 v 2 v 3 )(v 1 v 2 v 3 )(v 1 v 2 v 3 )(v 1 v 2 v 3 )(v 1 v 2 v 3 )(v 1 v 2 v
3 ) be a test case. It triggers four executions in the distinguishing automaton in Fig. 2. These executions are defined by four executions of mutation machine in Fig. 1 including e 1 = t 1 t 3 t 5 t 10 t 1 t 3 , e 2 = t 1 t 3 t 5 t 11 t 1 t 3 , e 3 = t 1 t 3 t 7 t 5 and e 4 = t 1 t 3 t 7 t 6 . The executions e 3 and e 4 are defined by the two executions to the sink state of the distinguishing automaton. Execution e 3 is not α-revealing because it is nondeterministic. Only execution e 4 is α-revealing and includes the two suspicious transitions in Susp(e 4 ) = {t 7 , t 6 }. Thus c e4 = t 7 t 6 and c α = c e4 . The solutions of c α determine the submachines involved in e 4 .

We denote by Generate_a_submachine(c) a function which either determines such a submachine from a solution of c it obtained after calling a solver or returns null if c has no solution. Nondeterministic and partially specified submachines are not mutants. To exclude such submachines as well as the specification from any solution, clusters in suspicious states has to be considered.

Let s be a suspicious state, Z(s) = {Z 1 , Z 2 , . . . , Z n } be the set of its clusters. Then the conjunction of variables of a cluster Z i expresses the requirement that all these transitions must be present together to ensure that a submachine with the cluster Z i is completely specified in state s. Moreover, since all mutants are deterministic, only one cluster in Z(s) can be chosen, therefore, the transitions are restricted by the expressions determining clusters. Each cluster Z i is exclusively determined by Boolean expression z i def = ( t∈Zi t) ∧ ( t∈Susp(s)\Zi t) which permits the selection of all the suspicious transitions in Z i and the exclusion of the remaining suspicious transitions leaving s, i.e., the exclusion of the other clusters. Lemma 1. Let Z i , Z j ∈ Z(s) be two clusters of state s. Every solution of z i is not a solution of z j .

Then each state s in S susp yields the expression c s def = n i=1 z i of which all the solutions determine all the clusters in Z(s).

Lemma 2. Every solution of c s determines a cluster in Z(s) and every cluster in Z(s) is determined by a solution of c s .

Each solution of s∈Ssusp c s determines the set of clusters of suspicious states either in the specification or in a mutant. Each such cluster in the specification has at least one untrusted transition in Untr(S). Excluding the specification can be expressed with the negation of the conjunction of the variables of all the untrusted transitions t∈Untr(S) t. Any of its solutions excludes at least one cluster in the specification and therefore cannot determine the specification. The Boolean expression c clstr Considering the example mutation machine, we determine the Boolean expressions for the suspicious states 3 and 4. For the four clusters of state 3 Z 31 = {t 5 , t 9 }, Z 32 = {t 5 , t 8 }, Z 33 = {t 6 , t 7 , t 9 } and Z 34 = {t 6 , t 7 , t 8 } we build Boolean expressions z 31 = t 5 t 9 (t 6 t 7 t 8 ), z 32 = t 5 t 8 (t 6 t 7 t 9 ), z 33 = t 6 t 7 t 9 (t 5 t 8 ) and z 34 = t 6 t 7 t 8 (t 5 t 9 ). Then c 3 = (z 31 ∨ z 32 ∨ z 33 ∨ z 34 ). Similarly for state 4, we build c 4 = (z 41 ∨ z 42 ) where z 41 = t 10 t 13 (t 11 t 12 ) and z 42 = t 11 t 12 t 10 t 13 . Finally, c clstr = c 3 ∧ c 4 ∧ (t 5 ∨ t 9 ∨ t 10 ).

A solution of c α ∧ c clstr defines a subset of Susp(M) which together with the trusted transitions of M determines (a transition relation of) a mutant detected by α. All solutions thus determine all mutants detected by the test α. For a non-trivial mutation machine, a sheer number of killed mutants makes their enumeration impracticable. Hence, instead of determining killed mutants, we determine a (conforming or nonconforming) mutant which survives the test α. The negation of c α , c α determines the transition relations of not only all mutants which survive α but also other submachines which are not mutants. Considering the running example, a partially specified submachine having the suspicious transitions t 9 and t 8 is determined by the solution of c α which assigns True t 9 and t 8 ; such a submachine is not a mutant and it does not belong to Sub(M). To eliminate them as well as the specification, we use c clstr as before. Finally, each mutant which survives test α is determined by a solution of the expression c α ∧ c clstr .

Theorem 2. Test α ∈ G * does not detect a mutant P if and only if there is a solution of c α ∧ c clstr which determines P.

Checking Completeness of a Test Suite

Given a fault model S, , M , a fault subdomain for S, FD is a subset of Sub(M). A test suite, TS is a set of tests. TS is complete for fault subdomain FD if it detects all the nonconforming mutants in FD. Let us define c TS def = α∈TS c α , a Boolean expression which determines the submachines involved in revealing executions for the tests in TS. Procedure Build_expression for building c TS is presented in Algorithm 1.

Let c fd be a Boolean expression specifying only all mutants in a fault subdomain FD. It can be formulated as the conjunction c clstr with another (possibly always True) Boolean expression over the variables of suspicious transitions, which excludes mutants from Sub(M) to obtain FD. A fault subdomain can always be refined with an expression specifying the mutants to be excluded. Later, in checking the completeness of a test suite for a given FD, we will be excluding conforming mutants. Theorem 3. Test suite TS is complete for fault subdomain FD if and only if c TS ∧ c fd has no solution or each of its solutions determines a conforming mutant.

The fault domain Sub(M) is specified with c clstr , which leads to Corollary 1.

Corollary 1. Test suite TS is complete for Sub(M) if and only if c TS ∧ c clstr has no solution or each of its solutions determines a conforming mutant.

Based on Theorem 3, checking the completeness of a test suite for a fault subdomain FD amounts to its iterative refinement by excluding conforming mutants as solutions to c TS ∧ c fd while no nonconforming mutant is found. In particular, the negation of the conjunction of variables of all suspicious transitions of a conforming mutant added to c fd excludes it from FD. This method is formalized in Algorithm 2 which presents Procedure Check_completeness for checking the completeness of a test suite TS for a fault subdomain specified by the input parameter c fd which is refined each time a conforming mutant is generated. The procedure Check_completeness also takes as inputs a test suite TS and the distinguishing automaton for the mutation and specification machines. It returns a witness test detecting a mutant surviving TS in case TS is not complete; otherwise the witness test is empty, which indicates that TS is complete. It also returns an updated expression of c fd specifying a reduced fault domain which is used to generate tests that make TS a complete test suite in Section 5. Procedure Check_completeness proceeds as follows. It calls Build_expression for building c TS , the Boolean expression which determines the submachines involved in revealing executions for tests in TS. Initialy, the fault domain is specified with the conjunction of c fd with the negation of c TS which determines all mutants surviving TS. The execution is iterative and each step consists in generating a mutant surviving TS, checking the conformance of the mutant and removing from the current fault domain the mutant in case it is conforming.

Procedure Check_completeness makes calls to Generate_a_submachine to select a mutant in a fault domain specified with Boolean expression c fd . Generate_a_submachine returns null in case the fault domain is empty. The execution of Check_completeness stops when Generate_a_submachine returns a nonconforming mutant or null. In case null is returned, the test suite is declared complete and Check_completeness returns the empty test; otherwise the test suite is declared incomplete and Check_completeness returns a non empty witness test detecting a nonconforming mutant. In both cases Check_completeness returns an expression specifying the reduced fault domain at the end of the execution. In the next section, we will check the completeness of generated tests (e.g., the witness tests) for the reduced fault domains in determining complete test suites for fault domains specified with mutation machines. 6 Prototype Tool and Experimental Results

t5t11t12)∨ (t5t8t10) c fd ∧ (t5t11t12) ∨ (t5t8t10) ∅ α, β, γ ε α = (v1v2v3)(v1v2v3)(v1v2v3)(v1v2v3)(v1v2v3)(v1v2v3) β = (v1v3)(v1 ∨ v2)(v2 ∨ v3) γ = (v1v3)(v1 ∨ v2)(v2v3)(v1v3 ∨ v2v3)(v1v3)(v1v2v3)(v2v3) (
We implemented in JAVA a prototype tool consisting of three main modules. The first module for parsing mutation machines in text format was developed using ANTLR 4.1 [START_REF] Parr | The Definitive ANTLR 4 Reference[END_REF]. The second module is concerned with building clusters, distinguishing automata and Boolean expressions for undetected mutants; it uses as a back-end the solver Z3 [START_REF] De Moura | Z3: An efficient smt solver[END_REF] for solving of non Boolean expressions obtained by combining predicates in building clusters and automata. We integrated the solver in the tool using a Z3 API. The third module is responsible of solving Boolean expressions for mutants, extracting mutants and generating new tests. The module also uses solver Z3 though it may also use a SAT solver [START_REF] Eén | An extensible SAT-solver[END_REF] since it deals with the resolution of Boolean expressions only.

In our experiments, we use a desktop computer with the following settings: 3.4Ghz Intel Core i7-3770 CPU, 16.0 GB of memory (RAM), Windows 7 (64 bits).

We use the prototype on an industrial-like SIFSM model obtained by transforming a Simulink/Stateflow model [START_REF] Petrenko | A method and tool for test optimization for automotive controllers[END_REF] of an automotive controller. To regulate the air quality in a vehicle, the controller sets an air source position to 0 or 1 depending on its current state and truth values of predicates on integer and Boolean input variables. The transformation required flattening and determinizing the original hierarchical Simulink/Stateflow model. The determinization is based on priorities assigned to nondeterministic transitions as it is done by Simulink [START_REF] Scaife | Defining and translating a safe subset of simulink/stateflow into lustre[END_REF]. We obtained a SIFSM with 13 states, 62 transitions and 22 input variables. Then we have manually introduced faults (transition faults, output faults, swapping of variables, replacing variables with constants), obtaining a mutation machine with 2 13 -1 = 8191 mutants. Our tool generates, within 30 seconds, a complete test suite with 14 tests detecting the mutants. Finally, we generate complete tests from automatically generated mutation machines with a generator executing randomly selected mutation operations. Table 2 presents the numbers of mutants in the mutation machines, the number of tests in the generated complete test suites. The maximal length of the tests is 8. We observed that the test generation is fast when the mutation operations introduce a small number of nonconforming mutants, which is a realistic assumption [START_REF] Jia | An analysis and survey of the development of mutation testing[END_REF] for applying our method.

Conclusion

We lifted the multiple mutation testing approach developed for classical (Mealy) FSM to symbolic input finite state machine (SIFSM). SIFSM extends classical FSM with predicates defined over input variables with possibly infinite domains.

We defined well-formed mutation machines for SIFSM as a fault model for compact representation of a fault domain consisting of several faulty implementations (mutants) of a specification machine. Then we defined mutation operations for building wellformed mutation machines. Based on the machine equivalence and distinguishability relations, we have defined tests detecting nonconforming mutants and developed a multiple mutation testing approach from SIFSM. The proposed approach leveraging on that developed for classical FSM includes a method for checking the completeness of test suites, i.e., their adequacy to detect all nonconforming mutants in a fault domain, and a method for complete test suite generation avoiding mutant enumeration. The novelty of the proposed approach is that it can analyze and enhance completeness of symbolic tests w.r.t. user defined fault models for a specification with infinite input domains.

The experiments with a prototype tool we have developed indicate that our methods can be applied to industrial-like models of systems.

Our current work focuses on extending the approach to FSM with outputs determined by arithmetic operations over input and output variables [START_REF] Petrenko | Checking experiments for symbolic input/output finite state machines[END_REF], to FSM extended with timing predicates [START_REF] Batth | Specification of timed efsm fault models in sdl[END_REF][START_REF] Nguena Timo | Conformance testing of variable driven automata[END_REF] and to program.

Definition 3 .

 3 Given a DSIFSM S = (S, s 0 , V, O, N ) and a mutation machine M = (S, s 0 , V, O, T ) of S, a finite automaton D = (D ∪ {∇}, d 0 , G, Θ, ∇), where D ⊆ S × S, ∇ is an accepting (sink) state and Θ ⊆ D × G × D is the transition relation is the distinguishing automaton for S and M, if it holds that

Fig. 2 Theorem 1 .

 21 Fig.2presents the distinguishing automaton for the mutation and specification machines in Fig.1. Multiple transitions are represented with a single arc labeled with multiple inputs.An execution of D starting at the initial state d 0 and ending at the sink state ∇ is said to be accepted. The language of D, L D is the set of tests labeling accepted executions of D. Any nonconforming mutant in Sub(M) can be detected by a test in L D .Theorem 1. Given the distinguishing automaton D for S and M, P S for some P ∈ Sub(M) if and only if P α S for some α ∈ L D .

def=

  s∈Ssusp c s ∧ t∈Untr(S) t Procedure Build_expression (TS, D); Input : TS, a test suite Input : D, the distinguishing automaton of mutation machine M and specification S Output : cTS, a Boolean expression defining submachines of M involved in revealing executions for tests in TS cTS := False; for each α ∈ TS do Using D, determine Eα, the set of α-revealing executions of M; cα := False; for each e ∈ Eα do ce := t∈Susp(e) t ; cα := cα ∨ ce; end cTS := cTS ∨ cα; end Return cTS; Algorithm 1: Building c TS excludes nondeterministic and partially specified submachines and the specification, which means that c clstr specifies only all mutants in the fault domain Sub(M).

  5 , t 6 , t 7 , t 8 , t 9 , t 10 , t 11 and t 12 ; three of them t 5 , t 9 and t 10 are untrusted. The states 3 and 4 are suspicious. The four clusters of state 3 are {t 5 , t 9 }, {t 5 , t 8 }, {t 6 , t 7 , t 9 } and {t 6 , t 7 , t 8 }. The only two clusters for state 4 are {t 10 , t 13 } and {t 11 , t 12 , t 13 }. The mutation machine includes seven mutants and the specification machine. Execution t 1 t 3 t 7 t 5 is nondeterministic because it includes two nondeterministic transitions t 7 and t 5 . Execution t 1 t 3 t 7 t 6 is deterministic and involves four mutants determined with the following sets of suspicious transitions {t 9 , t 7 , t 6 , t 10 }, {t 9 , t 7 , t 6 , t 11 , t 12 }, {t 8 , t 7 , t 6 , t 10 } and {t 8 , t 7 , t 6 , t 11 , t 12 }.

Table 1 :

 1 Execution of Procedure Complete_test_gen with the initial test α.

		In Check_completeness		End of the step
	step Revealing. Exec cTS curr	c fd	Surv. mut.	TS	TScurr
	init N/A	N/A	cclstr	N/A	∅	α
	1 t1t3t7t6	t7t6	c fd ∧ t7t6	t8, t11, t12	α	β
	2 t1t3t8	t8	c fd ∧ t8	t9, t11, t12	α, β γ
	3 t1t3t5t12t3t5t10,
	t1t3t5t10t1t3t8

Table 2

 2

	: Experimental results with the prototype tool
	#Mutants 8191 163839 1105919 9400319
	#Tests	14	15	18	18
	Time (sec.) 30	90	100	296

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

In checking the completeness of the initial test suite {α} for the example mutation machine and test α, Check_completeness takes as input c fd = c clstr , TS = {α} and the distinguishing automaton in Fig. 2. Then, it determines c TS = c α = t 7 t 6 , sets c fd = c TS ∧ c clstr , c P = False and α = ε and starts executing the loop. In the first iteration, the call of Generate_a_submachine with input c fd has generated the mutant with the suspicious transitions t 8 , t 11 , t 12 . The mutant is nonconforming and killed by the test

) labeling a path to the sink state in the distinguishing automaton for the mutant. Then the execution of Check_completeness terminates with outputs c fd and non empty test β, which indicates that the test suite {α} is not complete.

Complete Test Suite Generation

In case an initial (possibly empty) test suite does not detect all the nonconforming mutants in a fault domain, we want to generate tests which together with the initial tests constitute a complete test suite for the fault domain. This can be done iteratively by adding a new test detecting a nonconforming mutant surviving the incomplete test suite, obtaining a new test suite which in turn can be augmented in case it is not complete. This complete test suite generation method is formalized in Algorithm 3 with procedure Complete_test_gen which takes as inputs an initial test suite TS init and a fault domain represented with a mutation machine. At every step, the procedure adds a current test Procedure Complete_test_gen always terminates because the execution of its only loop always terminates. This is because the initial fault domain consisting of a finite number of mutants is reduced at every iteration step of the loop and Check_completeness returns the empty test when executed with the empty fault domain as an input.

Considering the running example, Table 1 summarizes data computed in executing Complete_test_gen to generate a complete test suite from initial test suite TS init = {α}. The iteration step appears at the first column. Data are initialized at the end of step init. In each step Complete_test_gen makes a call to Check_completeness which computes the executions revealed by TS curr determined in the previous step and updates c fd . Three iteration steps were sufficient to obtain the complete test suite {α, β, γ} having three tests for the detection of the seven nonconforming mutants, which shows that the method permits generating fewer tests than the nonconforming mutants. Notice that we generate symbolic tests; their concrete instances should be used to execute against black box implementations. In our working example, for simplicity, all input variables are Boolean, which however, can represent comparisons of integer variables with some constants. The obtained concrete tests could then be just rewritten by replacing every Boolean variable by an instance of the corresponding comparison.