Gregor V Bochmann
email: bochmann@uottawa.ca

Conformance Testing with Respect to Partial-Order Specifications

This paper deals with the testing of distributed systems. An implementation under test is checked for conformance with the properties defined by a reference specification. Since distributed systems usually have multiple interfaces, the reference specification will not define the order of all pairs of interactions taking place at different interfaces. Therefore a specification formalism supporting the definition of partial orders is required. Different such formalisms are compared in this paper, including MSC-Charts (or Interaction Overview Diagrams). A variation of this formalism, called Partial-Order-Charts (PO-Charts) is proposed which makes abstraction from the exchange of messages. It concentrates on the specification of partial orders between local actions in different system components. It is shown that the partial-order testing approach introduced for a single partial order specification can be adapted to testing PO-Charts which define various combinations of different partial orders which are sequenced by strict or week sequencing, including loops. Various examples are given to compare this testing approach with state machine testing methods which can be applied for bounded PO-Charts for which one can derive an equivalent state machine. The testing complexities and fault model assumptions of these two approaches are compared.

Introduction

Conformance testing is an activity where an implementation under test (IUT) is checked for conformance to a specification. For this purpose, input interactions are applied by testers at the different interfaces of the IUT and the outputs provided by the IUT are observed by the testers and are compared with what is expected according to the requirements defined by the specification. For distributed systems, the order of interactions taking place at different interfaces are often irrelevant for the defined behavior, furthermore, it is sometimes difficult to control the order of inputs at different interfaces, and to observe the order of outputs at different interfaces. For this reason, state machine models for the specification are not appropriate, since they precisely define a total order for all interactions. As a consequence, partial-order specifications have been proposed for describing the required behavior of distributed systems. A well-known example of a partial-order notation is Message Sequence Charts (MSC, or UML Interaction diagrams).

In order to test partial-order specifications, [Haar] proposed the concept of Partial-Order Input-Output Automata (POIOA) and discussed how to derive conformance test suites from such specifications. A POIOA is a state machine where each transition involves in general a set of input and output interactions for which a partial order is defined for their execution. However, each state of the POIOA represents a global synchronization point involving all the distributed interfaces. This enforces strict sequencing between the execution of subsequent transitions, that is, an interaction of the next transition can only occur after all interactions of the preceding transition have been completed. In real distributed systems, one often rather wants to impose weak sequencing which means that sequencing is enforced locally at each interface (or each component of the distributed system), but not globally.

Concepts for specifying control flow in distributed systems with partial orders including strict AND weak sequencing was proposed in [Castejon]. These concepts are quite similar to the more formal definition of MSC-Charts given by Alur and Yannakakis [Alur]. In a few words, an MSC-Chart is a state machine in which each state is associated with an MSC to be executed and the transitions between states are spontaneous. We modify this concept as follows and call it Partial-Order Chart (PO-Chart) by specifying for each transition whether it represents strict or weak sequencing, and by associating with each state a partial order of actions (including inputs, outputs and local actions) where each action is placed on a vertical "swim-lane" ("process" in MSC, or "role" in [Castejon]). Such a partial order is very similar to an MSC, but the arrows represent a partial-order dependency, and not necessarily exchanges of messages (as in MSCs and MSC-Charts).

We discuss in this paper how a test suite can be derived from a given PO-Chart specification. The main point is the fact that the partial-order test derivation from [Haar] can be applied to execution paths involving several PO-Chart states (corresponding to several transitions in the POIOA model). For limiting the length of the test suite in the case of loops in the PO-Chart, we adopt the approach that is common in software testing: assuming regularity of the IUT (as explained in [Bouge]), which means that one assumes that there exists an integer k such that, if a loop has been executed k times, then no further fault would be found if one executed the loop more than k times.

The paper contains many examples to illustrate the discussion. For the testing of an IUT in respect to a PO-Chart the partial-order testing of [Haar] is compared with state machine testing methods based on an equivalent state machine model. However, often the PO-Chart specifications are not bounded [Alur], which means that no equivalent finite state model exists.

The paper is structured as follows: In Section 2, an introduction to POIOA testing is given, as well as a formal definition of partial orders. In Section 3, we discuss the different notations for defining the reference specification for testing. In Section 4 we show how the partial-order testing of [Haar] and state machine testing can be applied to PO-Charts. In Section 5, we provide some comments comparing the specification formalisms of POIOA, collaboration ordering, MSC-Charts and PO-Charts. We also compare the complexity measures for partial-order and state machine testing, as well as the underlying fault models. Section 6 contains the conclusions.

Preliminaries

2.1

Testing POIOA

The testing of POIOA was introduced in [Haar]. A POIOA is a state machine where each state transition involves possibly several input and output interactions for which a partial order is specified for execution. When all interactions of a transition have been performed, the machine enters the next state and is ready to execute another transition. One normally assumes that each transition starts with a single or several (concurrent) input interaction(s). An example of such a transition is shown in Figure 1(a). This transition starts with the single input i1 which is followed by two concurrent outputs o1a and o1b, each followed by a sequence of input and output, i2 followed by o2 and i3 followed by o3, respectively. When testing an implementation for conformance with a POIOA specification, one has to verify the following two aspects:

1. The partial order of interactions specified for each transition is implemented as specified. 2. Each transition leads to the correct next state. For the second aspect, traditional state machine testing approaches can be used, such as Distinguishing Sequences [Bochmann a] or the HIS method [Bochmann c]. For this purpose one needs state identification sequences for each state which are applied after the execution of a transition, and which should be checked for validity on the implementation. We do not discuss these issues further in this paper.

For the testing of the partial order of input and output interactions defined for a given transition t, the following partial-order test has been proposed (see for instance [Bochmann a]). For each input i of t, perform the following test (where it is assumed that the implementation is already in the starting state of the transition):

1. Apply all inputs (different from i) that are not after i in the partial order of t (in an order satisfying the partial order), and observe the set of output interactions, called O1. 2. Apply i, and observe the set of subsequent output interactions, called O2. 3. Apply all other inputs of t (in an order satisfying the partial order), and observe the set of output interactions, called O3. If one of the output sets is different than what is expected from the specified partial order, we have detected a fault in the implementation. We have a guarantee of fault detection under the assumption that the transition t is realized in the implementation as a single transition and in the form of a partial order. For the example transition shown in Figure 1(a), we obtain the following test suite (where the tested input is written in bold, and the expected output sets are given in {}):

• For testing i1: <{}, i1 {o1a, o1b}, i2 {o2}, i3 {o3}> • For testing i2: <{}, i1 {o1a, o1b}, i3 {o3}, i2 {o2}>

• For testing i3: same test case as for i1.

In [Bochmann a], it was also explained that the tests for several inputs can be combined into a single test case if one of the input comes after another one. For the example transition, we are left with the two test cases given above.

In this paper, we limit our attention to quiescent states of the IUT, that is, states in which no further outputs are produced by the IUT unless further input is applied. The above partial-order test goes only through quiescent states, since the next input is only applied after some time-out period to ensure that no additional output is expected. An interaction sequence is called a quiescent trace [Simao] if each input is applied when the IUT is in a quiescent state. For example, the sequence < i1, o1a, i3, etc. > is allowed by the partial order of Figure 1(a), but it is not quiescent. The testing of nonquiescent traces is discussed in [Bochmann a].

It was noted that the length of the resulting test suite for testing a single transition using this method is much shorter in the presence of many concurrent inputs as compared with traditional state machine testing. For the example transition shown in Figure 1(a), the corresponding state machine (showing only quiescent states) is shown in Figure 1(b). State machine testing (without state identification) yields for this state machine the same two test cases above. However, if there are more concurrent inputs, the number of states of the corresponding state machine will blow up exponentially (see also Section 5).

The notion of POIOA has been criticized because it assumes that there is global synchronization (involving all interaction points) in each state of the automaton. It was argued that this is not realistic if the behavior of the POIOA is supposed to represent the behavior of a distributed system where interactions take place at different interaction points distributed over several system components. To avoid this criticism, we consider in this paper the concepts explained Section 3, which allow for strict sequencing of transitions (as in the case of POIOA), as well as for weak sequencing (which is more natural in distributed environments).

Formal definition "partial order"

Given a set E of events, a partial order on E is a binary relation < of events which is transitive, antisymmetric and irreflective. If <e1, e2> is in <, we say that e1 is before e2. Often we characterize an order by the event pairs that generate all pairs in the order by transitivity closure. We call these the generating event pairs of the order. For instance, the arrows in Figure 1(a) correspond to the generating event pairs, for instance the pair <i1, o1a>. However, the partial order defined by this figure also includes pairs such as <o1a, o2> which are obtained by transitivity.

In order to deal with a situation where the same type of event occurs several times, one usually considers a Partially Ordered Multi-Set (Pomset). Given a partial order (E, >) where some events in E may be of the same type, a Pomset on (E, >) is obtained by adding a labeling function L: E -> V, where V is a set of labels. For a given event e ϵ E, L(e) represents the type of event e. In fact, the names given to events in our figures represent the type of the event shown. For instance, the first event in We call initiating event any minimum event of the order, that is, event e ϵ E is minimum if there is no event e' ϵ E such that e' < e. Similarly, we call terminating event any maximum event of the order. In the remainder of this paper, when we talk about a partial order, we always mean a Pomset where the set of labels V is often partitioned into two subsets: the set I of inputs and the set O of outputs.

3

The concept of PO-Charts

Collaborations

Concepts for describing the behavior of distributed systems in a global view have been proposed in [Castejon]. First, the UML concept of collaborations is used. A collaboration identifies the different roles that the components of the distributed system may play in a given application. However, this UML concept does not talk about the dynamic aspect of the behavior. For describing the dynamic aspect of the behavior, it is proposed to decompose a given collaboration into several sub-collaborations (each involving possibly a subset of roles) and indicating in which order these subcollaborations are performed. Using the sequencing primitives of UML Activity diagrams (sequence, alternative and concurrency) an Activity-like notation is proposed, however, with the following modifications to the semantics: (a) a single Activitycalled a "collaboration" -would normally involve several parties (roles -or swimlanes); and (b) sequencing between successive collaborations may be in strict sequence (as in UML Activity diagrams, where any sub-activity of the second collaboration can only start when all sub-activities of the first have been completed), or in weak sequence (where a role may start with its activities of the second collaboration when it has completed its own sub-activities for the first).

A simple example is shown in Figure 2 (this is Figure 3 from [Castejon]). This is a simplified model of the execution of a medical test at the patient's premises in the context of tele-medicine. There are three roles in the system, as shown by the UML collaboration diagram of Figure 2(a): dt (doctor terminal), tu (test unit), and dl (data logger). Figure 2(b) shows the dynamic behavior of the Test collaboration: A Test starts with the DoTest sub-collaboration which is followed by the LogValues subcollaboration. This may be repeated several times until the GetValues subcollaboration is performed. The whole may be repeated several times.

The Test collaboration shown in the figure can, in turn, be used as a subcollaboration in a larger context of tele-medicine, as discussed in [Castejon]. This notation, therefore, allows for writing hierarchically structured behavior specifications. At the most detailed level, the behavior of a collaboration can be defined in the form of a Message Sequence Chart (MSC, also called UML Interaction diagram). A very simple example is shown in Figure 3 However, in the context of this paper, we prefer to define the behavior of a basic, unstructured collaborations in the form of what we call a partial order with roles. This is a notion very similar to an MSC. Like in MSCs, the roles involved in the behavior are explicitly shown as vertical line. Actions performed by a role are indicated by dots (events) with their names (event labels) and the partial order between these events is indicated by arrows. However, these arrows do not necessarily represent messages, as in MSCs. An example is given in Figure 3(b) for the behavior of the two collaborations DoTest and LogValues combined (see Figure 2(b)).

The semantics of the sequencing primitives that define the order in which subcollaborations are executed are defined in [Castejon] informally, based on the semantics of Activity diagrams (with modifications). A formal definition, using partial orders of events, is given by Israr [Israr] where, in addition, performance aspects are considered.

MSC-Graphs

In their article of 1999 [Alur], Alur and Yannakakis consider model checking of MSCs. This paper contains several discussions that are useful for our purpose: 1. The paper formally defines the semantics of an MSC (basic features only) based on partial orders. 2. The paper formally defines the notation of MSC-Graphs which correspond to the UML notation of Interaction Overview Diagram (see for instance figure 17.27 in [UML]). An MSC-Graph is an oriented graph where each node represents an MSC and each edge represents the sequential execution of the pointed MSC after the initial MSC. It is assumed in [Alur] that all edges either represent strict sequencing (called synchronous concatenation) or weak sequencing (called asynchronous concatenation). However, in this paper we assume that for each edge the type of sequencing can be specified separately (similar as in the collaboration notation discussed in Section 3.1).

The paper formally defines Hierarchical MSCs which is an extension of MSC-

Graphs were a node may also represent another MSC-Graph or Hierarchical MSC. However, it is assume that there is no recursion in this dependency. It is shown how a Hierarchical MSC can be flattened in order to obtain an equivalent (more complex) MSC-Graph. As this notation does not introduce any additional power of description, we do not further discuss this notation in this paper. 4. The paper defines a subset of MSC-Graphs, called bounded MSC-Graphs which have the important property that the defined behavior is regular, that is, it can be represented by a finite state machine. Therefore, such MSC-Graphs can be modelchecked (which is further discussed in [Alur]), and also, for such MSC-Graphs state machines testing methods can be applied. -An algorithm for determining whether a given MSC-Graph is bounded is also given. Essentially, it proceeds as follows: (a) The communication graph of an MSC has nodes corresponding to the roles (processes) of the MSC and an arc from p1 to p2 if role p1 sends a message to p2 in the MSC. (b) Given a subset S of nodes of an MSC-Graph, the communication graph of S is the union of the communication graphs of all the MSCs in the nodes of S. In such a graph, the roles that receive or send a message in some MSC of the graph are called the active processes of the graph. (c) An MSC-Graph is bounded if for each cycle c in the graph, the communication graph of the nodes on this cycle (after eliminating all non-active roles) is strongly connected.

PO-Charts

Inspired by the definition of MSC-Charts, we use in this paper the notion of PO-Charts. These charts are defined like MSC-Charts, except that each node, instead of containing an MSC, contains a partial order with roles, as defined in Section 3.1. Hierarchical PO-Charts and bounded PO-Charts can be defined as described for MSC-Charts in [Alur].

The main difference with MSC-Charts is the fact that for each edge representing the sequential execution between two partial orders with roles, it is indicated whether sequencing is weak or strict. Weak sequencing (abbreviated "ws") means that sequencing is enforced for each role separately. Strong sequencing (abbreviated "ss") means that the initiating events of the second partial order may only occur after all terminating events of the first partial order have occurred. This means that a strong synchronization point is introduced at this point during the execution.

We note that Hierarchical PO-Charts are an alternative notation for defining the behavior of collaborations as discussed in Section 3.1. We prefer this notation because it has a formally defined semantics, however, it does not support directly concurrency. An example of a PO-Chart is shown in Figure 4

Conformance testing with respect to PO-Charts

General testing assumptions

Test architecture

For distributed systems, the test architecture has a big impact on testing. For testing a system that has several interfaces, one often uses the distributed test architecture where a local tester is associated with each interface of the system. If the local testers cannot communicate with one another, there are usually synchronization problems for controlling the order of inputs to be applied to the system and difficulties to observe the order of outputs at different interfaces. Therefore an architecture with local testers without mutual communication provides usually incomplete testing power. -In the following we assume a test architecture with local testers that can communicate with one another by message passing.

Architectures for testing distributed systems in respect to specifications in the form of MSC were described in a recent paper [Dan]. In this context, it was assumed that the processes identified in the MSC can be classified as system or user processes.

Then the user processes are replaced by local testers (that may, or may not communicate with one another). These testers exchange messages as specified by the given MSC.

We take a slightly different approach for testing distributed implementations in respect to PO-Chart specifications. We assume that each role of the PO-Chart may have a local interface to which a local tester can be attached. We assume in this paper that these local testers can communicate with one another by message passing. We assume that, at each local interface, the local tester communicates with the implementation of the role behavior through input and output interactions. These are synchronous interactions between the tester and the role implementation, without queuing. This is similar to the interactions of POIOA, although the interactions of PO-Charts are associated with a particular role. Let us consider the example PO-Chart of Figure 4 (left). In order to define a suitable test architecture, we have to determine which of the given actions are input or output, or whether they are local actions that cannot be observed by the local tester. It may also be necessary to introduce additional input or output interactions in order to increase the power of testing. For this example system, we propose the enhanced PO-Chart of Figure 4 (right) which contains a few additional interactions with the local testers. Non-observable local actions are represented by dark dots, inputs by white dots, and outputs by white rectangles.

Test suites

Since usually no finite test suite provides the guarantee that all possible implementation faults would be detected, Bougé et al. [Bouge] suggest to consider a sequence of test suites TS i (i= 1, 2, …) with increasing complexity, such that all faults detected by TS i would also be detected by TS i+1 . Then one can talk about validity of such a set of test suites, which means that for any possible implementation fault, there is a test suite TS i (for some i) that would detect this fault.

Fault models [Bouge] also stresses the point that there are always some assumptions that are made about the tested implementations. These assumptions are often called fault model. The fault model defines the range of faults that should be detected by the given test suite. And at the same time these assumptions also state what properties of the implementation are assumed to be correctly implemented (and therefore need not be tested).

In this context, [Bouge] mentions the following types of assumptions that are important for justifying the selection of particular test suites:

• Regularity hypothesis: This is an assumption about the structure of the implementation. Assuming that we have some measure of the complexity of each test case, the regularity hypothesis states that there is a value of complexity k such that, if the implementation behaves correctly for all test cases with complexity less than k then it behaves correctly for all test cases. -In program testing, for example, one typically executes loops only once or twice and assumes that if no fault was detected then further executions of the loop will not lead to undetected faults.

• Uniformity hypothesis: This assumption justifies the practice in program testing where the domain of input parameters is partitioned into subdomains and some random values are selected in each sub-domain for testing. It is assumed that, if the implementation behaves correctly for some value in a sub-domain, then it will behave correctly for all values in that domain. How do these considerations apply to the testing of PO specifications? -The uniformity hypothesis applies to the variation of parameters of inputs to the implementation. In this paper we assume a finite set of distinct inputs where parameters can be ignored. -The regularity hypothesis takes on a particular form in the context of FSM testing methodology. The typical fault model of state machine testing assumes that the number of states of the implementation is not much larger (if not smaller or equal) to the number of states of the reference specification. Under this assumption, the test suites with test cases of bounded length can provide the guarantee of fault coverage.

For testing PO-Charts, we propose to use a regularity hypothesis similar to what is used for program testing. A PO-Chart defines possible control flows from the initial MSC-node to the final MSC-node. This is like the control flow in a program. As in program testing, we propose to test a PO-Chart by executing the different control paths through the chart, possibly using the well-known All-Branches or All-Paths criteria and executing loops typically once or twice.

Testing PO-Charts

For a bounded PO-Chart, there are essentially two approaches to test suite selection:

• The partial-order testing method proposed in this paper: The test designer should select a number of control flow paths through the PO-Chart, concatenate the partial orders of the nodes in the order of the path, using weak or strong sequencing as defined by the PO-Chart. The resulting partial order of inputs and outputs is then tested using the partial-order test described in Section 2.1. • The state machine testing approach (with all its different test selection methods): Derive the state machine that has the same behavior as the PO-Chart, and then use one of the state machine testing methods. If the PO-Chart is unbounded, the second approach is not applicable. As an example, we first discuss in the following the testing of a very simple bounded PO-Chart, and then consider an examples of unbounded PO-Charts.

Example of a bounded PO-Chart

We consider the PO-Chart shown in Figure 5(a) which contains a loop with node A containing the partial order of Figure 1(a) with an additional ordering constraint indicated by the dotted arrow. All sequencing between nodes are week sequences, alt-hough for this example this is equivalent to strong sequencing.

State machine testing

The state machine of Figure 5(b) is a partially defined machine. We recall that many state machine testing methods assume that the machine is fully defined (that is, in all states for all inputs). Let us assume that input messages received by the system are stored in a message pool until the system gets into a state where the input can be consumed (this is called "full reordering of messages" in [Castejon], Section 3.1). This is advantageous in distributed systems for avoiding race conditions [Bochmann b]. If we assume this for the state machine of Figure 5(b), then in all states all inputs can be accepted -inputs for which no transition is defined in the current state will provide no output, however, the state of the system changes since the content of the pool changes. Under this assumption, the state machine of Figure 5(b) has unique input-output (UIO) sequences of length one for all states, except for state 5. Let us assume that we ignore the possible implementation fault that the i4-transition leads to one of the states 1, 2, 3 or 4. A test suite with fault detection guarantee for implementations built as state machines with not more than 5 states would first include the test cases for validating the UIO sequences. These tests would already include the test cases <i1, i2, i3, i4> and <i1, i3, i2, i4> which cover all transitions of the state machine.

Partial-order testing

This PO-Chart allows for an infinite number of execution paths p(n) -for n = 0, 1, 2, … where p(n) consists of n repetitions of the partial order of node A followed by one execution of node B. If we only test the path p(1), using the partial order test described in Section 2.1, we obtain the two test cases <i1, i2, i3, i4> and <i1, i3, i2, i4>. For the path p(2) -shown in Figure 6(a) -we obtain the following test cases (where the dependencies of the bold inputs are determined): <i1, i3, i2, i1, i3, i2, i4> and <i1, i2, i3, i1, i2, i3, i4>.

Examples of unbounded PO-Charts

Let us consider the PO-Chart of Figure 5(a) again, but now without the dashed dependency. This chart is not bounded because there is no dependency where the right process has to wait for the left process. In this case, the right process may execute a second i1 input before an i3 input is applied to the left process, and this may repeat after a second i2 input is applied to the right process.

With partial-order testing, we obtain for testing the path p(2) the following test cases: <i1, i3, i2, i1, i3, i2, i4> and <i1, i2, i1, i2, i4, i3, i3>. For state machine testing one may want to test an initial part of the corresponding infinite state machine. Such an initial part is shown in Figure 6(b).

Another example of an unbounded PO-Chart is shown in Figure 4(right). The shortest execution path goes through the partial orders of the two nodes only once. In this case, the partial-order test gives rise to the following test cases (again, the inputs for which the dependencies are tested are written in bold): <request, get-req, i2, i3, i5> and <request, i2, i3, get-req, i5>. The realization of a correct implementation for the behavior defined by this PO-Chart is not straightforward, as discussed in [Faleh]. An implementation using messages for the order dependencies shown in the PO-Chart does not work because in the case that the doctor terminal (dt) sends a getreq message immediately after the request message to the test unit (tu), the former message may arrive at the data-logger (dl) before the o2 message arrives, which means that the data value returned does not include the last test measurement. Such a fault would be detected by the first test case. A well-known solution for a correct implementation is to count the number of times that the first node of the chart is executed, and include this information in the messages sent to the data-logger [Faleh].

We note that this implementation fault would possibly not be detectable if there was no testing interface at the test unit system component. On the other hand, the observation of the confirm output at the test unit is not useful for fault detection. We note that the first test case requires some coordination between the local testers at the doctor terminal and the test unit in order to make sure that the i2 input is not applied before the get-req input at the doctor terminal and all resulting outputs (in this case none -a timeout is assumed after each input in the test case) are observed.

Discussion

Specification formalism

The POIOA specification formalism has been criticized for assuming strong synchronization points in each state of the machine. This corresponds to PO-Charts in which all sequential edges between different nodes (partial orders) have strict sequencing. In contrast to the partial orders associated with POIOA transitions, the partial orders associated with a node of a PO-Chart indicates for each interaction the role (process or interface) where the interaction takes place. This additional information allows us to define weak sequencing between different nodes of a PO-Chart.

One could possibly introduce an extension to POIOA where the sequencing of incoming and outgoing transitions at each state could be explicitly specified by indicating for each initiating event of an outgoing transition what are the terminating events of an incoming transition for which this initial event must wait before proceeding (if the state was reached by that incoming transition). If it has to wait for all terminating events, then we have the situation of normal POIOA where the incoming transition must be completely terminated before an outgoing transition may start. Weak sequencing could also be specified if the roles of the events are known. However, we are not convinced that such a generality of defining the sequence of transitions is useful -we prefer the addition of the role information (as defined for PO-Charts) which automatically defines the semantics of weak sequencing (if this is the desired form of sequencing).

Testing complexity

It was argued in [Bochmann a] that the partial order test, as discussed in Section 2.1, is of much lower complexity than state machine testing when applied to systems with concurrency. This does not show up in the simple examples discussed above. But it is clear that the number of states of a state machine that is equivalent to a partial order grows exponentially if the degree of concurrency in the partial order increases. With the number of states of the reference specification, also the length of the test suite will grow accordingly.

As an example, we consider here a variation of the partial order of Figure 1(a) where we assume that three inputs i2, i3 and i4 are enabled after the input i1 (see Figure 7(a)). The corresponding state machine is shown in Figure 7(b). The state machine testing approach requires at least 6 test cases to cover all the branches of the state machine. With the partial order approach, we obtain the three test cases <i1, i2, i3, i4>, <i1, i3, i4, i2>, and <i1, i2, i4, i3>.

Different fault models

One may suspect that the lower complexity of the partial-order tests implicitly implies that their fault coverage is lower. This is in fact true. The fault model for which the partial-order tests provide fault coverage makes stronger assumptions about the tested implementation than the fault model used with state machine testing.

It was shown in [Bochman a] that the partial-order test method provides complete fault coverage under the assumption that the tested implementation has the behavior that can be defined by a single partial order (without alternatives). That is, a transition of the POIOA model is implemented as a single transition in the implementation POIOA. An example of an implementation that does not satisfy this assumption would be an implementation that has the behavior of Figure 7(b) with a single output fault in the dashed transition. Such a fault is not detected by the test suite given above, and this faulty implementation cannot be described by a single partial order.

Conclusions

For describing the behavior of distributed systems with multiple interfaces, one needs the notion of partial order for the interactions at the different interfaces, since there is no total order defined for all the interactions of the system. We have compared different notions of partial-order specifications, including POIOA, ordering of collaborations, and MSC-Charts (also called Interaction Overview Diagrams). We propose the use of a variant of the latter, called Partial-Order-Charts (PO-Charts). We have shown that for the testing of distributed systems in respect to such behavior specifications, the partial-order tests of [Haar] can be used.

In the case that the PO-Chart is bounded, one can also derive an equivalent state machine and use FSM testing methods. We provided in this paper a preliminary comparison of testing complexities and fault models for these two testing approaches (partial-order tests and FSM testing methods). For systems with much concurrency, the partial-order tests are advantageous if one can assume that the fault model of partial-order testing is satisfied. This is presumably the case when the implementation uses message passing between the different system components to implement the order dependencies defined in the specification.

Fig. 1 :

 1 Fig. 1: (a) A partial order with two roles. (b) An equivalent state machine

  Figure 1(a) is of type i1.

  (a) for the behavior of the GetValues collaboration included in Figure 2(b).

Fig. 2 :

 2 Fig.2: The Test collaboration: (a) UML Collaboration diagram, (b) behavior definition containing three sub-collaborations

  (left): This chart defines the Test collaboration already shown in Figure 2(b) -with a small change of control flow.

Fig. 4 :

 4 Fig. 4: (left) PO-Chart representing the Test collaboration. (right) The same behavior with additional input-output interactions for testing.

  Figure 5(b) shows the corresponding state machine.

Fig. 5 :

 5 Fig. 5: (a) Example of a PO-Chart. (b) An equivalent state machine

Fig. 6 :

 6 Fig. 6: (a) Partial order of path p(2) based on the PO-Chart of Fig. 5(a). (b) Part of the infinite state machine equivalent to the PO-Chart of Fig. 5(a) without the dashed dependency.

Fig. 7 :

 7 Fig. 7: (a) A partial order with roles. (b) An equivalent state machine.

Acknowledgements

I would like to thank Guy Vincent Jourdan for many fruitful discussions on testing POIOA.


Alexandre Petrenko
email: petrenko@crim.ca

Omer Nguena Timo

S Ramesh
email: ramesh.s@gm.com

Test Generation by Constraint Solving and FSM Mutant Killing

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

The problem of fault model-based test generation from formal models, in this case Finite State Machines, is addressed. We consider a general fault model which is a tuple of a specification, conformance relation and fault domain. The specification is a deterministic FSM which can be partially specified and not reduced. The conformance relation is quasi-equivalence, as all implementations in the fault domain are assumed to be completely specified FSMs. The fault domain is a set of all possible deterministic submachines of a given nondeterministic FSM, called a mutation machine. The mutation machine contains a specification machine and extends it with mutated transitions modelling potential faults. An approach for deriving a test suite which is complete (sound and exhaustive) for the given fault model is elaborated. It is based on our previously proposed method for analyzing the test completeness by logical encoding and SMTsolving. The preliminary experiments performed on an industrial controller indicate that the approach scales sufficiently well.

Introduction

Fault model-based testing receives constantly growing interests of both researchers and test practitioners. Fault models are defined in the literature in a variety of ways [START_REF] Bochmann | Fault models in testing[END_REF].

The work [START_REF] Petrenko | Fault models for testing in context[END_REF] proposes to define a fault model as a tuple of a specification, conformance relation and fault domain. In the context of testing from finite state machines, the specification is a certain type of FSM. A conformance relation is specific to the FSM type and for completely specified deterministic machines it is equivalence, while for partially specified machines it is quasi-equivalence. The fault domain is a set of implementation machines, aka mutants, each of which models some faults, such as output, transfer and transition faults.

In the traditional checking experiment theory the fault domain is the universe of all machines with a given number of states and input and output alphabets of the specification, see, e.g., [START_REF] Moore | Gedanken experiments on sequential machines[END_REF][START_REF] Vasilevskii | Failure diagnosis of automata[END_REF][START_REF] Chow | Testing software design modeled by finite-state machines[END_REF][START_REF] Lee | Principles and methods of testing finite-state machines -a survey[END_REF][START_REF] Vuong | A novel approach to protocol test sequence generation[END_REF]. Checking experiments are in fact sound and exhaustive, i.e., complete tests. However, their size for realistic specifications is often considered too big for practical applications. To us, this is a price to pay for considering the universe of all FSMs. Intuitively, choosing a reasonable subset of this fault domain might be the way to mitigate the test explosion effect. As an example, if one considers the fault domain of mutants that model output faults, a test complete for this fault model is simply a transition tour. The fault domains intermediate to these two domains have not yet received in our opinion sufficient attention.

To define a fault domain which is a subset of the universe of all FSMs, one could explicitly enumerate mutants as in program or model-based mutation testing, see, e.g., [START_REF] Pomeranz | Test generation for multiple state-table faults in finite-state machines[END_REF][START_REF] Poage | Derivation of optimal test sequences for sequential machines[END_REF][START_REF] Demilli | Constraint-based automatic test data generation[END_REF][START_REF] Belli | Model-based mutation testing -Approach and case studies[END_REF] or avoid this enumeration by defining a fault domain as a set of all possible submachines of a given nondeterministic FSM, called a mutation machine [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF]. The mutation machine contains as a submachine a specification machine, additional transitions model potential faults. Several methods were developed for test generation using this fault model [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF][START_REF] El-Fakih | FSM-based testing from user defined faults adapted to incremental and mutation testing[END_REF]. All these methods are adaptations of classical checking experiments for a fault domain defined by a mutation machine. A checking experiment is in fact a complete test suite, however, the use of the state identification approach imposes limitations on the fault model. First, the specification machine must be completely specified and reduced, so that state identifiers exist. Second, the mutation machine was defined only for such specification machines. The existing methods are not applicable for partial specification machines and mutation machines derived from them. Finally, the state identification approach does not support iterative test generation with a mutation machine allowing the tester to terminate the process when a complete test suite for the given fault model is not yet obtained, but facing the scalability problems he is forced to make a compromise between fault coverage and test length.

Addressing the above limitations, in our recent work [START_REF] Petrenko | Multiple mutation testing from FSM[END_REF], we have developed a method for analyzing the test completeness for a fault model using a mutation machine. The analysis approach is based on logical encoding and SMT-solving, it avoids enumeration of mutants while still offering a possibility to estimate the test adequacy (mutation score). This method paves a road to a test generation approach which uses the results of the analysis to find tests which kill mutants survived a current test suite and iterates until a test suite complete for a given fault model with a mutation machine is obtained or the tester decides to terminate it earlier. Elaboration of the iterative test generation approach which is based on the test completeness analysis and does not require the specification machine to be complete and reduced is the main goal of this paper.

The remaining of this paper is organized as follows. Section 2 defines a specification model as well as a fault model. In Section 3, we develop an approach for complete test suite generation for a given fault model with a mutation machine. Section 4 reports some results of experimental evaluation of the approach. Section 5 summarizes our contributions and indicates future work. M is completely specified (complete FSM) if for each tuple (s, x)  S  I there exists transition (s, x, o, s)  T; M is partially specified (partial FSM), if for some (s, x)  S  I there is no transition, we say in this case that input x is not specified in state s. Let PM denote the set of all pairs (s, x) for which M has no transitions.

M is deterministic (DFSM) if for each (s, x)  S  I there exists at most one transition (s, x, o, s)  T; if there are several transitions for some (s, x)  S  I then it is nondeterministic (NFSM).

An execution of M from state s is a sequence of transitions forming a path from s in the state transition diagram of M. The machine M is initially connected, if for any state s  S there exists an execution from s0 to s. Henceforth, we assume that all FSMs are initially connected. An execution is deterministic if each transition (s, x, o, s) in it is the only transition for (s, x)  S  I; otherwise, i.e., if for some transition (s, x, o, s) in the execution there exists in it a transition (s, x, o, s) such that o ≠ o or s ≠ s, the execution is nondeterministic. Clearly, a DFSM has only deterministic executions, while an NFSM can have both.

A trace of M in state s is a string of input-output pairs which label an execution from s. Let TrM(s) denote the set of all traces of M in state s and TrM denote the set of traces of M in the initial state. Given sequence   (IO)*, the input (output) projection of , denoted I (O), is a sequence obtained from  by erasing symbols in O (I). Given a trace  in state s the input projection I is an input sequence defined in state s. We use M(s) to denote the set of all the input sequences defined in state s and M to denote the set of all the input sequences defined in state s0. Clearly, if M is complete then M = I*.

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

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

We define several relations between states in terms of traces. Given states s1, s2 of an FSM M = (S, s0, I, O, T), s1 and s2 are (trace-) equivalent, s1

≃ s2, if TrM(s1) = TrM(s2); s2 is trace-included into (is a reduction of) s1, s2  s1, if TrM(s2)  TrM(s1). M is reduced
if any pair of its states are distinguishable, i.e., for every s1, s2  S there exists   M(s1)  M(s2) such that outM(s1, ) ≠ outM(s2, ),  is called a distinguishing sequence for states s1 and s2, this is denoted s1 ≄ s2 or simply s1 ≄ s2.

We also use relations between machines. Given FSMs M = (S, s0, I, O, T) and N = (P,

p0, I, O, N), M  N if s0  p0; N ≃ M if s0 ≃ p0; N ≄ M if s0 ≄ p0.
In this paper, we assume that a specification machine is a DFSM which could be complete or partial, but all the implementation machines are complete DFSMs. This implies that we should use the quasi-equivalence relation [START_REF] Petrenko | Testing from partial deterministic FSM specifications[END_REF] as a conformance relation between implementation and specification machines. Given a DFSM M = (S, s0, I, O, T) and DFSM N = (P, p0, I, O, N), N is quasi-equivalent to M if M is a reduction of N.

Given a complete FSM M = (S, s0, I, O, T), a machine N = (S, s0, I, O, N) is a submachine of M if S  S and N  T. The set of all complete deterministic submachines of M is denoted Sub(M). Obviously, each machine in Sub(M) is a reduction of M; moreover, if M is deterministic then Sub(M) contains just M.

Fault Model

We define the so-called mutation machine for a given specification machine by generalizing the definition previously given only a complete specification FSM [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF][START_REF] Petrenko | Multiple mutation testing from FSM[END_REF][START_REF] El-Fakih | FSM-based testing from user defined faults adapted to incremental and mutation testing[END_REF] to allow the latter to be partially specified. In this definition we interpret inputs which are not specified in some states of A as don't care inputs. This implies that in a conforming implementation these inputs may cause transitions with an arbitrary output to any state in S.

The transitions T of the mutation machine can be classified as follows. The transitions in the set {(s, x, o, s)  (s, x, o, s)  T, (s, x)  PA} are called don't care transitions; we let DNCM denote this set. The transitions in T  N are common for M and A, these are unaltered transitions. Transitions in the set T \ (N  DNCM), are mutated transitions. Given (s, x)  S  I, we let Tsx denote the set of transitions from state s and input x in M. If Tsx is a singleton then its transition is called a trusted transition. The set Tsx is called a suspicious set of transitions if it is not a singleton, transitions in a suspicious set are called suspicious. Notice that don't care transitions are also treated as suspicious, since they can either compensate faults represented by mutated transitions and form a conforming mutant or expose wrong outputs.

We assume that all possible implementation machines for the specification machine

A constitute the fault domain Sub(M), the set of all deterministic submachines of the mutation machine

M of A. A submachine B  Sub(M), B ≠ A is called a mutant. All
mutants share all the trusted transitions, they may differ in suspicious and don't care transitions. In fact, transitions in suspicious sets are alternative and only one can be present in a deterministic mutant. Similarly, each mutant has a single transition for each pair (s, x)  PA, as all mutants are complete machines. A mutant B is conforming if it is quasi-equivalent to A, otherwise, it is nonconforming. We say that input sequence   A detects or kills the mutant B if B ≄ A.

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

Consider the example in Fig. 1.

Fig. 1.

A specification machine A and mutation machine M, where mutated transitions are depicted with dotted lines, don't care transitions with dashed lines; state 1 is the initial state.

The specification machine A in Fig. 1 is a partial DFSM, where input b is not specified in state 2, hence PA = {(2, b)}. The machine is not reduced, since state 3 is quasiequivalent to state 2. All the existing methods for test generation using mutation machines [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF][START_REF] El-Fakih | FSM-based testing from user defined faults adapted to incremental and mutation testing[END_REF] cannot be applied for such a machine, as they are based on the assumption that the specification machine is a complete and reduced machine, as required by the state identification approach.

The mutation machine M in Fig. 1 has three mutated transitions, one representing an output fault and the other two transfer faults. It also has 14 suspicious transitions, eight of them are don't care transitions.

The mutation machine M represents mutants as its deterministic submachines. Their number is given by the following formula:

|Sub(M)| = (s,x)SI|Tsx|
In our running example, the number of mutants is 8  2  2  2 = 64. In the extreme case, considered in classical checking experiments a fault domain is the universe of all machines with at most n states, the number of states in the specification machine, and the alphabets of it. The corresponding mutation machine becomes in this case a chaos machine with all possible transitions between each pair of states. We use Chaos(A, n) to denote such a mutation machine for A. The number of FSMs it represents is the product of the numbers of states and outputs to the power of the product of the numbers of states and inputs.

Mutation testing

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

For deterministic FSMs tests that kill a given mutant FSM can be obtained from the product of the two machines, see, e.g., [START_REF] Poage | Derivation of optimal test sequences for sequential machines[END_REF][START_REF] Pomeranz | Test generation for multiple state-table faults in finite-state machines[END_REF][START_REF] Petrenko | Testing from partial deterministic FSM specifications[END_REF]. This approach can also be used to check whether a given test kills mutants, but it requires mutant enumeration.

In this work, we develop an approach for complete test suite generation for the fault model A, ≃, Sub(M), where A can be a partial or complete FSM not necessary reduced. It is based on mutant killing, but does not check mutants one by one, thus avoiding their full enumeration.

Distinguishing automaton

Tests detecting mutants of the specification can be determined using a product of the specification and mutation machines obtained by composing their transitions as follows.

Definition 2 [START_REF] Petrenko | Multiple mutation testing from FSM[END_REF]. Given a specification machine A = (S, s0, I, O, N) and a mutation machine M = (S, s0, I, O, T) of A, a finite automaton D = (C  {}, c0, I, D, ), where C  S  S, and  is an accepting (sink) state is the distinguishing automaton for A and M, if it holds that We illustrate the definition using the specification and mutation machines in Fig. 1.

 c0 = (s0,
Fig. 2 presents the distinguishing automaton for A and M.

The accepting state defines the language LD of the distinguishing automaton D for A and M and possesses the following properties. First, LD  A, then all input sequences detecting each and every mutant belong to this language. Theorem 1. Given the distinguishing automaton D for A and M, if B ≄ A for some B  Sub(M), then there exists   LD, such that B ≄ A and  is a prefix of .

Notice that for any nonconforming mutant there exists an input sequence of length at most n 2 , where n is the number of states of the specification machine, since a distinguishing automaton has no more than n 2 states.

An input sequence  LD triggers an execution in the distinguishing automaton D which is defined by an execution in the specification machine A and some execution in the mutation machine M triggered by . The latter to represent a mutant must be deterministic. Such a deterministic execution of the mutation machine M defining an execution of the distinguishing automaton D to the sink state is called -revealing. An input sequence triggering revealing executions enjoys a nice property of being able to detect mutants. Moreover all its extensions also detect at least the same mutants.

Theorem 2 [START_REF] Petrenko | Multiple mutation testing from FSM[END_REF]. Given an input sequence   A such that  LD, an -revealing execution includes at least one mutated transition, moreover, each mutant which has this execution is detected by the input sequence .

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

Characterisation of mutants (un)detected by an input sequence

Consider an input sequence   A whose prefixes trigger -revealing executions. These executions characterize mutants detected by , since each of them defines a distinct set of suspicious transitions involved in the execution. Based on these sets we can build a constraint on transition sets of mutants undetected by . This can be achieved by using a distinguishing automaton constrained to a given input sequence. Let Pref() be the set of all prefixes of . We define a linear automaton (Pref(), , I, D), such that each prefix of  is a state, and (, x, x)  D if x  Pref().

Definition 3 [START_REF] Petrenko | Multiple mutation testing from FSM[END_REF]. For  = bababa in our running example, the -distinguishing automaton for A and M is shown in Fig. 3. Three prefixes of bababa, namely baba, babab and bababa belong to LD and trigger -revealing executions in the mutation machine. Any deterministic execution of the mutation machine with the input sequence baba is revealing if it uses the two suspicious transitions involved in the first execution, i.e., (3, b, 0, 3) and (3, a, 0, 3). We recall that trusted are used in every mutant submachine. Hence, every mutant which has both these suspicious transitions is detected by baba. Considering all eight executions, any mutant which has any of the eight sets of suspicious transitions is nonconforming and by bababa. Conversely, any mutant undetected by bababa must have mutated transitions such that do not form any of the sets defined by the listed executions. This property can be formalized as a constraint on suspicious transitions using conditional operators {=, } and logical operators {, } for constraint formulas.

Given a pair (s, x) S  I such that Tsx is a suspicious set of transitions, we introduce an auxiliary variable zsx which takes values from the indexes of the transitions of the mutation machine in Tsx.

Each revealing execution e of the mutation machine involving the set of suspicious transitions {t1, t2, …, tn} yields a clause ce = ((zs

1 x 1  t1)  (zs 2 x 2  t2)  …  (zs n x n  tn))
where si and xi are the source state and the input of transition ti for 1 ≤ i ≤ n. The clause ce is satisfied whenever zs i x i is not ti for some 1 ≤ i ≤ n. A solution of ce excludes at least one transition in e.

In the running example, the sets of suspicious transitions indexed with an integer identifier are: (1, a, 0, 1)1, (1, b, 0, 2)2, (2, a, 0, 2)7, (4, b, 0, 2)16. So we consider four variables z2b, z3a, z3b and z4a whose domains are T2b, T3a, T3b, and T4a, respectively. To simplify the presentation we use transition identifiers in constraints. The constraint formula for bababa consists of a preamble and eight clauses. The preamble (z2b  T2b)  (z3a  T3a)  (z3b  T3b)  (z4a  T4a) specifies the domains of the variables, thus constraining the possible solutions of the conjunction of the eight clauses to transitions of the mutation machine.

T2b = {(
((z2b  T2b)  (z3a  T3a)  (z3b  T3b)  (z4a  T4a)  ((z3a  12)  (z3b  14))  ((z4a  18)  (z2b  4)  (z3b  15))  ((z4a  18)  (z2b  6)  (z3b  15))  ((z4a  18)  (z2b  9)  (z3b  15))  ((z4a  18)  (z2b  11)  (z3b  15))  ((z3a  13)  (z3b  14))  ((z4a  18)  (z2b  8)  (z3a  13)  (z3b  15))  ((z4a  18)  (z2b  10)  (z3b  15))).
Clearly, the constraint always has a solution where values of variables determine all the unaltered transitions, but to find nonconforming mutants we need a solution if it exists which has at least one mutated transition. To this end, we add the constraint ((z3a  12)  (z3b  15)  (z4a  17)) excluding the solution defining the specification machine augmented with an arbitrary don't care transition, called a completed specification machine.

The final constraint formula for bababa is C(bababa)= ((z2b

 T2b  z3a  T3a  z3b  T3b  z4a  T4a)  ((z3a  12)  (z3b  14))  ((z4a  18)  (z2b  4)  (z3b  15))  ((z4a  18)  (z2b  6)  (z3b  15))  ((z4a  18)  (z2b  9)  (z3b  15))  ((z4a  18)  (z2b  11)  (z3b  15))  ((z3a  13)  (z3b  14))  ((z4a  18)  (z2b  8)  (z3a  13)  (z3b  15))  ((z4a  18)  (z2b  10)  (z3b  15))  ((z3a  12)  (z3b  15)  (z4a  17))).
The constraint C(characterizing the mutants undetected by an input sequence is the conjunction of a clause excluding all completed specification machines and the clauses generated for every revealing execution. Any existing constraint solver, e.g., Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF], could be used for satisfiability checking. A solution of C() if it exists is an assignment of the auxiliary variables. The mutant defined by such a solution includes the transitions specified by the solution along with all the trusted transitions of the mutation machine. Any nonconforming mutant detected by cannot be defined by any solution of C(), only conforming mutants can.

Algorithm 1 presents a procedure that builds a constraint CTS for a given test suite TS out of the constraints for each test in the test suite. In the running example, to solve the constraint formula C(bababa), we use the SMT solver Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] which finds the solution z2b = 11, z3a = 13, z3b = 15, z4a = 17. The solution defines a mutant with all trusted transitions, one don't care transition (2, b, 1, 4)11 and one mutated transition (3, a, 1, 3)13. The mutant is presented in Fig. 4. The mutant is nonconforming, which can be verified with the help of a distinguishing automaton obtained for the specification machine and the mutant also shown in Fig. 4.

Notice that the solver could find another solution of the C(bababa), namely, z2b = 11, z3a = 12, z3b = 15, z4a = 17 which defines a conforming mutant. Given an initial test suite TSinit, the question arises how to augment TSinit with new input sequences to detect all nonconforming mutants. We elaborate a complete test suite generation procedure in the next section.

Complete Test Suite Generation

We are given a test suite TSinit  A and a fault model A, ≃, Sub(M). We want to add test cases to TSinit to obtain a complete test suite. Constraints defined in the previous section can be used to analyse the completeness of a test suite, elaborated in our previous work [START_REF] Petrenko | Multiple mutation testing from FSM[END_REF]. If the constraint for a test suite has no solution or the first solution computed by a solver defines a nonconforming mutant, we can immediately assert the incompleteness of the test suite. If however the solution defines a conforming mutant, the search continues such that the mutant will not be found again in a new round of satisfiability checking. This process iterates until no new solution is found or the generated solution defines a nonconforming mutant. A witness nonconforming mutant can be used to determine a test case which detects the mutant. A new test can kill other nonconforming mutants. Hence the constraints generated by this test should be added to the ones of the current test suite. The search terminates when the current constraint is unsatisfiable which indicates that the test suite is complete. The test generation procedure is formalized in Algorithm 2.

The algorithm has two loops. The coverage analysis loop includes statements in lines 7 to 9 and the test generation loop includes statements at lines 4 to 13. The former loop is nested in the latter. When the current test suite is not complete, the execution of the test generation loop augments (in line 4) it with a new test case and updates the constraint of the current test suite with that of the generated test case. Then the coverage analysis loop is executed checking the completeness of the updated test suite, searching for a new nonconforming mutant. To this end, constraints excluding conforming mutants defined by the found solutions are iteratively added to the current constraint. The procedure terminates when the resulting constraint is unsatisfiable, indicating that the Proof. The procedure TestSuiteGen terminates as the test generation loop terminates. It does so because a mutation machine has a finite number of submachines and the solution defining a particular mutant is generated at most once. According to Theorem 2, the computed tests are revealing input sequences. On termination of the procedure the final constraint characterizing undetected mutants excludes all conforming mutants and it is unsatisfiable. Based on Theorem 3 we have that the test suite returned by the procedure is complete.

To generate a complete test suite for the running example we consider the initial test suite TSinit = {bababa}, used in Section 3. The procedure TestSuiteGen also generates a complete test suite starting when the initial test suite contains just an empty input sequence.

In the next section we present experimental results obtained with a prototype tool.

Experimental results

We have developed a prototype tool implementing the proposed method for complete test suite generation. In this section we present the tool and some experimental results using it.

Prototype tool

The prototype tool is composed of four modules: an I/O module, a completeness checking module, a test generation module and a module for solver execution. The I/O module converts input data into an internal representation for processing and obtained results into a human-readable format. To this end, it implements an ANTLR-based parser [START_REF] Parr | The definitive ANTLR 4 reference[END_REF] to interpret the mutation machine specified in a text format; it also parses the output of SMT solver Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] to extract a solution and builds a mutant. The completeness checking module builds -distinguishing automata, determines revealing executions of the mutation machine and generates constraints for the solver. The test generation module iteratively calls the former module. The prototype can also be used with other SMT solvers compatible with the SMT-LIB 2.0.

For the experiments we use a desktop computer with the following settings: 3.4 Ghz Intel Core i7-3770 CPU, 16.0 GB of RAM, Z3 4.3.2, and ANTLR 4.5.1.

Test Generation for an Automotive Controller

We consider as a case study an automotive controller of the air quality system (HVAC), which we also used in our previous work [START_REF] Petrenko | A method and tool for test optimization for automotive controllers[END_REF][START_REF] Petrenko | Multiple mutation testing from FSM[END_REF]. The functionality of the controller is to set an air source position depending on its current state and input from the environment.

The controller initially specified as a hierarchical Simulink Stateflow model is converted into an FSM with 14 states, 24 inputs and 24 x 14 = 336 transitions.

Several mutation machines were used in the experiments. The first one Mhvac was obtained by adding 46 mutated transitions to the specification machine (details are available in [START_REF] Petrenko | Multiple mutation testing from FSM[END_REF]). The formula in Section 2 gives the number of mutants 3 12 × 2 17 = 69,657,034,752.

The other mutation machines were built by adding more mutated transitions to Mhvac.

In particular, 20, 100, 428, 764 and 1000 mutated transitions were randomly added, resulting in five more mutation machines, M+20, M+100, M+428, M+764 and M+1000. Tab. 1 presents the numbers of mutated transitions, mutants, generated tests and the computation time. Each generated mutant was non-conforming, so their number coincides with that of the tests, conforming mutants were never generated. The third column of Tab. 1 represents the average values for 30 mutation machines randomly generated by adding 20 mutated transitions to Mhvac. The experimental results indicate that the approach scales sufficiently well on a typical automotive controller even with the large number of mutants.

Conclusions

In this paper we focused on generation of a complete test suite detecting all nonconforming implementations in a fault domain defined by a mutation machine. A mutation machine is a nondeterministic FSM, interpreted as a compact representation of a set of deterministic implementations of a system represented by a partially or completely specified FSM. Each deterministic submachine of the mutation machine models an implementation.

We proposed a method for generating a complete test suite which avoids complete enumerations of nonconforming mutants. The method iteratively builds constraints specifying mutants undetected by an incomplete (possibly empty) test suite and uses a solution of constraints generated by a solver to determine an undetected mutant from which a new test case is selected and derives an augmented constraint for a next iteration step until the obtained constraint becomes unsatisfiable.

While it enumerates all conforming mutants, which exist mostly when the specification is partial or unreduced FSM, it does not generate all nonconforming ones. The experimental results with a prototype tool which uses the SMT solver Z3 indicate that the number of generated nonconforming mutants reaches only a small percentage of all mutants represented by a mutation machine.

Novelty of the contributions of this paper are as follows. The proposed approach allows one to construct checking experiments for FSMs which are not necessarily complete and reduced without using any state identification facility such as characterization sets, distinguishing sequences, and state identifiers, as opposed to traditional checking experiment approaches. Thus, we demonstrate that it is possible to construct checking experiments using logical encoding and constraint solving instead of classical methods based on state identification [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF][START_REF] El-Fakih | FSM-based testing from user defined faults adapted to incremental and mutation testing[END_REF]. Moreover, test completeness is guaranteed for a predefined subset of the universe of all FSMs with a given number of states, represented by a mutation machine. Compared to all previous work on the use of mutation machine [START_REF] Grunsky | Design of checking experiments with automata describing protocols[END_REF][START_REF] Petrenko | Test suite generation for a FSM with a given type of implementation errors[END_REF][START_REF] Koufareva | Test generation driven by user-defined fault models[END_REF][START_REF] Petrenko | Multiple mutation testing from FSM[END_REF][START_REF] El-Fakih | FSM-based testing from user defined faults adapted to incremental and mutation testing[END_REF], we have generalized its definition to make it applicable to partially defined specification machines. The method proposed in [START_REF] El-Fakih | FSM-based testing from user defined faults adapted to incremental and mutation testing[END_REF] is only applicable to mutation machines which satisfy the following assumption. If a transition of the specification machine becomes suspicious in the mutation machine then the latter has all possible (thus chaotic) suspicious transitions from the start state of the transition caused by the same input. The method also requires the specification machine be completely specified. Compared to that work, our method is applicable to arbitrary mutation machines, while the specification machine is allowed to be partially specified.

Another interesting feature of the approach is that it is iterative and allows the tester to obtain an incomplete test suite for which fault coverage can be estimated (as discussed in [START_REF] Petrenko | Multiple mutation testing from FSM[END_REF]) when facing the scalability problems he is forced to make a compromise between fault coverage and test length.

The experiments indicate that the proposed approach may scale sufficiently well, though, more experiments with industrial size specifications are needed. Our current work focuses on extending the approach to FSMs with symbolic inputs and outputs [START_REF] Petrenko | Checking experiments for symbolic input/output finite state machines[END_REF] and eventually to a more general type of EFSM [START_REF] Petrenko | Confirming configurations in EFSM testing[END_REF].

  In the case where M = Chaos(A, n) a complete test suite is called n-complete. This notion coincides with the classical notion of checking experiments for the fault domain consisting of FSMs with at most n states[START_REF] Hennie | Fault detecting experiments for sequential circuits[END_REF][START_REF] Lee | Principles and methods of testing finite-state machines -a survey[END_REF][START_REF] Petrenko | Fault models for testing in context[END_REF].

Fig. 2 .

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

  Given a specification machine A = (S, s0, I, O, N), input sequence   A, and mutation machine M = (S, s0, I, O, T), a finite automaton D = (C  {}, c0, I, D, ), where C Pref()  S  S, and  is a designated sink state is the distinguishing automaton for A and M if it holds that  c0 = (, s0, p0)  For any (, s, t)  C and x  I, such that x  Pref(), ((, s, t), x, (x, s, t))  D, if there exist (s, x, o, s)  N, (t, x, o, t)  T, such that o = oand ((, s, t), x, )  D, if there exist (s, x, o, s)  N, (t, x, o, t)  T, such that o  o.

Fig. 3 .

 3 Fig. 3. The -distinguishing automaton D for the specification A machine and mutation machine M in Fig. 1, where = bababa. There are eleven executions of the mutation machine listed below which are defined by five executions of the -distinguishing automaton reaching the sink state in Fig. 3. Suspicious transitions are in bold font and the others are trusted transitions. Transitions of the specification are underlined. Three executions, executions 9, 10, and 11, are non-deterministic. The first eight executions belong to mutants detected by bababa.1. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 3)(3, a, 0, 3) 2. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, b, 1, 2) 3. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, b, 1, 1) 4. (1, b, 0, 2)(2,a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, b, 1, 3) 5. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, b, 1, 4) 6. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 3)(3, a, 1, 3)(3, b, 0, 3)(3, a, 1, 3) 7. (1, b, 0, 2)(2, a, 0, 3)(3, b, 0, 4)(4, a, 1, 2)(2, b, 0, 3)(3, a, 1, 3)

  2, b, 0, 2)3, (2, b, 1, 2)4, (2, b, 0, 1)5, (2, b, 1, 1)6, (2, b, 0, 3)8, (2, b, 1, 3)9, (2, b, 0, 4)10, (2, b, 1, 4)11}, T3a = {(3, a, 0, 3)12, (3, a, 1, 3)13}, T3b = {(3, b, 0, 3)14, (3, b, 0, 4)15} and T4a = {(4, a, 1, 1)17, (4, a, 1, 2)18}. The remaining trusted transitions are indexed as follows:

Algorithm 1 . 3 .

 13 Build_Constraint Input: TS, a test suite A, a specification machine M, a mutation machine for A Output: CTS, a constraint specifying mutants undetected by tests in TS 1. CTS = True 2. For each input sequence   TS, (a) Determine the -distinguishing automaton Dand set c = True (b) For each -revealing execution e of the mutation machineset cc ce, where ce is the disjunction of constraints excluding the suspicious transitions in e (c) CTS = CTS  c 3. Add to CTS the constraints restricting the value of the variables to their domain and excluding A 4. Return CTS Theorem Let CTS be a constraint specifying undetected mutants by the test suite TS. TS is complete w.r.t. the fault model A, ≃, Sub(M) if and only if CTS is unsatisfiable or every solution of CTS defines a conforming mutant.

Fig. 4 .

 4 Fig. 4. A nonconforming mutant defined by a solution of the constraint for TS = {bababa} and the distinguishing automata for the mutant and the specification A.

  is complete or the solver generates a solution defining a nonconforming mutant. In this case, the execution of the test generation loop augments the current test suite with a new test killing the mutant. It is determined by finding the shortest path to the sink state of the distinguishing automaton of the mutant and the specification.

Algorithm 2 .Goto 4 Theorem 4 .

 244 TestSuiteGen Inputs: TSinit, an initial test suite A, a specification machine M, a mutation machine for A Output: TS, a complete test suite 1. TS =  2. C = True 3. TSnew = TSinit 4. TS = TS ∪ TSnew 5. Let Cnew = Build_Constraint(TSnew, A, M) be a constraint specifying mutants undetected by TSnew 6. Let C = C  Cnew 7. Check the satisfiability of C by calling a solver 8. if C is "unsatisfiable" then terminate with "TS is a complete test suite" 9. Let N be a mutant defined by a solution of C obtained by a solver 10. if N is conforming then set C = C  CN where CN is the constraint that excludes N and Goto 7 11. Determine D, the distinguishing automaton of A and N 12. Let TSnew = {}, where   LD 13. Procedure TestSuiteGen always terminates with a complete test suite.

2 .

 2 Procedure TestSuiteGen first goes into the test generation loop which builds Cnew = C(bababa), updates TS and C to {bababa} and C(bababa) defined in Section 3.2. Then the coverage analysis loop finds the solution of C defining the nonconforming mutant in Fig 4. The test baa is then generated by determining the only shortest path to the sink state in the distinguishing automaton for the specification and the mutant, so TSnew becomes {baa}. Then the constraint Cnew = C(baa) = (z3a ≠ 13) is generated in line 5, TS becomes {bababa, baa} and C = C(bababa)  C(baa). The solution of C defines a nonconforming mutant killed by the test babaaba, the input sequence of the shortest path to the sink state the distinguishing automaton for the new nonconforming mutant and the specification, then TSnew becomes {babaaba}. The constraint Cnew = C(babaaba) = (((z3a ≠ 12)  (z3b ≠ 14))  ((z3a ≠ 13)  (z3b ≠ 14))  ((z4a ≠ 18)  (z3b ≠ 15))) is generated; it includes one clause for each of the three -revealing executions triggered by babaaba. TS becomes {bababa, baa, babaaba} and C = C(bababa)  C(baa)  C(babaaba). C is satisfiable and the procedure iteratively generates only conforming mutants augmenting C each time with a constraint excluding the last conforming mutant. No additional tests are generated. The conjunction of C with the eight constraints excluding eight conforming mutants is unsatisfiable. The procedure returns a complete test suite TS = {bababa, baa, ba-baaba}. Notice that it generated only ten out of total 64 mutants.

Definition 1 .

 1 Let A = (S, s0, I, O, N) be a specification DFSM with the set of stateinput pairs PA for which A has no transitions. A complete NFSM M = (S, s0, I, O, T) is a mutation machine of A, if {(s, x, o, s)  (s, x)  PA, o O, s S}  T and A is a submachine of M.

Acknowledgements. This work is supported in part by GM, NSERC and MEIE of Gouvernement du Québec.


Eder C M Gomes

Paulo R P Amora
email: paulo.amora@lsbd.ufc.br

Elvis M Teixeira
email: elvis.teixeira@lsbd.ufc.br

Antonio G S Lima

Felipe T Brito
email: felipe.timbo@lsbd.ufc.br

Juliano F C Ciocari
email: juliano.ciocari@hp.com

Javam C Machado
email: javam.machado@lsbd.ufc.br

UTTOS: A Tool for Testing UEFI Code in OS Environment

Keywords: UEFI, Unit Test, C, Code Coverage, Embedded Systems

Unit tests are one of the most widely used tools to assure a minimal level of quality and compliance during development. However, they are not used in many projects where development takes place at low-level contexts. The main reason is that unit test development itself demands more time and becomes expensive in this context and tools that assist test creation are rare or absent. In UEFI development this scenario matches the reality of most teams and unit testing as well as other testing techniques are often not used. To address this fault we propose UTTOS, a tool that parses EDKII build configuration files, mocks the UEFI-specific functions for C development and enables UEFI test suite code to run in the operating system. We show that UTTOS is able to run the test suit in the operating system and save development time.

Introduction

Testing has being often considered the crucial phase in the process of creating high quality software systems and most development frameworks include functionality to assist the use of some automatic testing strategy. In low level systems such as embedded systems, BIOS and device drivers development the situation is much less well established. Here, requirements are often fixed by protocol specification. This decreases complexity and most testing is basically checking for conformity to the protocols. On the other hand automated testing is not generally easy here since the code is targeted to run in devices different from the developer's workstation often through the use of cross compiling. Tools to assist the generation of automatic tests are rare in such platforms.

UEFI (Unified Extensible Firmware Interface) is the current specification for the interface between the platform firmware and the operating system, it is meant to eventually replace the BIOS (Basic Input Output System) and addresses many of it's limitations. First of all, the BIOS development is made in assembly language thus the complexity of keeping it modularized and maintainable was a big issue, BIOS runs on 16 bit mode so the amount of memory usable is very limited. In UEFI there is a call stack and most of the development is done in C, also the execution environment is 32bit or 64bit depending on the processor architecture. These features make it a much richer platform with many application possibilities, therefore going beyond the basic task of initializing the hardware and calling the OS loader [START_REF] Zimmer | Beyond BIOS: developing with the Unified Extensible Firmware Interface[END_REF] [START_REF]UEFI Forum: UEFI Specification 2.6[END_REF].

UEFI also enables OEMs (Original Equipment Manufacturer) to bundle applications and drivers with the machine itself then providing a minimal OS-like environment. But with the greater flexibility provided by UEFI and the variety of software that is being written to that platform comes complexity, and then the need for robust development and quality assurance practices. The issue at hand is that the DXE (Driver Execution Environment) code is targeted to run in the pre-boot phases, so it is usually written and compiled in a workstation then run in the target machine in order to be tested and then brought back to the developers workstation to be validated and debugged.

It is possible to identify two alternatives to use automated test strategies for UEFI software: to develop or use testing tools that run in the DXE or develop tools to mimic the DXE by mocking its basic functions. We favour the second approach in order to run the code in to be tested in the OS context, thus overcoming the lack of test tools available by enabling DXE code to be run in the OS by using unit tests with the external dependencies, such as the functions in the boot services table, mocked.

Since the code is run in the OS, developers and testers have access to many other tools that exist to help them ensure code quality, such as code coverage and other tools that are not available in UEFI environment.

Contributions. In this paper we discuss a tool that enables unit tests for UEFI code to run as standard operating system programs and show a case study with a compliant driver to evaluate it's benefits. During the discussion of the driver implementation ideas about how to use the test suit to minimize the number of times a developer needs to rewrite the machine's flash memory and protocol conformity.

Section 2 describes the state-of-the-art techniques for unit testing of DXE code. It shows that the existing techniques are not extensible, and do not allow for further code metrics. In Section 3, the proposed tool and the way it works is explained. Section 4 describes the case study and presents results. Finally, Section 5 concludes this paper and proposes future work.

Related Work

There are several works advocating the use of unit testing in the development of software [START_REF] Greening | Test Driven Development for Embedded C. Pragmatic Bookshelf[END_REF], [START_REF] Myers | The art of software testing[END_REF], [START_REF] Pressman | Software Engineering: A Practitioner's Approach[END_REF]. While in UEFI there are no specific unit test tools, there are validation tools for firmwares and drivers such as PI SCT [START_REF]UEFI Forum: Platform Initialization Self Certification Test 2.4B[END_REF] provided by the UEFI open source community, FWTS [1] and Chipsec [START_REF]CHIPSEC: Platform Security Assessment Framework 1.2.2[END_REF]. All of these run functional tests.

The field that most closely resembles tasks accomplished in UEFI development is that of embedded systems development, mainly because of the use of C and the fact that many operating system services may not be available. In that context there are some tools that try to make test-driven development more pleasant, Unity [START_REF] Vandervoord | ThrowTheSwitch.org[END_REF] for example, provides several assertion macros to guide unit test development for C modules. CMock [START_REF] Vandervoord | ThrowTheSwitch.org[END_REF] parses the included header files and checks for function declarations to provide mocked or stub implementations of them, this allows one to remove the dependencies on the functionality of third party modules avoiding effects of their behaviour in the results of the tests. Ceedling [START_REF] Vandervoord | ThrowTheSwitch.org[END_REF] is a build management system that integrates those tools and allow custom configurations through its project descriptor file.

EDKII (EFI Development Kit)[10] module development uses the following structure: At first, a package is created. Inside the package are the platform descriptor file (.dsc), responsible for describing all the dependencies used by the modules in the platform. The declaration file (.dec) contains all the include paths used by the modules, as well as GUID declarations for protocol communication. Then, each module inside the package, be it an application or driver, has its descriptor file (.inf), which contains information about the module such as compiled source codes, libraries, dependencies and protocol GUIDs published or consumed, separated into sections, such as [Packages], [Guids] and [Protocols].

According to Saadat, H. [START_REF] Saadat | Design and development of an automated regression test suite for UEFI[END_REF], hardware diagnostics are not effective in detecting code errors, therefore, UEFI code must be tested from a software perspective. Also, it is mentioned that only one test tool may be insufficient to cover all the phases in UEFI, which is why a combination of tools must be used.

There are some groups interested in testing embedded systems code during development and UEFI code as well. However, the UEFI approach to unit testing still uses the UEFI environment, making the use of debbugers and other OS specific tools impossible. Our solution, called UTTOS, aims to execute the code in the OS, mocking UEFI specific dependencies, thus allowing unit tests to be run in the same development environment and enabling use of other tools, like code coverage tools.

The UTTOS Solution

It is possible to write unit tests that run in UEFI through the use of CuTestLib [START_REF] Jalis | CuTest: C Unit Testing Framework 1.5[END_REF] or some other similar tool. However, the fact that the firmware run in a processless, single threaded fashion poses a number of limitations. If there is a problem with a statement and the code breaks in a way that should generate a segmentation fault in an OS context, the firmware is likely to just freeze, leaving the test developer without any feedback or clue to what happened. This is an issue that may happen to even more sophisticated test approaches that involve transmission of test results over network or serial port.

Those limitations and the extra complexity needed to achieve simple tasks like writing test results to a screen or to a file in the firmware level makes good practices like test-driven development often impractical or even absent in many projects.

To avoid these problems, we propose an UEFI Test Tool for Operating Systems (UTTOS). UTTOS addresses this issue by enabling code that was written to the EDKII platform and meant to run in the DXE context to be compiled and executed as an ordinary executable in the operating system of the developer platform. The unit tests generated in this fashion are much more flexible as they enable the test developer to use the full stack of debugging tools that are available for C. If there is a segmentation fault, for example, the developer can make use of the core dump generated by the operating system and a debugger, like GDB, without any specialized hardware-aided solution.

UTTOS strategy for running EDKII in the operating system runtime consists of looking for dependencies declared in the descriptor of the module being compiled, that is our UEFI driver or application, and then generates stub versions of the EDKII specific functions. The developer is responsible for configuring the expected arguments and return values of these functions for each test suite. This effort is not repetitive since the most used functions can be reused.

The main tool used by UTTOS is Ceedling, that tracks dependencies and have a configuration file feature-rich enough to permit customization of the whole process. Ceedling itself makes use of a few other open source tools, namely: CMock for mocking and Unity for test creation. UTTOS acts in the beginning of the process parsing the EDKII build files and generating the Ceedling configuration accordingly. And as we are in an operating system environment we also include Gcov for coverage evaluation. A more detailed view of the UTTOS workflow is described in Fig. 1. It first the module descriptor file and gathers information about the dependencies and the consumed resources. The resources in a UEFI firmware are identified by a Globally Unique Identifier (GUID). In the process of constructing the dependency tree, the descriptor files and declaration files (.dec extension) of other modules are read to gather all the required headers, include paths and GUIDs used by the current module. From this procedure, two files, guids.h and guids.c are output for use in the test suite compilation.

The next step is the generation of a Ceedling project where the module descriptor is located. The project is created using Ceedling's default configurations for a C project. After this, the Ceedling project descriptor is modified by UT-TOS, that adds the include paths for the dependencies, the source files to be built, the suitable compiler options and the instructions to CMock on which functions have to be mocked.

The final step is the placing of the generated files inside the created test suite to allow correct code compilation. The test suite is generated with two stub functions for setup and clean up. At this stage, it is ready to use. Ceedling manages the test suite and its dependencies, assuring transparent use of the UEFI code. If further configuration is needed, the project is customizable after UTTOS executes.

With the suite ready to be executed, the user can add individual test cases with custom assertions and control flows. The user can also specify the expected parameter and return values for the mocks created by CMock to strengthen the tests coverage further. Ceedling also monitors suite execution and reports formatted results, allowing the developer to ensure quickly that the written code is working.

Case Study

As a case study, a simple UEFI DXE driver fully compliant with the UEFI Driver Model was developed. The driver installs a protocol and an associated GUID to the UEFI runtime that provides a service for UEFI applications to convert roman numbers in string format to a regular C integer type. Because one of the most interesting scenarios that requires testing in the context of driver development is the process of providing a new protocol, we decided to go with an algorithm that, although simple, provides a good number of test cases as there are a number of possibilities for invalid roman numbers.

The driver was developed under the EDKII version 2.6 source tree in a Debian GNU/Linux 8 machine using the GCC compiler version 4.9.

This process starts by creating a set of functions called the Driver Binding Protocol [START_REF] Corporation | Uefi driver writer's guide[END_REF]. These functions are responsible for querying all the nodes of the UEFI service database checking if any of these corresponds to a device that the driver can control. This query process is performed by the Supported function and it has to return a success status for a device that is suitable for the driver and an unsupported status otherwise. If such a device is found, the Start function is called to initialize the driver data structures and the device itself.

If for some reason the user wants to remove the driver from the environment, the driver binding protocol also provides the Stop function, that is responsible for releasing all the resources that were allocated by Start, and for the removal of any protocol installed by the driver and their respective GUIDs. Stop makes sure the services provided by the driver will not appear to be available to applications after it is unloaded.

In UEFI, all the available memory is shared as a single address space to all drivers and applications. Therefore, an error in any of these functions is likely to freeze the whole system. Consequently, all these steps must be previously validated before one takes the job of rewriting the firmware of the machine to check if the driver works as expected. Here is where the ability to run unit tests in the developer's workstation as a prior step shows it's value, since most of the trivial mistakes can be avoided before actually touching the target hardware.

The Gcov [START_REF] Ledru | Gcovr. gcovr.com[END_REF] utility was used to evaluate the code coverage of the tests performed. Gcov is another python tool that translates the symbols generated by GCC to human readable results allowing a nice html format to be output. Fig. 2 shows the test coverage results for our case study. It can be seen that most of the control flows were covered. The results of the individual test cases were all positive and they have successfully assured that the driver binding process would occur without errors when embedded in the machine's firmware. This is important in the sense that it allows the developer to be concerned with the driver's functionality correctness straight from the first firmware writing, and not with these initial service and protocol setup that often takes a considerable time in real world projects.

In comparison with the approach of testing the code in DXE environment directly, the first major benefit observed is that ones does not have to rewrite the firmware in the flash memory so many times to test code, a process that is time consuming and decreases flash memory life time. Additionally, code coverage measuring tools are one of many that are not available in the DXE phase so these results would not the easily achieved today.

Conclusion and Future Works

In this paper, we proposed UTTOS, a tool that makes use of a set of OS-based test tools to test UEFI code. It adapts the test framework to be able to run UEFI code as a regular operating system executable with that UEFI specific functions mocked. A case study was also conducted, with the implementation of an example driver in order to test the whole process of driver installation, production usage and removal to simulate as close as possible the reality of device driver development.

In the development time it was observed a decrease in the need for rewriting the machine's firmware and the ability to focus in functionality rather than in protocols conformity which can in practice be, using UTTOS, considered to be boilerplate code.

During the experiments, we were able to not only create unit tests, but to make use of code coverage, as we were running the code in an OS-based environment. This would not be possible by running the code only in UEFI DXE phase.

For future works, it is intended to integrate this tool with an IDE. Support for other code metrics, such as cyclomatic complexity and nesting depth can also be considered.

Fig. 1 .

 1 Fig. 1. Workflow of UTTOS, from module descriptor to test suites.

Fig. 2 .

 2 Fig. 2. Code coverage report of the implemented driver.

Acknowledgements. This publication is the result of a project promoted by the Brazilian Informatics Law (Law No. 8248 of 1991 and subsequent updates) and was developed under the Cooperation Agreement 11/2016 between Federal University of Ceara and HP Brazil Industry and Trade Electronic Equipment Ltda. This research was also partially supported by LSBD/UFC.