Jan Peleska

Artur Honisch
email: artur.honisch@daimler.com

Florian Lapschies

Helge Löding
email: hloeding@verified.de

Peer Smuda Hermann Schmid
email: hermann.s.schmid@daimler.com

Elena Vorobev

Cornelia Zahlten

A Real-World Benchmark Model for Testing Concurrent Real-Time Systems in the Automotive Domain

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

Introduction

Model-based testing. Automated model-based testing (MBT) has received much attention in recent years, both in academia and in industry. This interest has been stimulated by the success of model-driven development in general, by the improved understanding of testing and formal verification as complementary activities, and by the availability of efficient tool support. Indeed, when compared to conventional testing approaches, MBT has proven to increase both quality and efficiency of test campaigns; we name [START_REF] Löding | Timed moore automata: test data generation and model checking[END_REF] as one example where quantitative evaluation results have been given. In this paper the term model-based testing is used in the following, most comprehensive, sense: the behavior of the system under test (SUT) is specified by a model elaborated in the same style as a model serving for development purposes. Optionally, the SUT model can be paired with an environment model restricting the possible interactions of the environment with the SUT. A symbolic test case generator analyzes the model and specifies symbolic test cases as logical formulae identifying model computations suitable for a certain test purpose (also called test objective). Symbolic test cases may be represented as LTL formulas of the form Fφ, expressing that finally the test execution should produce a computation fragment where the test purpose specified by φ is fulfilled.

Constrained by the transition relations of SUT and environment model, a solver computes concrete model computations which are witnesses of symbolic test cases Fφ. More formally, solvers elaborate solutions of so-called bounded model checking instances

tc(c, G) ≡ def c-1 i=0 Φ(σ i , σ i+1 ) ∧ G(σ 0 , . . . , σ c ) (1)
In this formula σ 0 represents the current model state and Φ the transition relation associated with the given model, so any solution of ( 1) is a valid model computation fragment of length c. Intuitively speaking, tc(c, G) tries to solve LTL formula Fφ within c computation steps, starting in model pre-state σ 0 , so that each step is a valid model transition, and test purpose φ is encoded in G(σ 0 , . . . , σ c ).

The inputs to the SUT obtained from these computations are used in the test execution to stimulate the SUT. The SUT behavior observed during the test execution is compared against the expected SUT behavior specified in the original model. Both stimulation sequences and test oracles, i. e., checkers of SUT behavior, are automatically transformed into test procedures executing the concrete test cases in a software-in-the-loop or hardware-in-the-loop configuration.

Observe that this notion of MBT differs from "weaker" ones where MBT is just associated with some technique of graphical test case descriptions. According to the MBT paradigm described here, the focus of test engineers is shifted from test data elaboration and test procedure programming to modeling. The effort invested into specifying the SUT model results in a return of investment, because test procedures are generated automatically and debugging deviations of observed against expected behavior is considerably facilitated because the observed test executions can be "replayed" against the model.

Objectives and Main Contributions. The main objective of this article is to present a "real-world" example of a model used in the automotive industry for system test purposes. The authors have experienced the "validation powers" of such models with respect to realistic assessment of efforts in model development, and with respect to the tool capabilities required to construct concrete model computations -i. e., test data -for given symbolic test cases. We hope to stimulate a competition of alternative methods and techniques which can be applied to the same benchmark model in order to enable objective comparison of different approaches. For starting such a competition we also give an overview of the methods and algorithms applied in our tool and present performance values, as well as test generation results to be compared with the results obtained using other methods and tools.

To our best knowledge, comparable models of similar size, describing concurrent real-time behavior of automotive applications and directly derived from industrial applications are currently not available to the public, at least not for application in the MBT domain. As a consequence, no systematic approach to benchmark definitions has been made so far. We therefore suggest a simple classification schema for such benchmarks, together with a structuring approach for the test suites to be generated. While this article can only give an overview of the model, detailed information are publicly available on the website [START_REF] Peleska | Embedded systems testing benchmark[END_REF] (www.mbt-benchmarks.org).

Overview. In Section 2 we present an introductory overview over the benchmark model. In Section 3 the methods applied in our test generator are sketched, with the objective to stimulate discussions about the suitability of competing methods. The representation of symbolic test cases as constraint solving problems (CSP) is described, and we sketch how these CSPs are solved by the test generation engine in order to obtain concrete test stimulations to be passed from the test environment to the SUT.

In Section 4 we propose a classification of benchmarks which are significant for assessing the effectiveness and performance of model-based testing tools. This classification induces a structure for reference test suites. In Section 5 a test generation example is presented.

Since the complete model description and the detailed explanation of algorithms used for test case generation and CSP solving is clearly beyond the page restriction of this submission, interested readers are referred to [START_REF] Peleska | Embedded systems testing benchmark[END_REF], where the material is presented in more comprehensive form, and the model can be downloaded in XMI format and as a model file for the EnterpriseArchitect CASE tool [START_REF] Systems | Enterprise architect 8.0[END_REF] which was used to create the model and its different export formats. Additionally an archive may be downloaded whose files allow to browse through the model in HTML format. The symbolic test cases used in the performance results are also available, so that the sequence of CSP solutions created by our test case generator can be repeated by other tools. The current benchmark evaluation results, including test generations performed with our tool are also published there.

Related Work.

Benchmarking has been addressed in several testing domains. For "classical" software testing the so-called Siemens benchmarks [START_REF] Harrold | Siemens programs, hr variants[END_REF] provide a collection of C programs with associated mutations rated as representative for typical programming bugs. A more comprehensive discussion and review of available software testing benchmarks is given in [START_REF] Lu | Bugbench: Benchmarks for evaluating bug detection tools[END_REF]. In [START_REF] Memon | [END_REF] an initiative for event-driven software testing benchmarks has been launched.

In the field of model-based embedded systems testing only very few benchmarks are currently available, and none of them appear to describe comprehensive industrial control applications. In [START_REF]Jeppu: A benchmark problem for model based control systems tests -001[END_REF] a Matlab/Simulink model for a flight control system has been published. According to our classification proposed in Section 4 it addresses the benchmark category test strength benchmarks: A set of test cases is published which have been generated using random generation techniques inspired by Taguchi methods. To analyze the strength of test cases, several mutants of the model have been provided which may either be executed in Simulink simulation mode or as C programs generated from the mutant models. Since random test generation techniques on the input interface to the SUT are used, the model coverage achieved is only analyzed after test suite execution. As a consequence, no test generation benchmarks suggested in Section 4 are discussed. All existing benchmarks we are aware of may be classified as test strength benchmarks. Our proposition of test generation benchmarks seems to be a novel concept.

While our test generation approach relies on constraint solvers to find testinput-data, search-based testing techniques use randomized methods guided by optimization goals. In [START_REF] Arcuri | Black-box system testing of real-time embedded systems using random and search-based testing[END_REF] the use of random testing, adaptive random testing and genetic algorithms for use in model-based black-box testing of real-time systems is investigated. To this end, the test-environment is modeled in UML/MARTE while the design of the SUT is not modeled at all, since all test data are derived from the possible environment behavior. An environment simulator is derived from the model that interacts with the SUT and provides the inputs selected by one of the strategies. The environment model also serves as a test oracle that reports errors as soon as unexpected reactions from the SUT are observed. This and similar approaches are easier to implement than the methods described in this paper, because there is no need to encode the transition relation of the model and to provide a constraint solver, since concrete test data is found by randomized model simulations. We expect, however, that the methods described in [START_REF] Arcuri | Black-box system testing of real-time embedded systems using random and search-based testing[END_REF] do not scale up to handle systems of the size presented here, where the concurrent nature of the SUT requires to consider the interaction between several components in real-time (the model would be too large to construct a single large product automaton from the many smaller ones describing the component behavior). To the best knowledge of the authors there is no work on using search based testing on synchronous parallel real-time systems in order to achieve a high degree of SUT coverage, let alone to find test input data to symbolic test-cases.

The solutions presented here have been implemented in the RT-Tester test automation tool which provides an alternative to TRON [START_REF] Nielsen | Automated test generation from timed automata[END_REF][START_REF] David | Timed testing under partial observability[END_REF] which supports timed automata test models and is also fit for industrial-strength application. TRON is complementary to RT-Tester, because it supports an interleaving semantics and focuses on event-based systems, while RT-Tester supports a synchronous semantics with shared variable interfaces. RT-Tester also competes with the Conformiq Tool Suite [START_REF]Conformiq Tool Suite[END_REF], but focuses stronger on embedded systems testing with hard real-time constraints.

Model Overview

General. Our MBT benchmark model specifies the turn indicator functions available in Mercedes Benz cars; this comprises left-/right turn indication, emergency flashing, crash flashing, theft flashing and open/close flashing. The level of detail given in the model corresponds to the observation level for system testing. To provide the full functionality, several automotive controllers cooperate using various communication busses (CAN and LIN). The signals exchanged between controllers can be observed by the testing environment; additionally the environment can stimulate and monitor discrete and analogue interfaces between SUT and peripherals, such as switches, buttons, indicator lights and various dashboard indications. Capturing this functionality in a formal way requires a concurrent real-time system semantics.

System Interface. In Fig. 1 the interface between system under test (SUT) and testing environment (TE) is shown. Due to the state-based nature of the hardware interfaces (discretes, periodic CAN or LIN bus messages repeatedly sending state information) the modeling formalism handles interfaces as shared variables written to by the TE and read from by the SUT or vice versa.

The TE can stimulate the SUT via all interfaces affecting the turn indication functionality in the operational environment: in CentralLockingRM ∈ {0, 1, 2} denotes the remote control for opening and closing (i. e. unlocking and locking) cars by means of the central locking system. Signal in CrashEvent ∈ {0, 1} activates a crash impact simulator which is part of the TE, and in EmSwitch ∈ {0, 1} simulates the "not pressed"/"pressed" status of the emergency flash switch on the dashboard. Signal in IgnSwitch ∈ {0, . . . , 6} denotes the current status of the ignition switch, and in TurnIndLvr ∈ {0, 1, 2} the status of the turn indicator lever (1 = left, 2 = right). In special-purpose vehicles (SPV), such as taxis or police cars, additional redundant interfaces for activation of emergency flashing and turn indicators exist (e. g., in EmSwitchSPV ∈ {0, 1}). Observe that these redundant interfaces may be in conflicting states, so that the control software has to perform a priority-dependent resolution of conflicts. Inputs to the SUT marked by OPTION specify different variants of vehicle style and equipments, each affecting the behavior of the turn indication functions. In contrast to the other input interfaces to the SUT, options remain stable during execution of a test procedure, since their change requires a reset of the automotive controllers, accompanied by a procedure for loading new option parameters. If the TE component does not contain any behavioral specifications, the test generator will create arbitrary timed sequences of input vectors suitable to reach the test goals, only observing the range specifications associated with each input signal. This may lead to unrealistic tests. Therefore the TE may be decomposed into concurrent components (typically called simulations) whose behavior describe the admissible (potentially non-deterministic) interaction of the SUT environment on some or all interfaces. The test generator interprets these simulations as additional constraints, so that only sequences of input vectors are created, whose restrictions to the input signals controlled by TE components comply with the transition relations of these simulations.

SUT outputs are captured in the SignalsOut interface (Fig. 1 shows only a subset of them). The indicator lights are powered by the SUT via interfaces pwmRatio FL, pwmRatio FR, . . . ∈ {0, . . . , 120} where, for example, FL stands for "forward left" and RR for "rear right". The TE measures the percentage of the observed power output generated by the lamp controllers, 100% denoting identity with the nominal value. System integration testing is performed in grey box style: apart from the SUT outputs observable by end users, the TE also monitors bus messages produced by the cooperating controllers performing the turn indication service. Message tim EFS ∈ {0, 1}, for example, denotes a single bit in the CAN message sent from a central controller to the peripheral controllers in order to indicate whether the emergency flash switch indicator on the dashboard should be activated, and tim FL ∈ {0, 1} is the on/off command to the controller managing the forward-left indicator light. Behavioral Semantics. Model components behave and interact according to a concurrent synchronous real-time semantics, which is close to Harel's original micro-step semantics of Statecharts [START_REF] Harel | The statemate semantics of statecharts[END_REF]. Each leaf component of the model is associated with a hierarchic state machine. At each step starting in some model pre-state σ 0 , all components possessing enabled state machine transitions process them in a synchronous manner, using σ 0 as the pre-state. The writes of all state machine transitions affect the post-state σ 1 of the micro-step. Two concurrent components trying to write different values to the same variable in the same micro-step cause a racing condition which is reflected by deadlock of the transition relation and -in contrast to interleaving semantics -considered as a modeling error. Micro-steps are discrete transitions performed in zero time.

Inputs to the SUT remain unchanged between discrete transitions. If the system is in a stable state, that is, all state machine transitions are disabled, time passes in a delay transition, while the system state remains stable. The delay must not exceed the next point in time when a discrete transition becomes enabled, due to a timeout condition. At the end of a delay transition, new inputs to the SUT may be placed on each interface. The distinction between discrete and delay transitions is quite common in concurrent real-time formalisms, and it is also applied to interleaving semantics, as, for example, in Timed Automata [START_REF] Springintveld | Testing timed automata[END_REF]. The detailed formal specification of the semantic interpretation of the model is also published on the website given above [START_REF] Peleska | Automated modelbased testing with RT-Tester[END_REF].

IgnSwitchBusRouting NormalAndEmerFlashing OpenCloseFlashing CrashFlashing TheftFlashing PriorityHandling OnOffDuration MessageHandling AffectedLamps LampControl Fig. 2: First-level decomposition of system under test.

Benchmark Reference Tool

Tool Components and Basic Concepts. The reference data for the benchmarks have been created using our model-based testing tool RT-Tester. It consists of a parser front-end transforming textual model representations (XMI export provided by the CASE tool) into internal representations of the abstract model syntax.

A constraint generator derives all model coverage goals from the abstract syntax tree and optionally inputs user-defined symbolic test cases. Users may select which symbolic test cases should be discharged in the same test procedure. A transition relation generator traverses the model's abstract syntax tree and generates the model transition relation Φ needed for expressing computation goals according to Equation [START_REF] Arcuri | Black-box system testing of real-time embedded systems using random and search-based testing[END_REF]. During the test data and test procedure generation process, the constraints associated with these symbolic test cases are passed on to an abstract interpreter. The interpreter performs an abstract conservative approximation of the model states that are reachable from the current model state within a pre-defined number n of steps. The goals which may be covered within n steps according to the abstract interpretation are passed on in disjunctive form to an SMT solver. The solver unrolls the transition relation in a step-by-step manner and tries to solve at least one of the goals. If this succeeds, a timed sequence of input vectors to the SUT is extracted from the solution provided by the SMT solver. Starting from the current model state, a concrete interpreter executes this sequence until a new stable state is reached where further inputs may be generated to cover the remaining goals. If the solver cannot discharge any goal within n steps, random simulations and/or backtracking to model states already visited can be performed in order to identify other model states from where the next goal may be reached. Constraint generator, interpreters and solver represent the core of the tool, called the test generation engine. Its components only depend on the abstract syntax representation of the model and its transition relation, but not on the concrete modeling syntax and the syntax required by the test execution environment for the test procedures.

At the end of the generation process a multi-threaded test procedure is generated which stimulates the SUT according to the input sequences elaborated by the solver and simultaneously checks SUT reactions with respect to consistency with the model. In the sections below we highlight the most important features of the tool; a detailed description is given in [START_REF] Peleska | Automated modelbased testing with RT-Tester[END_REF].

SMT-Solver. The constraint solving problems of type (1) may contain linear and non-linear arithmetic expressions, bit-operations, array-references, comparison predicates and the usual Boolean connectives. Data types are Booleans, signed and unsigned integers, IEEE-754 floating-point numbers and arrays.

Our SMT-solver SONOLAR uses the classical bit-blasting approach that transforms a formula to a propositional satisfiability problem and lets a SATsolver try to find a solution [START_REF] Jha | Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic[END_REF][START_REF] Brummayer | Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays[END_REF]. Variables in the formula are translated to vectors of propositional variables (i. e., bit vectors). The lengths of these bit vectors correspond to the bit width of the respective data types. Operations are encoded as propositional constraints relating input to output bit vectors. Since we reason on bit-level, this enables us to precisisely capture the actual semantics of all operations. Integer arithmetic takes potential overflows into account and each floating point operation is correctly rounded to the selected IEEE-754 rounding-mode.

To this end, the formula is first represented as an acyclic expression graph, where each variable and each operation of the formula is represented as a node. Using structural hashing on these nodes, identical terms are shared among expressions. This representation allows us to perform word-level simplifications, normalization and substitutions. The expression graph is then bit-blasted to an And-Inverter Graph (AIG). AIGs are used by several SMT solvers to synthesize propositional formulas [START_REF] Jha | Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic[END_REF][START_REF] Brummayer | Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays[END_REF][START_REF] Jung | SWORD v1.0. Tech. rep[END_REF]. Each node of an AIG is either a propositional variable or an and -node with two incoming edges that may optionally be inverted, i.e. negated. The AIG is structually hashed and enables us to perform bit-level simplifications. Readers are referred to [START_REF] Eén | Applying logic synthesis for speeding up SAT[END_REF][START_REF] Brummayer | Local two-level and-inverter graph minimization without blowup[END_REF] for more information on logic synthesis using AIGs. The AIG is then translated to CNF using the standard Tseitin encoding and submitted to a SAT solver.

In order to handle the extensional theory of arrays we adopted the approach described in [START_REF] Brummayer | Lemmas on Demand for the Extensional Theory of Arrays[END_REF]. Instead of bit-blasting all array expressions to SAT up-front, array expressions that return bit-vectors associated with array-reads or checks for array equality are replaced by fresh variables. This results in an over-abstraction of the actual formula since the array axioms are left out. If the SAT solver is able to find a solution to this formula the model is checked for possible array inconsistencies. In this case, additional constraints are added on-demand to rule out this inconsistency. This process is repeated until either the SAT solver finds the refined formula to be unsatisfiable or no more array inconsistencies can be found. While unrolling the transition relation constraints are incrementally added to the SMT solver.

Abstract Interpretation. Our abstract interpreter has been developed to compute over-approximations of possible model computations in a fast way. Its main application is to determine lower bounds of the parameter c in Formula (1) specifying the number of times the transition relation Φ must be unrolled before getting a chance to solve tc(c, G). This considerably reduces generation time, because (a) the SMT solver can skip solution trials for tc(c, G) with values of c making a solution of tc(c, G) infeasible, and (b) the abstract interpretation technique provides the means for non-chronological backtracking in situations where it is tried to solve tc(c, G) from a former model state already visited (see [START_REF] Peleska | Automated test case generation with SMTsolving and abstract interpretation[END_REF] for a more detailed description).

The abstract interpreter operates on abstract domains: interpretation of model behavior is performed using an abstract state space Σ A instead of the concrete one. Σ A is obtained by replacing each concrete data type D of the concrete state space Σ with an adequate abstract counterpart L(D). Functions defined over concrete data types D 0 , . . . , D n are lifted to the associated abstract domains L(D 0 ), . . . , L(D n ). In order to be able to reason about concrete computations while computing only the abstract ones, concrete and abstract states are related to one another by Galois connections. A Galois connection is a tuple of mappings ( : P(Σ) → Σ A , : Σ A → P(Σ)) defining for any set of concrete states the associated abstract state and vice versa, see [START_REF] Peleska | Automated test case generation with SMTsolving and abstract interpretation[END_REF] for additional details. Finally, each abstract domain L(D) is equipped with a join operator : L(D) × L(D) → L(D) which establishes the basis for the join operator over two abstract states : Σ A × Σ A → Σ A . This operator is essential as it allows to reduce the complexity usually arising when interpreting large models where the computation of all reachable states would otherwise be infeasible, due to the number of states and the number of control decisions.

The abstract interpreter uses the interval, Boolean and power set lattices as abstract domains for numerical data types, Booleans and state machine locations, respectively. The interpretation of a given model is parametrized by an initial abstract state σ 0 A ∈ Σ A , an integer c max denoting the maximal number of transition steps to be interpreted and a test case goal G to be checked for satisfiability. Starting in the given initial state, the interpreter computes a sequence of up to c max abstract states σ 1 A , σ 2 A , . . . where each state σ i+1

A is guaranteed to "include"4 every concrete state σ i+1 reachable from any of the concrete states represented by σ i A . The interpretation stops as soon as either the maximal number of steps has been reached or the test case goal G evaluates to true or 5 . In the latter case the actual step number is returned.

MBT Benchmark Classification

We propose to classify MBT benchmarks according to the following characteristics, denoted by test strength benchmarks and test generation benchmarks.

Test strength benchmarks investigate the error detection capabilities of concrete test cases and test data generated by MBT tools: even if two MBT tools produce test suites of equivalent model coverage, they will usually possess different strength, due to different choices of symbolic test cases, representatives of equivalence classes, boundary values and timing of input vectors passed to the SUT, or due to different precision of the test oracles generated from the model. Mutation testing is an accepted approach to assessing test suite strength; therefore we suggest to generate model mutants and run test suites generated from the unbiased model as model-in-the-loop tests against these mutants. The evaluation criterion is the percentage of uncovered mutations for a fixed set of mutant models.

Test generation benchmarks input symbolic test cases as introduced in Section 3 and measure the time needed to generate concrete test data. We advocate a standard procedure for providing these test objectives for a given model, structuring symbolic test cases into several sets. The first sets should be related to model coverage criteria [START_REF] Weißleder | Test Models and Coverage Criteria for Automatic Model-Based Test Generation with UML State Machines[END_REF], such as (1) control state coverage (every control state of the SUT model is visited by at least one test), (2) state machine transition coverage (every transition of every state machine is taken at least once) and (3) MC/DC coverage (conditions of the type φ 1 ∧ φ 2 are tested at least once for is the Boolean lattice value representing the concrete value set {false, true}.

each of the valuations (φ 1 , φ 2 ) = (false, true), (true, false), (true, true), and conditions of the type φ 1 ∨ φ 2 are tested at least for (φ 1 , φ 2 ) = (false, false), (true, false), (false, true)).

Conventional model coverage criteria as the ones listed in (1 -3) do not possess sufficient strength for concurrent real-time systems, because the dependencies between state machines operating in parallel are not sufficiently addressed. Since models as the one under consideration are too large to consider coverage of all state vector combinations, a pragmatic compromise is to maximize the coverage of all basic control state pairs of interacting components C 1 , C 2 , combined with pairs of input equivalence classes of signals influencing C 1 , C 2 . As a consequence suggest symbolic test cases consisting of (a subset of) these combinations as a forth set. As a fifth set of symbolic test cases it is proposed to define application-specific test cases of specific interest.

Given these classes for a specific model, this induces 5 test suites to realize a comprehensive test generation benchmark.

Evaluation criteria for test generation benchmarks. Apart from the time needed to generate concrete test data, the number of SUT resets involved in the resulting test procedures should be minimized as well: since SUT resets usually consume significant time when testing embedded systems, hardware-in-the-loop tests avoiding resets significantly reduce the test suite execution time. Moreover, test executions covering many test cases drive the SUT into more internal states than test executions resetting the SUT between two or only a small number of test cases. As a consequence, the error detection capabilities of test procedures are usually increased with the number of test cases they cover between resets. Avoiding resets is adverse to the reduction of generation time: if some goal Fφ is very time consuming to reach from a given model state σ 0 , backtracking to a former model state from where computation fragments fulfilling Fφ can be reached more easily frequently helps to reduce the generation time in a significant way. Since the SUT is usually unable to roll back into a previous state, backtracking enforces a SUT reset, after which the new computation can be exercised. For comparing the performance of tools we suggest to calculate Pareto frontiers of pairs (generation time,number of resets) for each competing tool, and compare the tool-dependent frontiers.

Significance of test generation benchmarks. According to standards applicable to safety-critical systems verification [START_REF]EN 50128 -Railway applications -Communications, signalling and processing systems -Software for railway control and protection systems[END_REF][START_REF]SC-167[END_REF] the error detection strength of a test suite is just one aspect to be addressed when justifying the adequateness of test cases. Complementary to that the standards require to account for sufficient coverage on the levels of requirements, design and code. As a consequence, the capability of test automation tools to generate sufficient test cases to achieve such coverage has significant impact on verification and certification efforts.

The benchmark website [START_REF] Peleska | Embedded systems testing benchmark[END_REF] contains two classes of symbolic test cases: (1) user-defined test cases reflect specific test purposes identified by test engineers. They serve either to test more complex requirements which cannot be traced in the model to simple sets of basic control states or transitions to be covered, or they are used to explore SUT reactions in situations where a failure is suspected. (2) Model-defined test cases aim at covering certain parts of the model according to pre-defined strategies, such as basic control state coverage, state machine transition coverage and MC/DC coverage. They are automatically derived by our tool from the abstract syntax representation of the model. Instead of explicitly determining the sequence of timed input vectors to the SUT which is suitable for covering the test purpose described, we specify simpler and shorter symbolic test cases that may also refer to internal model states and leave it up to the tool's generation engine to calculate the concrete test input data and its timing. Symbolic test case This formula is a directive to stay in the theft alarm state for at least another 2 seconds after which a model state is to be reached where the internal model variable oc_CentralLockingStatus has value 1 (= "unlocked"), indicating that an "unlock doors" command has been given via remote key control. Again, the associated inputs and timing is calculated by the test generation engine. The final symbolic test case to be processed by the generator is It is a directive to stay in the "theft alarm disabled" state ...THEFT_ALARM_OFF for at least another two seconds, so that it can be observed that after one flash period signaling that the doors have been unlocked, no further alarm indications are made. The signal flow associated with this test (inputs and expected SUT outputs) is depicted in Fig. 3. The generator created a sequence of input vectors where first doors are closed by means of the remote key control input in_CentralLockingRM (2 = lock, 1 = unlock). This triggers three flashing periods for left and right indicator lamps (pwmRatio_FR, pwmRatio_FL, see Fig. 3b). For open/close flashing the on-duration of a flashing period is 340ms; this is captured in the internal model variable ood_OnDuration whose contents will be transmitted by the SUT via CAN bus and can therefore be observed and checked by the threads running on the test engine and acting as test oracles. After two seconds an alarm is raised by setting in_TheftAlarm = 1. This changes the on-duration of the flashing period to 220ms. Theft alarm flashing is switched off at model execution time stamp 4000, approx. 500ms after the unlock-doors signal has been given (in_CentralLockingRM=1); the change of the internal oc_CentralLockingStatus from 0 to 1 indicates that the "doors unlocked" status has now been realized (see Fig. 3a). One flashing period signals "doors unlocked" (again with on-duration 340ms), after which no further alarm indications occur.

Conclusion

We have presented a model of an automotive control application, covering the full functionality related to turn indication, emergency flashing, crash, theft and open/close flashing. The model is a 1-1-transcription of the one currently used by Daimler for system testing of automotive controllers. As the only adaptation we have presented the model in pure UML 2.0 style, while Daimler uses a specific UML profile optimized for their hardware-in-the-loop testing environment. The model is made available to the public in complete form through the website [START_REF] Peleska | Embedded systems testing benchmark[END_REF], together with benchmark test suites and performance values achieved with our reference tool. Additionally, a classification of benchmarks for embedded systems test tools has been suggested which takes into account both the test strength and the performance for automated test suite generation. The underlying methods of the MBT tool used by the authors for performing embedded systems test have been described, in order to facilitate the comparison of competing techniques applied to the benchmarks in the future. The tool is currently applied in industrial projects in the automotive, railway and avionics domains.

Fig. 1 :

 1 Fig. 1: Interface between test environment and system under test.

  In this section a test generation based on user-defined test cases from [17, Test UD 003] is presented. The underlying test purpose is to investigate the interaction between theft alarm and open/close flashing: theft alarm flashing is only enabled when the doors are locked. As a reaction to alarm-sensor activation the turn indicator lights shall start flashing on both sides. Pressing the remote control key to unlock the doors automatically shuts off the alarm flashing.

  (a) Generated inputs and internal model state oc CentralLockingStatus. (b) Expected outputs and internal model state ooo OnDuration.

Fig. 3 :

 3 Fig. 3: Generation results of theft alarm test procedure.

  refers to SUT inputs (theft alarm-sensor in_TheftAlarm) the model execution time (_timeTick) and basic control states of state machines which are part of the SUT model (SystemUnderTest.TheftFlashing...ALARM_OFF). The LTL formula is a directive to the test generation engine to find a computation which finally reaches a model state where theft alarm flashing is enabled but not yet active (this is the case when the basic control state ...ALARM_OFF is reached), and the theft alarm-sensor should remain passive until 2000ms have passed since start of test (the leading finally operator is always omitted in our symbolic test case specifications). The inputs derived by the generation engine to cover this test case drive the SUT into a state where an alarm is signaled and the SUT has to react by activating theft alarm flashing. The next symbolic test case to be processed is

	6
	TC-turn_indication-THEFT_ALARM-0001;
	[ SystemUnderTest.TheftFlashing.TheftFlashing.THEFT_ALARM_ACTIVE.ALARM_OFF
	&& ! in_TheftAlarm ]
	Until
	[ _timeTick >= 2000 && in_TheftAlarm ]
	TC-turn_indication-THEFT_ALARM-0002;
	[ SystemUnderTest.TheftFlashing.TheftFlashing.THEFT_ALARM_ACTIVE.ALARM_ON
	&& in_TheftAlarm ]
	Until
	[ _timeTick >= 4000 && IMR.in_TheftAlarm &&
	SystemUnderTest.oc_CentralLockingStatus == 1 ]

In the sense that σ i+1 ∈ (σ i+1 A )

The symbols used in the test cases below are taken from the turn indicator model published in[START_REF] Peleska | Embedded systems testing benchmark[END_REF]. A detailed description of inputs, outputs and internal model variables can be found there.


Neil Walkinshaw
email: nw91@le.ac.uk

Assessing Test Adequacy for Black-Box Systems Without Specifications

Testing a black-box system without recourse to a specification is difficult, because there is no basis for estimating how many tests will be required, or to assess how complete a given test set is. Several researchers have noted that there is a duality between these testing problems and the problem of inductive inference (learning a model of a hidden system from a given set of examples). It is impossible to tell how many examples will be required to infer an accurate model, and there is no basis for telling how complete a given set of examples is. These issues have been addressed in the domain of inductive inference by developing statistical techniques, where the accuracy of an inferred model is subject to a tolerable degree of error. This paper explores the application of these techniques to assess test sets of black-box systems. It shows how they can be used to reason in a statistically justified manner about the number of tests required to fully exercise a system without a specification, and how to provide a valid adequacy measure for black-box test sets in an applied context.

Introduction

When do we know that a test set is adequate? How do we know that it is sufficiently rigorous for its execution to highlight the presence of any faults? If it is not adequate, how many more tests will we need to generate to achieve a requisite level of adequacy? These questions are fundamental to software testing.

Although numerous approaches are routinely used to assess test adequacy (e.g. code or model coverage), these have significant drawbacks. Code-based coverage has been shown to be an unconvincing fault predictor (c.f. work by Nagappan et al. [START_REF] Nagappan | The influence of organizational structure on software quality: an empirical case study[END_REF]). Model-based coverage on the other hand makes the restrictive assumption that there exists a complete and up-to-date model of the system in question.

Over the past 30 years, a different approach to test adequacy has emerged that attempts to circumvent the weaknesses of traditional techniques. This approach exploits an intuitive relationship between the seemingly unrelated fields of inductive inference and software testing. The idea is to treat the two approaches as two sides of the same coin; both are dealing with a system that is unknown; testing elicits behaviour, and inductive inference reasons about its behaviour by inferring models. From the perspective of test adequacy, there is a direct link between the accuracy of an inferred model and the adequacy of the test set that was used to infer it [START_REF] Zhu | Inductive inference and software testing[END_REF][START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF]. If a model can be shown to be accurate, the underlying test set evidently exercises the system in a sufficiently extensive manner.

There has been a recent resurgence in techniques that expolit this relationship [START_REF] Bergadano | Testing by means of inductive program learning[END_REF][START_REF] Briand | Using machine learning to refine category-partition test specifications and test suites[END_REF][START_REF] Cherniavsky | A recursion theoretic approach to program testing[END_REF][START_REF] Ghani | Strengthening inferred specifications using search based testing[END_REF][START_REF] Last | Data mining for software testing[END_REF][START_REF] Perkins | Efficient incremental algorithms for dynamic detection of likely invariants[END_REF][START_REF] Raffelt | Learnlib: A library for automata learning and experimentation[END_REF][START_REF] Shahamiri | An automated framework for software test oracle[END_REF][START_REF] Shahbaz | Inferring mealy machines[END_REF][START_REF] Walkinshaw | The practical assessment of test sets with inductive inference techniques[END_REF][START_REF] Walkinshaw | Increasing functional coverage by inductive testing: A case study[END_REF][START_REF] Walkinshaw | Iterative refinement of reverse-engineered models by model-based testing[END_REF][START_REF] Weyuker | Assessing test data adequacy through program inference[END_REF] by inferring models from test sets, and in some cases using these models to elicit further test cases. However, these techniques tend to suffer from two problems: [START_REF] Angluin | learning regular sets from queries and counterexamples[END_REF] there is no means of predicting how many tests would be required to arrive at an adequate test set and (2) given a partial test set, there is no basis for gauging how close it is to being adequate.

Problems that are analogous to these have been the subject of much research in the context of inductive inference [START_REF] Blumer | Learnability and the vapnik-chervonenkis dimension[END_REF][START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF][START_REF] Valiant | A theory of the learnable[END_REF]. These techniques, which are largely based on probabilistic reasoning, are especially interesting from a testing perspective because they offer potential solutions to these testing problems. This was the subject of a reasonably concentrated amount of research in the eighties and nineties [START_REF] Cherniavsky | A recursion theoretic approach to program testing[END_REF][START_REF] Romanik | Approximate testing and its relationship to learning[END_REF][START_REF] Romanik | Using Vapnik-Chervonenkis dimension to analyze the testing complexity of program segments[END_REF][START_REF] Weyuker | Assessing test data adequacy through program inference[END_REF][START_REF] Zhu | Inductive inference and software testing[END_REF][START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF], but has not been revisited in the light of the aforementioned surge in popularity of learning-based testing techniques.

This paper investigates the application of these techniques in a realistic testing context. The key contributions are as follows:

1. An implementation of Valiant's PAC framework [START_REF] Valiant | A theory of the learnable[END_REF] in a testing context. This enables the probabilistic specification of what would be considered to be an adequate test set in terms of the accuracy of the model that is inferred from it. 2. The application of PAC-based probabilistic techniques [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF][START_REF] Blumer | Learnability and the vapnik-chervonenkis dimension[END_REF] to estimate lower bounds on the number of tests required for a test set of a black-box SUT to be adequate.

-An applied demonstration of how to apply these approaches to SUTs that may be modelled by Finite State Machines.

3. A practical demonstration of the use of the PAC framework in an applied setting to quantify the adequacy of test sets with respect to a small black-box simulator of an SSH client. The entire infrastructure used for experimentation have been made openly available.

Section 2 will present the background to combining inductive inference with testing. Section 3 will show how the PAC framework can be reinterpreted in a testing context. Section 4 will show how this can be used to estimate the required size of an adequate test set. Section 5 shows how the PAC framework can be used in a practical context to estimate the adequacy of existing test sets. Section 6 will discuss related work, and section 7 will present the conclusions and discuss future work.

Background

The Setting

This paper considers a setting where the SUT is a black-box, but where there is no usable specification to generate tests from. In this context, a test case is simply an input to the SUT without an expected output. An adequate test set [START_REF] Weyuker | Assessing test data adequacy through program inference[END_REF][START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF][START_REF] Zhu | Inductive inference and software testing[END_REF] will exercise every essential element of functionality in the system, and in doing so trigger any obvious faults such as a crash or an uncaught exception. This setting is realistic. The source code of a system, even if it is available, is only effective to a limited extent when as a basis for test set generation [START_REF] Nagappan | The influence of organizational structure on software quality: an empirical case study[END_REF]. Although there are several sophisticated model-based testing techniques [START_REF] Lee | Principles and Methods of Testing Finite State Machines -A Survey[END_REF], developers rarely produce and maintain models that are sufficiently accurate and up-to-date to serve as a suitable basis for test generation.

The task of generating an adequate test set in this setting is seemingly impossible. Without a specification or source code there is no means by which to assess how complete the test set is. There is also no coverage-like metric to serve as a basis for homing-in on an adequate test set.

Testing with Inductive Inference

Over the past thirty years one approach has emerged that can (at least in principle) assess test sets in the above setting. Instead of generating a test set in a single step and subsequently executing it, the idea is to generate test sets by experimentation. The outputs produced by an initial test set are observed and are used to infer a hypothetical model of system behaviour. Depending on the approach, this may then be used to drive the generation of further test sets, or to assess the adequacy of the original test set by somehow comparing the model with the SUT.

Inductive inference is a means of reasoning about a black-box SUT in terms of its observable behaviour. If a test set is comprehensive enough to enable the inference of an accurate model, then it can be deemed to be adequate [START_REF] Weyuker | Assessing test data adequacy through program inference[END_REF][START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF]. The relationship between inductive inference and software testing was first explored by Weyuker in 1983 [START_REF] Weyuker | Assessing test data adequacy through program inference[END_REF]. Since then a large number of techniques have been developed that adopt different types of model inference. Initially, Weyuker's work and subsequent work by Bergadano et al. [START_REF] Bergadano | Testing by means of inductive program learning[END_REF][START_REF] Weyuker | Assessing test data adequacy through program inference[END_REF] focussed on synthesised programs. Since then however, similar approaches have been based upon Artificial Neural Nets [START_REF] Last | Data mining for software testing[END_REF][START_REF] Shahamiri | An automated framework for software test oracle[END_REF], invariants [START_REF] Ghani | Strengthening inferred specifications using search based testing[END_REF], decision trees [START_REF] Briand | Using machine learning to refine category-partition test specifications and test suites[END_REF] and deterministic finite state automata [START_REF] Berg | On the correspondence between conformance testing and regular inference[END_REF][START_REF] Raffelt | Learnlib: A library for automata learning and experimentation[END_REF][START_REF] Shahbaz | Inferring mealy machines[END_REF][START_REF] Walkinshaw | The practical assessment of test sets with inductive inference techniques[END_REF][START_REF] Walkinshaw | Increasing functional coverage by inductive testing: A case study[END_REF][START_REF] Walkinshaw | Iterative refinement of reverse-engineered models by model-based testing[END_REF].

Practical Problems in Establishing Test Adequacy

The use of inductive inference provides a plausible method for assessing the adequacy of test sets in a meaningful way (i.e. with respect to the behaviour they elicit). However, from a practical point of view, there remain two important barriers to its widespread use:

1. Predicting expense: There is no reliable basis for estimating how expensive the testing process will be, i.e. how many tests will be required to produce an adequate test set. This is a fundamental testing problem and is not restricted to testing techniques that incorporate inductive inference. In the context of testing techniques that use inductive inference, it is akin to stating that it is not known how many examples will be required to infer an accurate model.

Inductive Inference and Testing in a Probably Approximately Correct Setting

In the context of machine learning, the area that seeks to address such problems is generally referred to as Computational Learning Theory (also Statistical Learning Theory). Given the widely acknowledged link between inductive inference and testing, it seems intuitive that some of the Computational Learning Theory principles that have been successfully applied in inductive inference should be readily applicable in a testing context. This section sets the foundations for this by recoding a framework by Valiant [START_REF] Valiant | A theory of the learnable[END_REF], which has become widely known as the Probably Approximately Correct (PAC) framework, into the testing setting.

The PAC Framework

The PAC framework [START_REF] Valiant | A theory of the learnable[END_REF] describes a basic learning setting, where the key factors that determine the success of a learning outcome are characterised in probabilistic terms. As a consequence, if it can be shown that a specific type of learner fits this setting, important characteristics such as its accuracy and expense with respect to different sample sizes can be reasoned about probabilistically. The specific elements of the framework are illustrated here with respect to the example problem of learning a deterministic finite state machine from sample sequences (to save space, we presume the conventional definition and notation [START_REF] Walkinshaw | A framework for the competitive evaluation of model inference techniques[END_REF]). Much of the notation used here to describe the key PAC concepts stems from Mitchell's introduction to PAC [START_REF] Mitchell | Machine Learning[END_REF].

The PAC setting assumes that there is some instance space X. As an example, if we are inferring a finite state machine with an alphabet Σ, X could be the set of all words in Σ * . A concept class C is a set of concepts over X, so in our case case it the set of all deterministic finite state machines that can accept and reject words in X. A concept c ⊂ X corresponds to a specific target within C to be inferred (in our case it is the finite state machine that accepts a specific subset of words in Σ * ). Given some element x (in our case a word), c(x) = 0 or 1, depending on whether it belongs to the target concept. It is assumed that there is some selection procedure EX(c, D) that randomly selects elements in X following some static distribution D (we do not need to know this distribution, but it must not change).

The basic learning scenario is that some learner is given a set of examples as selected by EX(c, D). After a while it will produce a hypothesis h. The error rate of h subject to distribution D (error D (h)) can be established with respect to a further 'test' sample from EX(c, D). This represents the probability that h will misclassify one of the test samples, i.e. error D (h

) ≡ P r x∈D [c(x) = h(x)].
In most practical circumstances, a learner that has to guess a model given only a finite set of samples is susceptible to making a mistake. Furthermore, given that the samples are selected randomly, its performance might not always be consistent; certain input samples could happen to suffice for it to arrive at an accurate model, whereas others could miss out the crucial information required for it to do so. To account for this, the PAC framework enables us to explicitly specify a limit on (a) the extent to which an inferred model is allowed to be erroneous to still be considered approximately accurate, and (b) the probability with which it will infer an approximate model. The error parameter that puts an upper limit on the probability that an inferred model may mis-classify a given input. The δ parameter denotes an upper bound on the probability of a failure to infer a model (within the error bounds). The process starts with the generation of a test set A by the test generator (this is what we are assessing for adequacy). These are executed on the SUT, the executions are recorded and supplied to the inference tool. This infers a hypothetical test oracle. Now, the test generator supplies a further test set B, and the user supplies some acceptable error bounds and δ. The observations of test set B are then compared against the expected observations from the model to compute error D (h). If this is smaller than , the model inferred by test set A can be deemed to be approximately accurate (i.e. the test set can be deemed to be approximately adequate).

A PAC-Compatible Testing Framework

The δ parameter is of use if we want to make broader statements about the effectiveness of the combination of learner and test generator.

Estimating Test Set Size

Given that the SUT is a black-box, and that we can only reason about it by experimenting with it, it is seemingly impossible to ascertain a-priori how many test sets will be required to constitute an adequate test set. Surprisingly work that builds on the PAC framework does enable us to obtain a bound on the number of tests (if we make certain assumptions about the SUT, which are discussed later). By assuming that the set of test cases is selected randomly from some fixed distribution, it becomes possible to make a probabilistic argument the number of test cases required to arrive at a point where any model that is consistent with the test sets must be sufficiently accurate.

The approach relies on the ability to characterise the complexity of the learning task. In the context of PAC-learning Haussler [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF] describes two approaches, each of which is based on a different characterisation of complexity. One of them assumes that it is possible to place an absolute bound the number of possible hypotheses that could be produced by a learner (known as the Version Space), whilst the other assumes that it is possible to place a bound on the internal complexity of the hypothesis space (known as the VC Dimension). These two approaches will be presented in this section, followed by a demonstration of how each of them can be applied to reason about the size of an adequate test set for a black-box SUT that could be modelled by a deterministic finite state machine.

Bounding Test Set Size with Version Spaces

The question of how many tests belong to an adequate test set is akin to the question of how many tests would be required to ensure that an accurate (within the limits of and δ) model can be inferred. To establish this, Haussler's Version-Space based approach [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF] estimates a lower bound on the number of tests that would be required to ensure that all consistent hypotheses that could possibly be inferred from the test set fall within the acceptable error bounds.

To reason about the possible range of hypotheses, Haussler uses Mitchell's notion of version spaces [START_REF] Mitchell | Generalization as search[END_REF]. In the testing context, a test set D consists of inputs x and their expected outputs c(x) . Version spaces are defined as follows (using the definition from Mitchell's book [START_REF] Mitchell | Machine Learning[END_REF]):

V S H,D = {h ∈ H|(∀ x, c(x) ∈ D)(h(x) = c(x))}
Haussler defines the the version space as -exhausted if all of the hypotheses that can be constructed from D have an error below , with respect to any distribution D. More formally [START_REF] Mitchell | Machine Learning[END_REF]:

(∀h ∈ V S H,D )error D (h) <
The number of elements in D that is required to -exhaust V S H,D is exponential or infinite in the worst case. However, given that we are using the PAC setting, this is not the case, we know that the elements in D are selected independently and at random, the number number of tests m that are required to -exhaust V S H,D is considerably improved [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF]. If V S H,D is finite, it becomes possible to establish a lower bound on m. Assuming that set D is constructed by m ≥ 1 independent, random test cases, he shows that the probability that V S H,D is not -exhausted is less than |H|e -m (see Haussler's paper for the proof [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF]). Within the PAC framework, this probability should be less than or equal to δ. This can be factored in to the above probability, and rearranged to impose a lower bound on m, the number of test cases that constitute D:

m ≥ (ln|V S H,D | + ln(1/δ) (1)
The number of required tests m grows linearly in 1/ , it grows logarithmically with 1/δ, and it grows logarithmically in the size of V S H,D [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF].

Bounding Test Set Size with the Vapnik-Chervonenkis Dimension

Depending on the SUT, it may be impossible to easily impose an upper limit on the size of V S H,D (e.g. the SUT could be a function that computes a real number). For this case, Haussler proposed an alternative approach to bound the test set size that does not rely on the size of V S H,D , but uses a measure of complexity of H known as the Vapnik-Chervonenkis or VC dimension [START_REF] Vapnik | On the uniform convergence of relative frequencies of events to their probabilities[END_REF] (though this is not necessarily finite either).

To define the notion of a VC dimension, it is necessary to first introduce the notions of dichotomies, and shattering (see Haussler's paper [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF] for details). If I is some subset of the instance space X, then an hypothesis h ∈ H induces a dichotomy on I by dividing I into those examples that are classified as belonging to h, and those that are not. Π H (m) denotes the maximum number of dichotomies that can be induced by H on any set of m instances.

If H induces all possible 2 I dichotomies of I, then H shatters I. The VC dimension of H V C(H) is the cardinality of the largest subset of X that is shattered by H. Equivalently, it is the largest

m such that Π H (m) = 2 m [9].
Using a proof that is analogous to the one used in the version space approach, Haussler shows that the probability that V S H,D is not -exhausted is less than 2Π H (2m)2 -m/2 . From this, and by incorporating further results from Blumer et al. [START_REF] Blumer | Learnability and the vapnik-chervonenkis dimension[END_REF], it can be rearranged to yield the lower bound on m:

m ≥ 4log 2 (2/δ) + 8V C(H)log 2 (13/ ) (2)
Mitchell [START_REF] Mitchell | Machine Learning[END_REF] notes that this measure will often produce tighter bounds than the equivalent estimation using the Version Space approach. The bound m grows logarithmically in 1/δ, but grows log linear in 1/ . As will be shown in section 4.3, the choice between the version space and the VC approach depends on the ability of the tester to characterise the complexity hypothesis space for the SUT.

Bounding Test Sets for SUTs that are Finite State Machines

This subsection demonstrates the two above techniques, showing how they can estimate the number of tests that are required to test a black-box SUT. For the purposes of illustration, it is assumed that H is the range of deterministic finite state machines over some known alphabet. It is important to note that the use of state machines is merely for the purpose of illustration -Haussler's approach can be applied to a broad range of other representations.

As mentioned previously, the choice between the Version Space approach and the VC dimension approach depends upon the ability to characterise the complexity of H in an appropriate way. In practice the size of V S H,D is infinite for any DFA inference technique, because there are an infinite number of possible DFAs that are consistent with a given test set. The VC dimension for DFAs is also infinite; for any subset of words in X it is possible to produce an exact hypothesis to shatter them, and the largest subset of X is infinite [START_REF] De La Higuera | Grammatical Inference: Learning Automata and Grammars[END_REF].

As a consequence, to ascertain a limit on the test set, it becomes necessary to make some assumptions about the DFA, or the context in which it will be tested. The remainder of this section shows how such assumptions can be used to make the two techniques possible. Specifically, the Version Space approach can be used by imposing a bound on the length of the test cases (implying a bound on the depth of the DFA). Alternatively the VC dimension approach can be used by imposing an upper limit on the number of states in the DFA.

Using the Version Space approach by bounding test case length For DFA inference, the relationship between the set of samples D and the version space V S H,D was described by Dupont [START_REF] Dupont | What is the search space of the regular inference?[END_REF]. He showed how the version space can be interpreted as a lattice where the most specific element is a prefix tree automaton (PTA) (a tree-shaped minimal DFA that exactly represents the sample D [START_REF] Dupont | What is the search space of the regular inference?[END_REF][START_REF] Walkinshaw | Increasing functional coverage by inductive testing: A case study[END_REF][START_REF] Walkinshaw | Iterative refinement of reverse-engineered models by model-based testing[END_REF]), and the most general element is the universal DFA that accepts every element in the DFA alphabet Σ. The size of this version space, which is what we are interested here, is infinite if the depth of the PTA is unrestricted.

However, if the length of the test cases is limited to a chosen length n and the size of the alphabet is denoted σ, the maximum size of a PTA can be computed as: n i=0 σ i . In Dupont's lattice version space, any hypothesis h ∈ H corresponds to a particular partition of the set of states in the PTA (corresponding to the merging of states into their respective equivalence classes). Thus, the size of V S H,D is bounded by the number of possible set partitions of a set the size max -the Bell number of max.

The extremely rapid growth of this number limits the use of the version space approach in this finite state machine setting, and the example shown here is restricted to a very simple SUT. We consider a setting where the length of a test set is restricted to 7, and the size of the alphabet is 3. In this case, the maximum size of the PTA is 3,280 states1 . The upper bound on the number of DFAs that can be generated from such a PTA as computed by the Bell number of 3280 is approximately 1.5 * 10 7722 . Now the task for the tester is to decide a realistic error margin for the assessment of the test adequacy. To simply state that the test set should always be sufficiently comprehensive to produce an exact model is unrealistic. In our example the tester might consider it sufficient if the model inferred from the test set has an error ≤ 0.1, and that this should happen with a probability of 90%. In other words, = 0.1 and δ = 0.1 (calculated by 1 -0.9). This now allows us to apply Haussler's version-space estimation (see equation

Taking these values at face value, the task of constructing an adequate test set of this size for such a relatively simple scenario is unrealistic. It is however important to bear in mind the proportions of the problem space. From a possible 1.5 * 10 7722 hypotheses, it is possible to assert that a consistent learner will produce an accurate hypothesis from a 177,810 tests -i.e. to statistically justify this test set will be adequate.

Of course, considering the relative simplicity of the system in question, this is very large number of tests (despite the vast size of the hypothesis space). There are two things that one has to bear in mind when interpreting this number. Firstly, it is a conservative worst-case estimate. It does not take any failed / impossible tests into account (which would eliminate vast numbers of false hypotheses from an inference standpoint), and does not place any expectations on the learner to do anything with the input data other than be consistent (i.e. not to produce an hypothesis that contradicts the input data). In practice, negative sequences merge out a vast number of invalid merges, and inference techniques often use heuristics [START_REF] Lang | Results of the Abbadingo One DFA Learning Competition and a New Evidence-Driven State Merging Algorithm[END_REF] to efficiently home-in on the correct merges. Ultimately a justifiable upper bound, even if it is too large, is better than no bound at all, because it provides at least a rough guide for the complexity of the SUT, and the associated testing effort.

Using the VC dimension approach by bounding the number of states in the SUT In certain cases, it might not be possible to bound V S H,D . In the previous setting, any larger alphabets or test lengths would become too large to compute in a practical way, and it might simply be impossible to guess an upper bound on the maximum length of a test case anyway. The VC dimension alternative is useful because it does not rely on a finite version space, but instead provides an internal measure of the complexity of a potentially infinite hypothesis space.

Unfortunately, depending on the representation, it is not always possible to calculate a finite VC dimension. For arbitrary DFAs the VC dimension is infinite and can only be made finite by making assumptions about its maximum number of states -if this is n states, the VC-dimension is bounded by n log 2 n [START_REF] De La Higuera | Grammatical Inference: Learning Automata and Grammars[END_REF]. Thus, in this case, the choice between version spaces and VC-dimension approaches is determined by the nature of any additional knowledge of the DFA.

Estimating a suitable number of states n relies on the intuition of the tester, from their prior knowledge of the SUT. For this example, let us guess that the SUT contains at most 300 states. The VC dimension is thus bounded by 300 * log 2 (300) = 2, 468.65. This enables us to substitute for equation 2. As in the initial case for the version space example, let us assume that = 0.1 and δ = 0.1:

m ≥ 4log 2 (2/δ) + 8V C(H)log 2 (13/ ) ≈ m ≥ 4log 2 (2/0.1) + 8 * 2, 468.65 * log 2 (13/0.1) 0.1 ≈ m ≥ 1, 387, 032 (4)
As in the previous version-space approach, this number is a conservative worst-case estimation. It fails to take any heuristic capabilities of the inference technique into account. As previously, depending on the circumstances it might be possible to take this added efficiency into account by increasing the value of . If, using the same rationale, is increased to 0.4, the result is a much reduced bound of m ≥ 248, 012.

It is important to bear in mind that it does not make sense to compare the two approaches as presented here with respect to their estimated test sizes, because this would be comparing estimations for (potentially) completely different systems. Nonetheless, with respect to DFAs, if the number of states can be bounded it is better to use the VC-dimension approach, because it is easier to compute an estimate for more complex systems and tends to compute a much lower bound than the version-space approach (this latter fact applies to all representations, not just DFAs [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF][START_REF] Mitchell | Machine Learning[END_REF]).

Using the PAC Setting to Empirically Assess Test Sets

The ability to predict the sizes of test sets is only one side of the benefit of using the PAC framework for testing, and has been already explored to some extent in previous literature [START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF][START_REF] Romanik | Using Vapnik-Chervonenkis dimension to analyze the testing complexity of program segments[END_REF][START_REF] Romanik | Approximate testing and its relationship to learning[END_REF]. From an empirical aspect, the framework is equally valuable, because it presents us with a basis for making statistically justified measurements of test set adequacy for black-box SUTs, by assessing the performance of the inferred models. This section presents a practical example of this. It not only shows the value of being able to assess test sets, but also highlights an important practical consideration that can lead to problems of accuracy when computing the lower bounds for test size computed by the techniques presented in the previous section.

Current techniques that combine testing with model inference make a binary decision; a test set is adequate if it leads to an exactly accurate model (as assessed within the limits of some model-based testing technique), and inadequate otherwise. This is problematic because there is no basis for homing in on an adequate test set. This section illustrates how the PAC testing framework (as shown in Figure 3.2) can be applied in a practical context to provide feedback about test set adequacy.

The SUT, and the choice of Test Generation and Model Inference Techniques

The SUT in question simulates the behaviour of an SSH client, in terms of the FSM specification described by Poll et al. [START_REF] Poll | Verifying an implementation of ssh[END_REF]. It accepts sequences of instructions as specified, but will throw an "unexpected input" exception if given a sequence of inputs that is not part of the specification. The system is written in Erlang (implemented using the gen fsm behavioural pattern -available with the source code provided with this paper).

Let us assume that we have a small sample of 10 test scenarios that execute some of the expected behaviour of the system. Because these only exercise a tiny (albeit functionally significant) fraction of program behaviour, it is necessary to substantially bulk up the test set if we want it to be adequate. Given that we are presuming no further domain knowledge about the system, the rest of the tests will have to be generated randomly. For this we use a random generator that produces a set of unique random sequences from the given alphabet up to a certain length (for this example we choose 13 to be the maximum test case length, and choose the length of each test case randomly).

The problem with any resulting test set, no matter how large, is that we do not know how adequate it is. This is where the PAC framework can offer a solution. By generating two non-intersecting test sets, using one to infer a model, and the other to assess its accuracy, it is possible to obtain an insight into how adequate the first test set is.

To infer a model from the tests we choose Price's EDSM blue-fringe state merging algorithm [START_REF] Lang | Results of the Abbadingo One DFA Learning Competition and a New Evidence-Driven State Merging Algorithm[END_REF] -until recently the most accurate algorithm for inferring state machines from arbitrary examples. We use the openly available Ruby implementation by Bernard Lambeau that was developed as a baseline for the StaMInA inference competition [START_REF] Walkinshaw | A framework for the competitive evaluation of model inference techniques[END_REF].

Application of the PAC Framework

We start by generating test sets A and B (see Figure 3.2). The PAC framework assumes that these are drawn randomly from the same distribution, but must not overlap. To ensure that this is the case a large set of unique random test cases is generated, and the contents of A and B are selected at random from this superset. Set A will be used to train the model, and will be the test set that we assess, and test set B will be the set with which we assess the accuracy of the model (and so the adequacy of A).

Due to time constraints, we terminate the generation algorithm after an hour. In that time sets A and B have been populated with 42,410 tests each. Now the tests and their respective outcomes from set A are used to infer a model using the StaMInA tool. The model is then used to predict the outcomes for test set B. The error rate can then tell us how adequate test set A. If we use the conventional definition of error D (h) to compute the error, we end up with an adequacy assessment of 99.99%.

Upon closer inspection, splitting the test cases up into true or false positives and negatives shows that this figure has to be interpreted with care. Out of the 42,410 test cases, 42,397 tests are true negatives, five tests are true positives, five tests are false positives and three are false negatives. Ultimately, the fact that there is such a high overlap between sets A and B says more about distribution from wich they were sampled than it does about the SUT. PAC-learning assumes that the distributions A and B reflect the routine behaviour of the system in question, in which case this measure of overlap is appropriate.

In a testing context, this measure is not particularly helpful. A randomly generated test case will generate arbitrary distributions of test cases that do not evenly represent the input domain of the SUT, and may lead to heavily skewed error rates. To account for this, we use the Balanced Classification Rate (BCR) [START_REF] Walkinshaw | A framework for the competitive evaluation of model inference techniques[END_REF] 2 , which balances the ability of the inferred model to reject false negatives against its ability to reject false positives: BCR D (h) = 1 2 (T P/(T P + F N )) + (T N/(T N +F P )). If we apply this to calculate the adequacy of test set A above, we obtain a more balanced test adequacy assessment of 0.8124.

Discussion

This section has demonstrated how to assess the adequacy of a test set for a black-box system. However, in drawing the distinction between the different measures for calculating classification error (error D (h) and bcr D (h)), it highlights an important caveat for interpreting the test-size estimations produced by the techniques in section 4. These predictions only apply when the test set can be reliably assessed using the error D (h) measure, i.e. when the distribution of tests is roughly balanced between valid and invalid cases.

If this is not the case, the estimated lower bound on the number of required test cases will probably be a significant underestimation. Given that the SSH implementation has 19 distinct states [START_REF] Poll | Verifying an implementation of ssh[END_REF], this can be illustrated with the VCdimension approach. For 19 states we obtain a VC-dimension of 80.71. We might guess a conservative value of 0.1, and choose a δ value of 0.1. Substituting into equation 2, this gives us an estimated lower bound of 45,515 test cases.

This happens to be relatively close to the number of tests we generated in section 5.2. Had we used the conventional measure for error D (h), this would certainly be accurate. However, given that out of 42,410 random test-cases only 8 of these produce valid outputs from the SUT, it is clear that a much larger number of random test cases would be required to fully exercise the SUT in terms of its valid behaviour as well (and so reach a high level of adequacy with respect to the BCR). Future work (see section 7) will elaborate the techniques from section 4 to develop more accurate lower bounds that take into account the the balance between valid and invalid test cases.

Related Work

As discussed in the Background section, there has been much work on relating the fields of machine learning and software testing, and several relevant references are included in this paper. Due to limited space, this section shall focus on the more specific topic of the use of probabilistic techniques to reason about test sets for black-box systems without specifications.

The idea of testing "to a confidence level" by joining the fields of Inductive Inference and Testing was first raised by Cherniavsky and Smith in 1987 [START_REF] Cherniavsky | A recursion theoretic approach to program testing[END_REF] (although their work was primarily concerned with learning exact models). The subject was subsequently explored by Zhu et al. [START_REF] Zhu | Inductive inference and software testing[END_REF][START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF]. They used the PAC framework as a theoretical basis to reinterpret and justify a set of fundamental test adequacy axioms they had proposed in earlier work. They also suggest using an alternative to the VC-dimension and version-space estimation approaches to predict the necessary size of a test set (Haussler's Pseudo-dimension) though given that the work is theoretical in nature, there is no suggestion of how this might be used in a practical context (e.g. how to compute the pseudo-dimension for a given type of black box SUT).

The combination of PAC learning and testing was the subject of a substantial amount of work by Romanik et al.. By adopting the PAC framework, they proposed the notion of approximate testing [START_REF] Romanik | Approximate testing and its relationship to learning[END_REF]. They show how familiar machine learning concepts such as the VC-dimension can be used to reason about the general (approximate) testability of particular classes of program, with a particular interest in reasoning about certain classes that are un-testable. In subsequent work, Romanik [START_REF] Romanik | Using Vapnik-Chervonenkis dimension to analyze the testing complexity of program segments[END_REF] considers the relationship between the internal complexity of a program (i.e. its source code branching) and its testability, and proposes an extension of the VC-dimension (the VCP-dimension) to measure this.

Although Zhu and Romanik made pioneering theoretical contributions to the research on combining the two fields, it was perhaps the relative primitiveness of machine learning techniques at the time that prevented the practical application. It is only recently that inference techniques have developed the capabilities to infer (approximately) accurate models of software systems. To the best knowledge of the author, this paper the first work that attempts to experiment with the combination of PAC-learning and testing in a practical sense for the sake of assessing test sets.

Many of the recent testing techniques to involve machine learning (c.f. work by Raffelt et al. and Shahbaz et al. [START_REF] Raffelt | Learnlib: A library for automata learning and experimentation[END_REF][START_REF] Shahbaz | Inferring mealy machines[END_REF] are based on Angluin's L * algorithm [START_REF] Angluin | learning regular sets from queries and counterexamples[END_REF]. In her paper, she discusses how her algorithm could be adapted to suit a PAC setting. To the best of the author's knowledge, this has not yet been implemented in a testing context, but suggests that it would in principle be straightforward to adapt these existing testing techniques to apply the PAC-based principles that have been discussed in this paper.

Conclusions and Future Work

The challenge of producing a comprehensive test set for a black-box system without recourse to a specification is seemingly impossible. There is no obvious basis for determining whether a test set is adequate, and for identifying a candidate set of test cases from a potentially infinite set of potentials.

Against this backdrop, machine learning is a particularly interesting discipline, because it provides a wealth of techniques to reason in a systematic way about hidden systems by way of experimentation. Valiant's PAC framework provides a useful formal basis for this, and has formed the basis for a limited amount of theoretical work on software testing [START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF][START_REF] Romanik | Using Vapnik-Chervonenkis dimension to analyze the testing complexity of program segments[END_REF][START_REF] Romanik | Approximate testing and its relationship to learning[END_REF]. Specifically, the PAC framework can be used to reason about the accuracy of the inferred model which, in turn, provides feedback about the adequacy of the test set that was used to infer it. Furthermore, the use of the PAC framework enables the estimation of how many test sets might be required to produce an adequate test set.

In the light of the recent emergence of numerous testing techniques that are founded on specific machine learning techniques [START_REF] Berg | On the correspondence between conformance testing and regular inference[END_REF][START_REF] Briand | Using machine learning to refine category-partition test specifications and test suites[END_REF][START_REF] Ghani | Strengthening inferred specifications using search based testing[END_REF][START_REF] Last | Data mining for software testing[END_REF][START_REF] Perkins | Efficient incremental algorithms for dynamic detection of likely invariants[END_REF][START_REF] Raffelt | Learnlib: A library for automata learning and experimentation[END_REF][START_REF] Shahamiri | An automated framework for software test oracle[END_REF][START_REF] Shahbaz | Inferring mealy machines[END_REF][START_REF] Walkinshaw | The practical assessment of test sets with inductive inference techniques[END_REF][START_REF] Walkinshaw | Increasing functional coverage by inductive testing: A case study[END_REF][START_REF] Walkinshaw | Iterative refinement of reverse-engineered models by model-based testing[END_REF], this paper has sought to investigate the practical application use of the PAC framework. The paper shows how the PAC framework can be applied in practice. it shows how test set sizes can be predicted, and how the framework can be used to obtain a statistically valid assessment of test adequacy in practice.

The practical example in this paper has highlighted one problem of applying the PAC framework in a testing context. It is assumed that there is a rough balance between valid and invalid test cases, and the conventional measure of error can be misleading when this is not the case (which is typical in a testing context). Future work will attempt to adapt Haussler's predictions [START_REF] Haussler | Quantifying inductive bias: Ai learning algorithms and valiant's learning framework[END_REF], to produce more accurate predictions for typical random testing situations, where the test set is not balanced.

Figure 3 .

 3 Figure 3.2 shows how the inductive inference and testing processes can fit into the PAC framework[START_REF] Zhu | A formal interpretation of software testing as inductive inference[END_REF][START_REF] Walkinshaw | The practical assessment of test sets with inductive inference techniques[END_REF]. The arcs are numbered to indicate the flow of events. The test generator produces tests according to some fixed distribution D that are executed on the SUT c. With respect to the conventional PAC framework they combine to perform the function of EX(c, D).The process starts with the generation of a test set A by the test generator (this is what we are assessing for adequacy). These are executed on the SUT, the executions are recorded and supplied to the inference tool. This infers a hypothetical test oracle. Now, the test generator supplies a further test set B, and the user supplies some acceptable error bounds and δ. The observations of test set B are then compared against the expected observations from the model to compute error D (h). If this is smaller than , the model inferred by test set A can be deemed to be approximately accurate (i.e. the test set can be deemed to be approximately adequate).The δ parameter is of use if we want to make broader statements about the effectiveness of the combination of learner and test generator. By running multiple experiments, we can count the proportion of times that the test set is approximately adequate for the given SUT. If, over a number of experiments,

  By running multiple experiments, we can count the proportion of times that the test set is approximately adequate for the given SUT. If, over a number of experiments,

		5: δ,ε		PAC induc�ve test assessment
				framework
	8: adequacy
		decision
				3: test
	test		PAC	oracle	model
	genera�on	4: test	Assessment	inference
		inputs B
	1: test inputs A	6: test inputs B	7: execu�on observa�ons B
			black box	2: execu�on
			system		observa�ons A
	Fig. 1. Inductive testing with the PAC framework

this proportion is greater than or equal to 1-δ, it becomes possible to state that, in general, the test generator produces test sets that are probably approximately adequate (to paraphrase the term 'probably approximately correct', that would apply to the models inferred by the inference technique in a traditional PAC setting).

A small Erlang module with all of the routines used to compute the results in this paper is available http://www.cs.le.ac.uk/people/nwalkinshaw/Files/ ictss_code.zip

This measure is commonly used in machine learning, and should not be attributed to the author, but is described in this paper with respect to DFA inference.

Acknowledgements Much of the background material that relates inductive inference to software testing was influenced by discussions with Gordon Fraser at Saarland University in Saarbrücken.