Arnab Sharma
email: arnab.sharma@uni-paderborn.de

Heike Wehrheim
email: wehrheim@uni-paderborn.de

Automatic Fairness Testing of Machine Learning Models

Keywords: Fairness, Machine learning testing, SMT solving

In recent years, there has been an increased application of machine learning (ML) to decision making systems. This has prompted an urgent need for validating requirements on ML models. Fairness is one such requirement to be ensured in numerous application domains. It specifies a software as "learned" by an ML algorithm to not be biased in the sense of discriminating against some attributes (like gender or age), giving different decisions upon flipping the values of these attributes. In this work, we apply verification-based testing (VBT) to the fairness checking of ML models. Verification-based testing employs verification technology to generate test cases potentially violating the property under interest. For fairness testing, we additionally provide a specification language for the formalization of different fairness requirements. From the ML model under test and fairness specification VBT automatically generates test inputs specific to the specified fairness requirement. The empirical evaluation on several benchmark ML models shows verificationbased testing to perform better than existing fairness testing techniques with respect to effectiveness.

Introduction

Machine Learning (ML) is gradually being used in software systems and replacing humans in decision making. The application area of such software systems now ranges from social and economical domains to even law [START_REF] Liptak | Sent to prison by a software program's secret algorithms[END_REF]. Therefore, the quality assurance of these systems is of utmost importance. In the past few years, a significant amount of research works have been performed for checking various sorts of requirements arising in different application domains (e.g., robustness [START_REF] Huang | Safety verification of deep neural networks[END_REF], security [4], balancedness [START_REF] Sharma | Testing machine learning algorithms for balanced data usage[END_REF]).

One such requirement which often needs to be ensured by the "learned" software system is fairness. Although there exists multiple definitions of fairness in the literature [START_REF] Verma | Fairness definitions explained[END_REF], the basic idea of the property is always the same. Fairness requires that changing the values of only the protected attributes should not change the prediction of an ML classifier. For example, a loan granting software which decides whether a person gets a loan, is discriminating against "gender", if it gives a different decision (i.e., prediction) for male and female applicants when all other values of features besides "gender" are equal. Here, gender is considered to be the protected attribute.

Most often the use of biased training data results in such unfair predictors. However, even if the training data does not contain any unfairness, the generated ML model can still be biased. Hence, today there exists a number of specialized algorithms aiming at the generation of fair ML models (e.g. [START_REF] Calders | Building classifiers with independency constraints[END_REF], [START_REF] Zafar | Fairness constraints: Mechanisms for fair classification[END_REF]). Galhotra et al. [START_REF] Galhotra | Fairness testing: testing software for discrimination[END_REF] have nevertheless shown that even the use of these fair algorithms cannot guarantee fair predictive models. They have proposed a random testing technique called THEMIS which works by generating a number of test cases testifying if and how much unfairness exists in the ML model. They have furthermore proposed individual discrimination as the definition of fairness, as their work suggests that the existing fairness definitions can hide unfairness in an ML model. Later, Udeshi et al. have proposed AEQUITAS [START_REF] Udeshi | Automated directed fairness testing[END_REF] which generates a higher number of test cases in comparison to THEMIS in checking individual discrimination. More recently, Aggarwal et al. [START_REF] Aggarwal | Black box fairness testing of machine learning models[END_REF] have proposed a technique combining dynamic symbolic execution and local explanation which outperforms the previous two techniques in checking fairness.

Although these approaches perform quite well in detecting unfairness of a given ML model, they mostly focus on testifying one specific type of fairness. Hence, these approaches cannot be directly used to check a model for any fairness definition. As there exists several such fairness definitions depending on the application domain, a unified approach to test an ML model for a given fairness property is required.

In an earlier work, we have introduced a novel black-box testing approach [START_REF] Sharma | Higher income, larger loan? monotonicity testing of machine learning models[END_REF] to test the monotonicity of a given ML model. This approach works by systematically exploring the input space of the given model by firstly inferring a white-box model approximating the black-box model under test (MUT), and computing the counter examples to monotonicity on the white-box model via an established verification technique. The computed counter examples on the white-box model are then checked with the black-box model. The confirmed ones are stored as test cases violating the property and further varied to generate more test cases. If unconfirmed, they serve as input to an improvement of the approximation quality of the white-box model. Here, we extend this approach to test the fairness of a given machine learning model. Our idea is to develop a property-based testing mechanism for fairness checking where the specific fairness requirement can be specified using an assume-assert construct. Test cases are then automatically generated attempting to violate the specified fairness property. The underlying mechanism remains the same as before and comprises four key steps: 1) Whitebox model inference, 2) fairness computation, 3) variation and 4) white-box model improvement.

We have implemented our approach and have experimentally evaluated it by applying it on standard benchmark ML models. Our experimental results suggest that our verification-based testing technique performs better than existing fairness testing techniques ( [START_REF] Udeshi | Automated directed fairness testing[END_REF] and [START_REF] Aggarwal | Black box fairness testing of machine learning models[END_REF]) for most of the test cases. Summarizing, this paper makes the following contributions:

-We provide a specification language for formulating fairness requirements on ML Models. -We employ our verification-based-testing technique to test fairness of ML models. -We systematically evaluate our approach on several standard benchmarks and compare our results with existing fairness testing approaches.

The paper is structured as follows. In the next section, we define fairness of machine learning models. In Section 3 we describe our specification language and verification-based testing. Section 4 presents the results of our experimental evaluation. We discuss related work in Section 5 and conclude in Section 6.

Fairness

We begin with the basic terminologies in machine learning and then give definitions of fairness.

Our interest is in testing models obtained by supervised machine learning. Such algorithms typically have two steps. Initially, in the learning phase, the algorithm is presented with a set of data instances called training data. The ML algorithm then generates a function (the predictive model), generalising from the training data by using some statistical techniques. The generated predictive model (short, model) is used in the second (prediction) phase to predict classes for unknown data instances.

Formally, the generated model (M ) can be defined as a function

M : X 1 × . . . × X n → Y ,
where X i is the value set of feature i (or attribute or characteristics i), 1 ≤ i ≤ n, and Y is the set of classes. We define

#» X = X 1 × . . . × X n .
The training data consists of elements from #» X × Y , i.e., data instances with known associated classes. During the prediction, the generated predictive model assigns a class y ∈ Y to a data instance (x 1 , . . . , x n ) ∈ #» X. In the literature, a large number of fairness definitions for ML models can be found (see [START_REF] Verma | Fairness definitions explained[END_REF] for a survey). They basically all build on the same concept of fairness: an ML model (or algorithm in general) is unfair if it is discriminating some individuals (i.e., data instances) on the basis of values of some of their features. This discrimination is however formally captured in completely different ways: while some works (e.g. [START_REF] Dwork | Fairness through awareness[END_REF], [5]) employ statistical measures (probability distributions on certain outcomes of M ), others employ similarity-based measures (e.g. [START_REF] Galhotra | Fairness testing: testing software for discrimination[END_REF], [START_REF] Aggarwal | Black box fairness testing of machine learning models[END_REF]). Our objective here is to develop an approach for testing black-box models, i.e., what our approach can observe about a model are just the outputs (predictions) for certain inputs (data instances). We thus focus on similarity-based measures.

Fairness definitions first of all fix so-called protected or sensitive attributes which are supposed to not lead to discrimination. As an example, consider "income" and "age". A fairness requirement on loan granting software might for instance state that the software should not discriminate against "gender", hence "gender" would be the sensitive attribute. Definition 1. A predictive model M is fair with respect to a sensitive feature i if for any two data instances

x = (x 1 , . . . , x n ), x = (x 1 , . . . , x n ) ∈ #» X, we have (x i = x i ) ∧ (∀j, j = i.x j = x j ) implies M (x) = M (x ).
This fairness definition is termed individual discrimination and was introduced by Galhotra et al. [START_REF] Galhotra | Fairness testing: testing software for discrimination[END_REF]. According to this definition, all the feature values except for the protected one should have the same value. The idea is to find out whether changing only the protected feature value leads to the change of the prediction. Our decision tree model in Figure 1 is not fair wrt. Definition 1 and sensitive feature "gender". Take for instance the following pair of data instances income=1000, age=40, gender=female income=1000, age=40, gender=male For the first instance, the result of the prediction is 'no', while for the second data instance it will be 'yes'.

We next define group discrimination which extends Definition 1 to a set of protected features. Definition 2. A predictive model M is said to be fair with respect to a set of sensitive features F = {i 1 , i 2 , . . . , i m } ⊆ {1, . . . , n} if for any two data instances

x = (x 1 , . . . , x n ), x = (x 1 , . . . , x n ) ∈ #» X we have (∀j ∈ F : x j = x j ∧ ∀j / ∈ F : x j = x j ) implies M (x) = M (x ).
In case of the tree model depicted in Figure 1, it is evident that the decision tree is discriminating those female candidates who have age more than 40. The applicants with age less than 40 are treated equally regardless of their gender. But those who are above 40 should have a higher income than the rest.

Another similarity-based measure is fairness through unawareness. This requires that the protected attributes have no influence on the classification at all. Next, we directly define the group version. Definition 3. A predictive model M is said to be fair with respect to a set of sensitive features F = {i 1 , i 2 , . . . , i m } ⊆ {1, . . . , n} if for any two data instances

x = (x 1 , . . . , x n ), x = (x 1 , . . . , x n ) ∈ #» X we have ∀j / ∈ F : x j = x j implies M (x) = M (x ).
Whenever two data instances coincide on all features values except possibly for the protected attributes, they should get the same prediction.

Finally, there is also a similarity-based measure called fairness through awareness. This relaxes the strict equality of (some) feature values required by the definitions so far to similar values. The similarity is therein captured by some distance metric d :

#» X × #» X → [0, 1] on data instances 1 . Definition 4. Let d : #» X × #» X → [0, 1]
be a distance metric on data instances and ε a threshold. A predictive model M is said to be fair with respect to a set of sensitive features

F = {i 1 , i 2 , . . . , i m } ⊆ {1, . . . , n} if for any two data instances x = (x 1 , . . . , x n ), x = (x 1 , . . . , x n ) ∈ #» X we have d(x, x ) ≤ ε implies M (x) = M (x ).
For our loan-granting example, we could for instance define the distance metric as

d(x, x ) = 1 if x gender = x gender |xage-x age | 100
else and let ε = 0.1. This would require that all pairs of data instances with different gender and difference in age of less than or equal 10 get the same prediction.

Next, we describe an approach for testing arbitrary given ML models with respect to some given fairness definition.

Testing approach

In this section, we describe the language for specifying fairness and also briefly discuss our verification-based-testing (VBT) approach which we employ for testing fairness. Note that fairness testing is an instance of metamorphic testing [START_REF] Segura | A survey on metamorphic testing[END_REF] in that we cannot check violation of the tested property on a single test input, but just on pairs of test inputs.

Fairness specification

Usually, approaches for fairness testing employ a fixed fairness definition and allows users to specify the set of protected features only. Our testing approach in addition allows the software engineer to state the fairness requirement itself. Our language is inspired by property-based testing approaches [START_REF] Claessen | Quickcheck: a lightweight tool for random testing of haskell programs[END_REF]. The user can specify assumptions on the inputs, in our case pairs of data instances, and assertions # Assumptions: index '0' is income, '1' is age and '2' is gender for i in range(0, 3): on the outcome (the prediction). The testing technique then tries to generate inputs satisfying the assumptions and violating the assertions.

if ( i == 2): assume('x[i ] != y[ i ]', i ) else : assume('x[i ] = y[i ]', i ) # Assertion Assert('model.predict(x) = model.predict(y)')
For the specification of assumptions, the user needs to know the attributes of data instances. These are fixed in a schema definition given in an XML configuration file (attributes and their types). Such schema files are often used to describe the format of training data in machine learning. In the assumptions, attributes of a data instance x can be accessed like arrays, i.e., x[0] is the value of the first feature of instance x and so on. Assumptions are then arbitrary boolean expressions over the attributes of two data instances, called x and y (instead of x and x ). The model itself can be referred to by the result of training a specific classifier on a given training data set. All parts of the fairness specification are written in Python.

As an example, consider the loan-granting setting of the previous section. The assumptions and assertion for individual discrimination (Def. 1) can be found in Figure 2. First, we train a classifier as to get the model (M ). Before specifying the property, some input parameters need to be fixed for our approach to work. For example, the no_of_instance defines number of data instances required to specify the property which is in this case 2 and the instance_list contains the instance variables (in this case is x and y). Also, the XML schema file and ML model to be checked need to be specified. There are several other optional parameters with default values.

For example, the default value of parameter no_of_cex is set to 'single', indicating the generation of a single counter example if the assertion is violated. If the user assigns 'multi' to this parameter, then multiple counter examples for i in range(0, 3):

if ( i == 2): assume('x[i ] != y[ i ]', i ) else : assume('0.01 * (abs(x[i ] -y[i ])) <= 0.1', i ) # Assertion Assert('model.predict(x) = model.predict(y)')
Fig. 3. Python code snippet corresponding to Definition 3 would be generated. After fixing the input parameters, we state assumptions and assertion. The testing approach will subsequently generate test inputs which fulfill the assumptions and violate the assertion (if possible).

Similarly, Figure 3 shows the code snippet for checking fairness with respect to Definition 3. Here we have elided the part on parameter setting, training etc. The only difference to the previous example is the specification of the distance function. The assume statement describes the distance metric we have defined earlier. The absolute value operator (|..|) is specified by abs. The expression to describe distance metric dist (i.e. the expression of assume) can be of the following form.

dist := d x,y , d x,y := k ⊕ (x[i] ⊕ y[i]) | k ⊕ (|x[i] ⊕ y[i]|)
where ⊕ ∈ {+, -, * , /}, ∈ {=, ≤, ≥, >, <, =} and , k ∈ R. Currently, our approach can deal with arbitrary distance metrics, which can be defined by using standard arithmetic operators. Although, the distance metric containing multiplication or division operations might lead to undecidability of the satisfiability question. Hence, using those operators might cause a significant slow down of our approach.

Verification-based testing

For generating test inputs, we employ verification-based testing which we have introduced for testing monotonicity of ML models in [START_REF] Sharma | Higher income, larger loan? monotonicity testing of machine learning models[END_REF]. The basic idea is to approximate the black-box model under test (MUT) by a white-box model, essentially a decision tree. The intention therein is to be able to apply verification techniques for property checking once we have a white-box model. Decision trees are a good candidate for such a white-box model since they are easily convertible into logical formulae so that we can use an SMT solver to verify properties on the tree. The idea of using a white-box approximator for a given black-box model is not new and studied in the areas of interpretable AI and testing of non-ML software. In AI, Guidotti et al. [START_REF] Guidotti | A survey of methods for explaining black box models[END_REF] uses an explainable white-box model to explain an unknown black-box model. In the testing domain, Papadopoulos and Walkinshaw [START_REF] Papadopoulos | Black-box test generation from inferred models[END_REF] use the inference of a predictive model from test sets to further Figure 4 depicts the basic workflow of our approach. The inputs to our approach are the predictive model M (MUT), the schema describing the set of features F and their types (e.g. int, float) used in the training of the model as an XML configuration file and an assume-assert fairness specification.

Our approach consists of four steps. Below, we describe the steps of our technique and explain the workflow in detail.

1. White-box model inference. First, we train a decision tree with a set of data instances called oracle data. We generate this oracle data (i.e., training data for the tree) by using the predictions of the MUT for some randomly chosen input instances (referred to as 'Prediction input' in Fig. 4). A decision tree learner is trained on the oracle data which results in a decision tree model approximating the given unknown black-box model.

Test generation.

Once we have generated the decision tree, the next step is to verify the given fairness property and thereby generate test inputs. For this, we use the state of the art SMT solver Z3 [START_REF] De Moura | Z3: an efficient SMT solver[END_REF]. First, we translate the decision tree into a logical formula describing how the classes are predicted for inputs x and x . Figure 5 shows the Z3 code for the decision tree in Figure 1. The data instance x (i.e. test input) is described by the features gender1, age1 and income1 whereas, test input x is described by gender2, age2 and income2.

The Z3 code of the tree is then complemented with code for the fairness specification. The assumptions of the fairness requirement become assert statements in Z3, the assertion becomes an assert statement in its negated form. The resulting formula is then checked for satisfiability, i.e., we check whether the decision tree allows for a prediction satisfying the assumptions in the fairness constraint, but not the assertion. If the formula is satisfiable, the SMT solver returns a satisfying assignment which is a counter example to this fairness constraint (however, not necessarily for the black-box model, so far just for the decision tree).

; Declaring components of x and x' and their classes (declare -fun gender1 () Int) (declare -fun income1 () Real) (declare -fun gender2 () Int) (declare -fun income2 () Real) (declare -fun age1() Int) (declare -fun age2() Int) (declare -fun class1 () Int) (declare -fun class2 () Int) ; Specifying prediction of decision tree (no=0, yes=1) ( assert (=> (and (= gender1 0) (< income1 1000)) (= class1 0))) For example, consider the Python code for checking individual discrimination (Def. 1) described in Figure 2. The assume statements in Python code are translated to (assert(and(not(= gender1 gender2))(= income1 income2) (= age1 age2))) as Z3 code in Figure 5. The assert condition is then added as (assert (not (= class1 class2))) to Z3. The assertion specified is basically negated in the logical formula in an attempt to generate a counter example violating the specified property. The last two lines of the code ask Z3 to check for satisfiability of all assertions and -if yes (Sat) -to return a logical model. The logical model gives an evaluation for the variables such that all assertions are fulfilled. For our example, it can be found in Figure 6.

The counter example returned by the SMT solver is a pair of data instances and their respective classes ((x, y), (x , y )). The corresponding classes are essentially the prediction given by the approximating decision tree. As the tree is only an approximation, the counter example produced might not be valid for the MUT. Hence, we consider it as a candidate counter example (candidate CEX in Fig. 4). In the next step we check whether this is a valid counter example by using the prediction of the MUT. If yes, we add the counter example as a test input to the test suite. If not, (x, M (x)) and (x , M (x )) are added to the or- acle data in order to increase precision of the approximation in later steps by re-training the decision tree.

When Z3 cannot find a counter example, hence giving 'Unsat' as output, the approximated decision tree is fair wrt. the given fairness constraint. Still, it might be the case that the MUT itself is not fair. Then our approach was unable to generate test inputs. In all our experiments this has however not occurred so far.

3. White-box model improvement. Once we have collected a larger set of test pairs (candidate counter examples, see below on how to get multiple counter examples), we examine the validity of those for the MUT M . If any of the candidate counter examples turns out to be also a valid one for the MUT, we have found a test case violating the specified fairness property. If we cannot find such a case, then the decision tree's prediction obviously differs from the MUT for this input. These cases will then be added to the oracle data to re-train the decision tree and thereby improve the approximation. With this new tree, test generation will be started once more.

4. Variation. The basic workflow depicted in Figure 4 is enhanced by one more step. As discussed in the previous step, if a counter example found by Z3 on computing fairness of the decision tree is invalid, the approximating tree needs to be made more precise. This can be easily achieved by adding the counter example to the oracle data and train the decision tree algorithm again. But training is a costly operation and hence it would be more efficient to train the tree only after gathering a sufficient number of invalid counter examples. To this end, we apply two strategies to produce several different logical models (i.e., counter examples) for the same logical query by using Z3 repetitively, namely branch pruning and data instance pruning. Basically, branch pruning inserts additional constraints into the logical formulae which tell the SMT solver not to generate counter examples following the same branches of the tree while data instance pruning tells Z3 to generate different data instances.

The detailed algorithms of our pruning techniques can be found in our earlier work [START_REF] Sharma | Higher income, larger loan? monotonicity testing of machine learning models[END_REF]. We use these two pruning techniques to generate multiple counter examples. In the previous works of fairness testing, the effectiveness of a technique is measured in terms of the number of valid test cases generated, i.e., test cases violating the fairness constraint. Hence, we run test generation until we reach a specified limit or no further test cases can be found.

Evaluation

We have implemented our technique in Python. The implementation of our approach is available online at https://github.com/arnabsharma91/fairCheck. While evaluating our approach we have focused on the following two research questions.

RQ1. How does verification based testing compare to existing fairness testing approaches? RQ2. Which pruning strategy performs better in computing unfairness?

We have carried out the following experiments to evaluate the research questions.

RQ1. We intend to compare how our approach performs in detecting unfairness compared to existing fairness testing techniques. Note however that there does not exist a fairness checking mechanism so far which can validate a blackbox model with respect to a user given fairness specification. Hence, we compare our approach only to fairness testing techniques with fixed fairness definitions. For this, we have chosen AEQUITAS [START_REF] Udeshi | Automated directed fairness testing[END_REF] and Symbolic Generation (SG) algorithm [START_REF] Aggarwal | Black box fairness testing of machine learning models[END_REF] which have both been designed to test a given black-box model for individual discrimination. We do not consider THEMIS [START_REF] Galhotra | Fairness testing: testing software for discrimination[END_REF] for our comparison as it has already been shown to be less effective than the other two approaches as stated by Zhang et al. [START_REF] Zhang | White-box fairness testing through adversarial sampling[END_REF]. The aforementioned techniques use the number of valid unfair cases generated within a specified limit of total generated test cases as their evaluation metric. The comparison between the three techniques is thus performed on this basis. We employ both data instance and branch pruning strategies for this experiment.

RQ2. For test generation, we have implemented branch and data instance pruning strategies to achieve better coverage of the decision tree. We intend to find out which strategy is better in finding unfair test cases. We use a different evaluation metric for this comparison. Instead of counting the test cases generated we compute detection rate when each of the strategies is applied individually. We have also used a similar approach in our earlier work [START_REF] Sharma | Higher income, larger loan? monotonicity testing of machine learning models[END_REF] to compare our pruning strategies. The detection rate is defined as #Valid test cases #Total test cases , i.e., we measure how many of the generated test cases (candidate counter examples) are really test cases violating the fairness definition.

Setup

We have performed the evaluation on two data sets, namely Adult and German credit data from the UCI machine learning repository2 . The Adult dataset contains 13 features and 32561 data instances, the German credit dataset has 21 features and 1000 data instances. We have chosen four classification algorithms for our experiments: Naive Bayes (NB), Random Forests (RF), Logistic Regression and Decision tree. All these have been taken from scikit-learn.

The choice of these algorithms and datasets is driven by the fact that they all have been used in the previous works of fairness testing. These ML algorithms are also frequently being used in decision making systems.

We have evaluated the accuracy score while generating predictive models and used the score to adjust the hyperparameters of the learning algorithms. We have taken AEQUITAS from the GitHub repository 3 . It was hardcoded for working with Adult dataset only. We have modified its code to make it work for any dataset. We have obtained the implementation of SG from [START_REF] Zhang | White-box fairness testing through adversarial sampling[END_REF]. For AEQUITAS and SG we have chosen the setting which gives the best performance. We have created oracle data in the verification-based testing approach by using a combination of random data instances and training data instances.

Finally, because all three approaches involve some sort of randomness, every experiment was carried out ten times. The results give the average of test cases generated out of these ten turns. The experiments were run on a machine with 2 cores Intel(R) Core(TM) i5-7300U CPU with 2.60GHz and 16GB memory using Python version 3.6.

Results

Next, we report on the findings of our experimental evaluation.

RQ1. Tables 1 and2 show the results of the experiments for RQ1. They give the number of test cases generated by each of the technique while using the four ML models obtained by training on Adult and German credit dataset, respectively. It can be inferred from the results shown that in most of the cases our technique can generate a larger number of test cases in comparison to SG and AEQUITAS.

RQ2. Figure 7 represents our results for the two pruning strategies for Adult and Credit datasets. Here, we compute individual discrimination with respect to the feature 'Gender'. It is evident from the results that data instance (short, instance) pruning performs better than branch pruning in computing individual discrimination.

We have also performed experiments to evaluate the efficiency of our approach. We have observed that for all the test cases we consider here, the maximum run time of our approach is 929.76 seconds. On average, our approach needs 450 seconds to generate test cases.

Limitations and Threats to Validity

Since we employ an SMT solver for computing fairness, verification-based testing is restricted to feature values and operations allowed by the solver. The datasets we consider in this work containing integer and real values. For categorical feature values, an encoding needs to be performed. But this is frequently done by ML algorithms in data preprocessing step.

A threat to the internal validity is the high degree of randomness involved in the techniques. First, the classifiers considered here use randomized algorithms for generating models. Thus, in principle we might get varying number of test cases to unfairness when training with the same classifier on exactly the same data set. To ensure a fair comparison, all three approaches were always started with the same model as input (training of MUTs is external to testing). All three approaches randomly generate data instances (AEQUITAS and SG for test data and VBT for oracle data). In addition to that, VBT and SG use a decision tree training algorithm which itself involves randomness. To mitigate these threats, all experiments were performed 10 times and the results give the average over these 10 runs.

Related work

We divide our discussion of related works in three parts. First, we discuss some works of fairness testing of predictive models, then mention some recent techniques for machine learning testing, and third discuss approaches using model inference in testing. Fairness testing. There exists a number of works discussing testing fairness of ML models. Galhotra et al. propose [START_REF] Galhotra | Fairness testing: testing software for discrimination[END_REF] black-box testing of predictive model for fairness. They introduce individual discrimination as a definition of fairness and give a confidence driven random testing technique to check it. They also experimentally show why the existing fairness definitions are not enough to detect discrimination in the ML model. However, their approach is less effective as they solely rely on random test case generation.

Later, Udeshi et al. propose AEQUITAS [START_REF] Udeshi | Automated directed fairness testing[END_REF] for individual discrimination detection. It first randomly searches for discriminatory input test cases. Once such test cases have been found, it tries to generate more test cases by perturbing the initial ones. They propose an automated technique to use the generated test cases for retraining the given model and then obtaining a fair one.

Our approach is closest to the work of Aggarwal et al. [START_REF] Aggarwal | Black box fairness testing of machine learning models[END_REF]. They generate a path of a decision tree from the black-box model under test by using a tool called LIME. This tool generates a small decision tree for local explanations of the predictions given by the model. After generating such a partial decision tree, they use dynamic symbolic execution to generate multiple test cases violating individual discrimination. In contrast, we approximate the entire black-box model by a decision tree. We then compute the test inputs on this tree. Also, we cater for checking the predictive model with respect to several fairness definitions instead of just individual discrimination.

In a more recent work, Zhang et al. [START_REF] Zhang | White-box fairness testing through adversarial sampling[END_REF] propose a fairness testing technique for Deep Neural Networks (DNN). They focus on individual discrimination by generating test cases through adversarial sampling. Like AEQUITAS, they also operate in two phases. Although their approach outperforms existing fairness testing approaches, they perform a white-box testing technique, hence are limited to DNNs.

Validating models. There exists a number of recent works which aim at validating properties of predictive models. One such important property of an ML model is robustness. In [START_REF] Huang | Safety verification of deep neural networks[END_REF], Huang et al. first propose this as a safety property and give a verification technique showing that a Deep Neural Network (DNN) guarantees postconditions to hold on its outputs when the inputs satisfy a given precondition. Pei et al. [START_REF] Pei | Deepxplore: Automated whitebox testing of deep learning systems[END_REF] later propose the first white-box testing technique based on differential testing approach to test DNNs for robustness. Sun et al. [START_REF] Sun | Concolic testing for deep neural networks[END_REF] propose a concolic testing approach to test DNNs.

In a very recent work, Lee et al. [START_REF] Lee | Effective white-box testing of deep neural networks with adaptive neuron-selection strategy[END_REF] propose a white-box technique for DNNs to generate test cases for checking robustness. They use an online algorithm to select the relevant neurons during the testing process and thus do not rely on a fixed strategy of selecting neurons for coverage. The experimental results show the effectiveness of their approach across diverse DNN models.

Recently, Sharma et al. [START_REF] Sharma | Testing machine learning algorithms for balanced data usage[END_REF] have proposed a property called balancedness on the learning algorithm. They perform specific transformations on the training data and check whether the learning algorithm generates a different predictive model after applying such transformations. Instead of checking the predictive model, this work focuses on testing the learning algorithm. A survey of different important properties arising in Machine Learning and their validation techniques can be found in [START_REF] Zhang | Machine learning testing: Survey, landscapes and horizons[END_REF].

Testing via model inference. The inference of a decision tree describing the behaviour of software has already been pursued by Papadopoulus and Walkinshaw [START_REF] Papadopoulos | Black-box test generation from inferred models[END_REF] as well as Briand et al. [START_REF] Briand | Using machine learning to refine category-partition test specifications and test suites[END_REF].

The former work is related to ours as it also translates the decision tree to logical formula in Z3. However, they do not use the tree to compute counter examples to the property to be tested. Instead, they use Z3 to generate test inputs covering different branches of the tree. Our approach on the other hand use the white-box model to generate targeted test inputs by using an established verification technique. Briand et al. use the decision tree in a semi-automated approach to the re-engineering of test suites. This approach requires the manual inspection of the decision tree by testers.

Conclusion

In this work, we have proposed a novel approach to test ML model for a user given fairness property. Our technique approximates the black-box model by a white-box model and then applies SMT solving techniques to compute fairness. It allows the user to specify the required fairness constraint herself, and with this goes beyond current fairness testing with hardcoded requirements.

We have evaluated the effectiveness of our approach by applying it to several ML models and found our approach to perform better than the existing fairness testing approaches in testifying a particular type of fairness in a large number of cases.

As future work, we plan to apply this scheme to validate other important properties of ML models. Our white-box model easily allows for checking other properties, like for instance robustness, just by applying a different check on the generated SMT code. Also, we would like to improve our framework by incorporating additional techniques to check statistical measures of fairness.

Fig. 1 .

 1 Fig.1. A decision tree for predicting who gets a loan

#

  Train the ML algorithm with Loan data containing 3 features: income, age, gender df = pd.read_csv('LoanData.csv') data = df.values x_train = data[:, : -1] y_class = data[:, -1] model = LogisticRegression() # Using Logistic regression classifier to train model = model.fit(x_train, y_class) # Setting the parameters of fairCheck fc = fairCheck(no_of_instance = 2, XML_file = 'input.xml', model = model, instance_list = (x,y))

Fig. 2 .

 2 Fig. 2. Python code snippet corresponding to Definition 1

Fig. 4 .

 4 Fig. 4. Basic workflow of verification-based testing

Fig. 5 .

 5 Fig. 5. Z3 code of the decision tree with individual discrimination constraint

Fig. 6 .

 6 Fig.6. Logical model for the query of Fig.5

Fig. 7 .

 7 Fig. 7. Performance of data instance and branch pruning in computing individual discrimination for Adult (left) and Credit dataset (right)

Table 1 .

 1 Comparison of number of test cases generated for Adult dataset

	Classifier	Prot. feature VBT	SG AEQUITAS
	Logistic Regression	Gender	133	37	80
	Logistic Regression	Race	66	58	25
	Random Forest	Gender	456	90	29
	Random Forest	Race	358	338	129
	Naive Bayes	Gender	75	18	6
	Naive Bayes	Race	43	40	30
	Decision tree	Gender	684	94	156
	Decision tree	Race	739	320	134

Table 2 .

 2 Comparison of number of test cases generated for German credit dataset

	Classifier	Prot. feature VBT	SG AEQUITAS
	Logistic Regression	Gender	182	60	38
	Logistic Regression	Age	127	164	3
	Random Forest	Gender	173	211	200
	Random Forest	Age	130	118	4
	Naive Bayes	Gender	16	3	0
	Naive Bayes	Age	27	20	0
	Decision tree	Gender	453	135	259
	Decision tree	Age	444	155	3

Note that the definition given here differs from that of[START_REF] Verma | Fairness definitions explained[END_REF] as we again do not consider probability distributions of outcomes here.

https://archive.ics.uci.edu/ml


Robert Sachtleben
email: robsac@uni-bremen.de

An Executable Mechanised Formalisation of an Adaptive State Counting Algorithm

Keywords: Complete Test Methods, Finite State Machines, Isabelle/HOL, Mechanised Proofs, Proof Assistants, Reduction

This paper demonstrates the applicability of state-of-the-art proof assistant tools to establish completeness properties of a test strategy and the correctness of its associated test generation algorithms, as well as to generate trustworthy executable code for these algorithms. To this end, a variation of an established test strategy is considered, which generates adaptive test cases based on a reference model represented as a possibly nondeterministic finite state machine (FSM). These test cases are sufficient to check whether the reduction conformance relation holds between the reference model and an implementation whose behaviour can also be represented by an FSM. Both the mechanical verification of this test strategy and the generation of a provably correct implementation are performed using the well-known Isabelle/HOL proof assistant.

Introduction

Objectives In this paper, we present a mechanised proof for a variation of the complete test strategy originally published by Petrenko and Yevtushenko in [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF] and provide a formalisation of selected algorithms described by the same authors in [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF] to calculate concrete test suites. We generate executable code from this formalisation to provide a trustworthy implementation of the test strategy.

The formalised strategy facilitates verifying the reduction conformance relation between two finite state machines (FSMs), of which the first serves as a reference model representing a specified behaviour, whereas the second represents the true behaviour of the system under test (SUT). Both FSMs may be nondeterministic but are assumed to be completely specified and observable. Additionally assuming an upper bound on the number of states contained in the (unknown) FSM representing the behaviour of SUT, the strategy generates finite test suites guaranteeing complete fault coverage using a state counting method. These test suites are adaptive and thus the number of tests applied to the SUT during testing depends on its observed behaviour. In many situations, the generated test suites are therefore significantly smaller than those generated using the well-known "brute force" strategy based on product FSMs1 , which requires O(|Σ I | mn ) test cases 2 for the same effect.

Motivation We advocate an approach to systematic testing that includes formal proofs of fault coverage capabilities of test strategies, so that no doubt with respect to their test strength remains. This process entails making explicit any underlying hypotheses, such as the specification of fault domains. Since complete test strategies are of considerable importance for the verification of safety-critical systems, the correctness of fault coverage claims for a given strategy is crucial from the perspective of system certification. Thus, we further advocate the use of proof assistants to check the proofs, as we believe that due to the large number of different test strategies and the often intricate nature of their corresponding proofs it cannot be expected that each proof is manually checked by many members of the testing community. Our previous work [START_REF] Sachtleben | A mechanised proof of an adaptive state counting algorithm[END_REF] supports this view, as it uncovered an ambiguity in the textual description of a test strategy, which could lead to incomplete implementations. In [START_REF] Sachtleben | A mechanised proof of an adaptive state counting algorithm[END_REF] we also voiced our hope that mechanised proofs could be used as artefacts presented to certification authorities as a means of showing that an applied test strategy provides the fault detection capabilities claimed for it. We now additionally believe that the use of provably correct code generated from formalisations could reduce the effort required to provide convincing arguments for tool qualification of tools employing such code.

Provably correct implementations of the test strategy formalised in this paper can be employed as trustworthy components in a large variety of testing applications. These include the generation of test suites for testing whether an SUT behaves only in ways allowed in a specification that can be represented as a (possibly nondeterministic) completely specified FSM, where nondeterminism indicates that the SUT may omit some reactions. Such specifications include communication protocols that contain optional behaviour. Additionally, many interesting conformance relations can be reduced to testing for this reduction conformance relation between completely specified FSMs, including quasiequivalence and quasi-reduction for incomplete specification FSMs (see [START_REF] Hierons | FSM quasi-equivalence testing via reduction and observing absences[END_REF]) and reduction for reactive I/O transition systems (see [START_REF] Huang | Complete model-based equivalence class testing for nondeterministic systems[END_REF]). This in turn allows for trustworthy implementations to be employed in the process of testing, for example, embedded systems against specifications given in SysML (see [START_REF] Huang | Complete model-based equivalence class testing[END_REF]).

Main Contributions To our best knowledge, this is the first time that a mechanised proof for the complete reduction test strategy elaborated in [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF] is presented. Moreover, trustworthy executable code is generated from a mechanically verified formalisation of an algorithm that realises the strategy, incorporating selected algorithms from [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF]. This provably correct implementation is used as the trustworthy core of a set of testing tools.

Related Work

The first complete state counting approach to reduction testing has been published in [START_REF] Petrenko | Testing deterministic implementations from nondeterministic FSM specifications[END_REF], specialising on the case of deterministic implementations being tested against nondeterministic reference models for language inclusion. Later, adaptive state counting has been proposed as an optimisation in [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF]. The restriction to deterministic implementations has then been dropped in later works considering a more general formulation of the problem, admitting both nondeterministic reference models and implementations. This has been studied in [START_REF] Hierons | Testing from a nondeterministic finite state machine using adaptive state counting[END_REF] and [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF], the latter being the article the present paper is based on.

To our best knowledge, applying proof assistants to testing has first been advocated in [START_REF] Brucker | Interactive testing with HOL-TestGen[END_REF]. Using Isabelle/HOL at its core, an integrated testing framework has been developed by the same authors and described in [START_REF] Brucker | On theorem prover-based testing[END_REF]. This framework allows for elaboration of test strategies (called test theorems in [START_REF] Brucker | On theorem prover-based testing[END_REF]), fault coverage proof, test case and test data generation in the same tool. Several cases of mechanised proofs establishing the completeness of testing theories are elaborated by the authors, not including the strategy analysed in the present paper.

Our approach to model-based testing (MBT) contrasts to that advocated in [START_REF] Brucker | On theorem prover-based testing[END_REF] in that we favour the use of specialised tools for strategy elaboration (Isabelle/HOL), modelling (FSM and SysML modelling tools), and test case and test data generation (RT-Tester [START_REF] Peleska | Model-based testing for avionic systems proven benefits and further challenges[END_REF] with SMT solver [START_REF] Peleska | Automated test case generation with SMTsolving and abstract interpretation[END_REF]). We base this preference on the possibility of performing SMT solving internally, without explicit interactions with the users, which requires less specialised expertise than the interactive handling of proof assistants. In this we agree with [START_REF] Bjørner | Z3 and SMT in industrial R&D[END_REF].

In [START_REF] Sachtleben | A mechanised proof of an adaptive state counting algorithm[END_REF] we presented a mechanised proof for the strategy described in [START_REF] Hierons | Testing from a nondeterministic finite state machine using adaptive state counting[END_REF], but in contrast to the present paper, this effort did not yet focus on providing a formalisation from which provably correct executable code could be generated.

Finally, tool qualification for model-based testing tools is discussed for example in [START_REF] Brauer | Efficient and trustworthy tool qualification for model-based testing tools[END_REF], where the replaying of test executions against the specification model is introduced as a measure to uncover potential faults in the untrusted test case generation. Our approach obviates the need for many such measures by employing trustworthy code to generate test suites.

Reference to Online Resources

The Isabelle/HOL session containing all the formalisations and proofs elaborated in this paper and a set of command line tools which employ the executable code generated from this session to generate test suites and apply them to SUTs, together with corresponding documentation and a short evaluation of the tools applied to a set of randomly generated FSMs, are publicly available on https://bitbucket.org/RobertSachtleben/ an-executable-formalisation-of-an-adaptive-state-counting.

Overview Section 2 provides a short overview of the test strategy presented in [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF]. Next, Section 3 describes our formalisation of this strategy in Isabelle and outlines the strategy of our mechanical completeness proof. Thereafter, Section 4 describes the generation of a trustworthy implementation, its integration into a set of test tools, and experiments performed using this implementation. Finally, we provide conclusions in Section 5.

The test strategy described in [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF] and formalised mechanically in this paper is employed to check whether an SUT, whose behaviour is assumed to correspond to some unknown finite state machine M , conforms to a specification, given as a finite state machine M , with respect to the reduction conformance relation. We first introduce the constructions used within this strategy as detailed in [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF].

Finite State Machines A finite state machine M = (Q, q 0 , Σ I , Σ O , h) is 5tuple consisting of a finite set Q of states, an initial state q 0 ∈ Q, finite sets Σ I and Σ O constituting the input and output alphabet, respectively, and a transition relation h ⊆ Q × Σ I × Σ O × Q where (q 1 , x, y, q 2 ) ∈ h if and only if there exists in M a transition from q 1 to q 2 for input x that produces output y. We define the size of M , denoted |M |, by the number |Q| of states it contains. Finally, the language L(M, q) denotes the set of all sequences x/ȳ ∈ (Σ I × Σ O ) * of input-output (IO) pairs such that M can react to x applied to q with outputs ȳ. The language of M itself, denoted L(M ), is the language of its initial state. We write xx /ȳ ȳ for the concatenation of IO-sequences x/ȳ and x /ȳ .

Primarily based on its transition relation, further properties of an FSM M can be distinguished: M is deterministic if for any state q in M and input x at most one transition exists. M is observable if for each contained state q, input x and output y there is at most one state q that is reached from q through a transition with input/output x/y, i.e. there is at most one state q in Q such that (q, x, y, q ) ∈ h. That is, the target state reached from some state with some input can be uniquely determined using the observed output. This property also extends to IO-sequences, as the state reached by an IO-sequence x/ȳ ∈ L(M, q) applied to state q is again uniquely determined. Next, M is completely specified if a transition exists from each contained state q for each contained input x. That is, any input x ∈ Σ I applied to a state q ∈ Q must produce some output. Furthermore, M is acyclic if L(M ) is finite, and a state q is a deadlock state if no transition from q exists. Also, M is single-input if for each state q all transitions from q share the same input component. Finally, an

FSM M = (Q , q 0 , Σ I , Σ O , h ) is a submachine of M if Q ⊆ Q and h ⊆ h hold.
In the remainder of this paper we assume every FSM to be both observable and completely specified, which is no restriction, as there exist techniques to complete any FSM (see [START_REF] Hierons | Testing from a nondeterministic finite state machine using adaptive state counting[END_REF]) and to transform it into a language-equivalent observable minimised machine [START_REF] Luo | Test selection based on communicating nondeterministic finite-state machines using a generalized wp-method[END_REF]. We do not, however, require any FSM to be deterministic. We furthermore assume that FSM M , representing the behaviour of the SUT, uses the same inputs as the specification M and satisfies |M | ≤ m.

The product machine (intersection) of FSMs M 1 = (S, s 0 , Σ I , Σ O , h 1 ) and M 2 = (T, t 0 , Σ I , Σ O , h 2 ) is an FSM PM = (S × T, (s 0 , t 0 ), Σ I , Σ O , h), which generates the language intersection L(PM) = L(M 1 ) ∩ L(M 2 ) by the following construction of h: ((s, t), x, y, (s , t )) ∈ h ⇐⇒ (s, x, y, s

) ∈ h 1 ∧ (t, x, y, t ) ∈ h 2 .
Finally, a state q 1 of an FSM M 1 is a reduction of some state q 2 of an FSM M 2 if and only if L(M 1 , q 1 ) ⊆ L(M 2 , q 2 ) holds, and M 1 is a reduction of M 2 if and only if the initial state of M 1 is a reduction of the initial state of M 2 .

State Preambles and Definitely Reachable States

A state preamble P of M = (Q, q 0 , Σ I , Σ O , h) for some q ∈ Q is an acyclic single-input submachine of M with q being its single deadlock state such that for every state q = q in P all transitions of M from q with the single input defined for q in P are also contained in P . That is, a state preamble P of M for q can be seen as a strategy for reaching q in every completely specified submachine of M and thus, for any sequence x/ȳ ∈ L(P ) ∩ L(M ) that reaches q in P , the state reached by x/ȳ in the SUT representation M must be a reduction of q for M to be a reduction of M . A state q of M is called definitely reachable if and only some state preamble of M for q exists. We say that a state of M is reached by a preamble P if it is reached by some x/ȳ that reaches q in P . We call such x/ȳ preamble sequences.

Note here that the initial state q 0 of M is definitely reachable by the preamble P 0 = ({q 0 }, q 0 , Σ I , Σ O , ∅). This implies that if a set P S of pairs (q, P ) of states of M and corresponding preambles contains (q 0 , P 0 ) and also L(M ) ⊆ L(M ) holds, then a minimal length IO-sequence xf /ȳ f and additionally a sequence xp /ȳ p that reaches a deadlock state in a preamble in P S must exist such that xp xf /ȳ p ȳf ∈ L(M ) \ L(M ) holds, since L(P 0 ) contains only the empty sequence . In the following, we will refer to sequences such as xf /ȳ f in short as minimal sequences to a failure extending xp /ȳ p if the set P S is obvious from the context. In the test strategy, for each definitely reachable state q of M a preamble P for q is used to identify states in the SUT representation that must conform to q, which include all states in M reached by sequences that reach q in P .

State Separators A state separator S of M for states q 1 and q 2 is an acyclic single-input FSM with two reachable deadlock states d 1 and d 2 such that (1) for any x/ȳ ∈ L(S) it holds that if x/ȳ reaches d 1 then x/ȳ ∈ L(M, q 1 ) \ L(M, q 2 ) holds whereas if x/ȳ reaches d 2 then x/ȳ ∈ L(M, q 2 )\L(M, q 1 ) holds, and (2) for any sequence x/ȳ ∈ L(S) reaching some non-deadlock state q in S with a single defined input x, S contains a transition from q with output y for each output y produced by any of the states reached in M by via x/ȳ from q 1 or q 2 to x. That is, S provides a strategy of reliably distinguishing q 1 and q 2 in all complete submachines of M . States q 1 and q 2 of M a called r-distinguishable if and only if a state separator of M for them exists. In the following, test separators S for states q 1 and q 2 are used to check whether certain states in M behave like only one of q 1 or q 2 , or neither of them.

Adaptively Testing of the Reduction Conformance Relation

The SUT conforms to the specification FSM M with respect to the reduction conformance relation if and only if the FSM M , which is assumed to represent the behaviour of the SUT, is a reduction of M . That is, the SUT conforms to M if and only if every behaviour of it is also admissible in M . As the languages of completely specified FSMs with nonempty input alphabets are infinite, it is not possible to check this property by simply enumerating L(M ) and L(M ) and therefore test suites must be applicable in a finite amount of time. In the case of nondeterministic FSMs this furthermore requires some fairness assumption that all reactions to some input can be observed within a finite number of applications of this input. In this paper, we employ the complete testing assumption (see [START_REF] Hierons | Testing from a nondeterministic finite state machine using adaptive state counting[END_REF]) and thus assume that there exists some upper bound k on the number of applications required to observe all reactions to a given sequence of inputs.

Furthermore, an SUT might exhibit only a proper subset of the behaviours of M , which enables the use of adaptivity in testing by controlling the application of inputs based on the observed behaviour of the SUT. An adaptive test case (ATC) A for FSM M is an acyclic single-input FSM that is output-complete for M (for every non-deadlock state there exists a transition for every output of M ) and which may contain a designated deadlock state fail. FSM M in state q passes A if and only if there exists no sequence in L(A) ∩ L(M , q ) that reaches fail in A. Applying A to M thus reduces to calculating L(A) ∩ L(M , q ) and checking the states reached in A, which is feasible as L(A) is finite.

For example, a state separator S of M for q 1 and q 1 can be transformed into an ATC I q1 that checks whether the state it is applied to behaves like q 1 and not like q 2 by replacing d 2 with fail and adding to every non-deadlock state q a transition to fail for every output of M that is not produced by q in S.

Finally, adaptive test cases can be concatenated at their deadlock states. Given ATCs A 1 and A 2 and a deadlock state d = fail of A 1 , A 1 @ d A 2 denotes the ATC created by replacing d in A 1 with the initial state of A 2 and inserting all transitions and other states of A 2 into A 1 . For simplicity we assume here that the state sets of ATCs are pairwise disjoint, ensuring that the @ operator is associative and well-behaved when concatenating multiple ATCs.

Overview of the Formalised Adaptive State Counting Algorithm

The adaptive state counting algorithm re-verified in this paper creates a test suite for M and an assumed upper bound m on the number of states in M as a set of adaptive test cases. This is performed by first calculating a preamble for each definitely reachable state of M and a state separator for every pair of r-distinguishable states in M , followed by a process of extending sequences from the definitely reachable states until they are too long to be proper prefixes of any minimal sequence to a failure, resulting in so-called traversal sets. The termination criterion for this extension is based on the number of r-distinguishable states of M encountered during the application of a sequence, which can constitute a lower bound on the number of states in any non-conforming FSM M . Finally, a test suite is constructed by concatenating preambles, extended sequences and state separators in accordance with this termination criterion.

Traversal Sets Let RD denote the set of all maximal sets of pairwise rdistinguishable states of Q. Given a set R ∈ RD let R dr denote the subset of R containing only definitely reachable states. Note that every state of M is contained in some such R and that R dr may be empty.

For every definitely reachable state q of M the set N m (q) of m-traversal sequences is then constructed starting from the empty sequence by extending input sequences until they satisfy the following rule: An input sequence x is not extended further if for all x/ȳ ∈ L(M, q) there exists some R ∈ RD such that x/ȳ applied to q visits states from R at least (m -|R dr | + 1) times, where a state is visited if it is reached by any nonempty prefix of x/ȳ applied to q.

From N m (q) the traversal set T m (q) is constructed as the set containing for every x ∈ N m (q) all x/ȳ ∈ L(M, q) such there exists some R ∈ RD whose states are visited exactly (m -|R dr | + 1) times along x/ȳ applied to q, while this does not hold for any proper prefix of x/ȳ. We call R a terminating set of x/ȳ. Finally, from each x ∈ N m (q) an acyclic observable FSM M q,x with language L(M q,x ) = {x /ȳ ∈ T m (q) | x is a prefix of x} is created such that any two sequences in M q,x reach the same state in M q,x only if they reach the same state if applied to q in M . This FSM can then be further simplified as described in [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF]. The adaptive test case T C(q, x) denotes the output completion of M q,x .

Test Suite Generation Given a preamble P q for every definitely reachable state q of M and for each state q in M a set ID q containing for each q in M that is r-distinguishable from q an adaptive test case I q of a state separator S of M for q and q , a test suite TS is created from an empty set as follows: For each definitely reachable state q of M , each x ∈ N m (q), each T C(q, x) and each set {x 1 /ȳ 1 , . . . , xk /ȳ k } of all sequences of length |x| in L(T C(q, x)) that do not reach fail, a set of adaptive test cases T of the following form is added to TS, where q i denotes the state reached by applying xi /ȳ i to q, t i denotes the deadlock state reached by applying xi /ȳ i to the initial state of T C(q, x), T C(P q ) is the adaptive test case created from the output completion of P q , and each I qi ∈ ID qi is only concatenated onto one ATC for each xi /ȳ i :

T := T C(P q )@ q T C(q, x)@ t1 I q1 @ t2 I q2 . . . @ t k I q k Applying test suite TS to an SUT thus essentially consists of applying the traversal sets after the preambles and applying after each such sequence a set of ATCs created from state separators that r-distinguish the state reached by the sequence from all states it is r-distinguishable from.

For the formalisation and implementation described in the following sections we have chosen a different representation of the test suite and its test cases, but the underlying strategy remains unchanged. We furthermore integrate the optimisation already described by Petrenko and Yevtushenko in [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF] that it is not always necessary to distinguish the target of some x/ȳ ∈ T m (q) from all states it is r-distinguishable from, as it is sufficient to r-distinguish the target from other states in some R ∈ RD only if R is used in the termination criterion of some sequence of which x/ȳ is a prefix (see the use of Id(s , R β ) in [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF]Algorithm 2]).

The Mechanised Proof

Isabelle/HOL Isabelle is a generic proof assistant featuring an extensive implementation of higher-order logic (Isabelle/HOL). We chosen this logic as the base for our formalisation, as it is highly expressive and already contains many useful definitions and theorems. For an introduction to Isabelle see Nipkow et al. [START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF]. The Isabelle core libraries are further extended by the Archive of Formal Proofs (see www.isa-afp.org). The Isar (Intelligible Semi-Automated Reasoning) proof language offered in Isabelle distributions allows for proofs to be written in a human-readable style [START_REF] Wenzel | Isabelle, Isar -a versatile environment for human readable formal proof documents[END_REF]. Our previous paper [START_REF] Sachtleben | A mechanised proof of an adaptive state counting algorithm[END_REF] contains an exemplary Isar proof on FSM properties. Isabelle is also able to automatically generate executable code from many formalisations written in it, which we use in Section 4 to generate a trustworthy implementation of the formalised test strategy. The correctness of this translation process is proven in [START_REF] Haftmann | Code generation via higher-order rewrite systems[END_REF], which also describes how the code generator can serve to facilitate program and data refinement.

Data Structures In our Isabelle/HOL formalisation we define FSMs as records (type fsm-impl) which we then restrict to well-formed FSMs (type fsm), where an FSM M = (Q, q 0 , Σ I , Σ O , h) is well-formed if its component sets are finite and additionally This follows the classical definition of FSMs more closely than the definition in our previous work [START_REF] Sachtleben | A mechanised proof of an adaptive state counting algorithm[END_REF] and also avoids cluttering proofs with well-formedness assumptions on the employed FSMs. Consider, for example, the following very natural definition of completely specified FSMs in our Isabelle formalisation3 :

q 0 ∈ Q and h ⊆ Q × Σ I × Σ O × Q hold.
completely-specified M = (∀ q∈states M .∀ x ∈inputs M .∃ q y.(q,x ,y,q )∈transitions M )

We represent state preambles and separators simply as FSMs, but we represent test suites as values of a new datatype such that a test suite TS = (PS, tps, rds, seps) consists of (1) a set PS of pairs (q, P q ) for each definitely reachable state q, (2) a map tps from each definitely reachable state to the traversal sequences starting from it, (3) a map rds assigning to each pair (q, x/ȳ), consisting of a definitely reachable state and a traversal sequence starting from it, all states that the target of x/ȳ needs to be r-distinguished from, and (4) a map seps assigning to each pair of r-distinguishable states (q 1 , q 2 ) at least one state separator S with corresponding deadlock states d 1 and d 2 .

This representation also requires a new formulation of the pass relation. We say that M passes test suite TS = (PS, tps, rds, seps) for M , denoted passes test suite M TS M in the Isabelle formalisation, if (1) M passes TC(P q ) for every (q, P q ) ∈ PS, (2) for every (q, P q ) ∈ PS and x/ȳ ∈ tps(q), every reaction of M in a state reached by P q to any prefix of x is also prefix of some sequence in tps(q), and (3) for every (q, P q ) ∈ PS, x/ȳ ∈ tps(q), q ∈ rds(q, x/ȳ) and (S, d 1 , d 2 ) ∈ seps(q, q ), M in a state reached by P q followed by x/ȳ passes the adaptive test case I q created from S. Note that this different representation and formulation does not affect the result of applying a test suite TS against the SUT: M passes TS represented as a set of ATCs if and only if passes test suite M TS M holds.

Proof Strategy

The first main goal of our formalisation is to prove that the formalised strategy is complete. That is, an SUT should pass a generated test suite if and only if it is a reduction of its specification. We split this proof into two parts by first formulating a sufficient condition such that any test suite satisfying it is complete, and then proving that the test suites generated by the formalised strategy do satisfy the condition. We will refer to this condition as the completeness predicate and describe it and its formulation in Isabelle in Subsection 3.2.

An overview of the steps performed in the overall proof is given in Figure 1: Let TS be a test suite generated by the formalised strategy. By construction (outlined in Subsection 2.1, implemented in Section 4), TS satisfies the completeness predicate and is also finite. All further proofs then only rely on these properties and the assumptions on the structure of M (observable, completely specified, same inputs as M , |M | ≤ m). M can fail a test suite satisfying the completeness predicate only if a behaviour of M is observed that is not admissible in M , and hence TS is sound : if M is a reduction of M , then it passes TS. The main effort in establishing completeness thereafter lies in proving TS to be exhaustive: if M is not a reduction of M , then M must not pass TS. This is realised via a proof by contradiction detailed in Subsection 3.2. Finally, completeness follows from soundness and exhaustiveness and still holds if test suites are reduced to finite prefix-free sets of IO-sequences (see Section 4).

The formalisation in Isabelle is split into several theory files covering separate aspects of the proof: First, files FSM Impl.thy, FSM.thy and Product FSM.thy provide basic definitions and properties for finite state machines. Next, the files State Preamble.thy, State Separator.thy and Traversal Set.thy respectively introduce the three main components of the test suite and algorithms for their computation. These are then combined within Test Suite.thy, which defines the completeness property and shows that each satisfying test suite is complete. Finally, an algorithm for calculating complete test suites is provided in Test Suite Calculation.thy and refined in further theory files. Overall, the formalisation effort comprises 18 theory files containing a total of 621 lemmata, which can be verified within 201 seconds using Isabelle2020 on a Ryzen 5 3600 CPU and Ubuntu 18.04. Most of these lemmata prove general properties on FSMs and related algorithms and are not restricted to any specific test strategy, allowing their reuse in future formalisation projects employing FSMs. TS is exhaustive:

passes test suite M TS M =⇒ L(M ) ⊆ L(M )
[passes test suite exhaustiveness] some minimal length sequence xf /ȳf exists that extends some preamble sequence xp/ȳp ∈ L(Pq) of some (q, Pq) Fig. 1: Overview of the overall proof strategy employed in the mechanised formalisation, with a focus on the proof of exhaustiveness of generated test suites. Names in square brackets indicate lemmata in the Isabelle formalisation. Predicate implies completeness is a shortened version of the completeness predicate described in Section 3.2 for a greedy strategy of calculating RD .

used in TS to a failure xp xf /ȳp ȳf ∈ L(M ) \ L(M ) some prefix x f /ȳ f of xf /ȳf is contained in T m (q) (

A Completeness Predicate for Reduction Testing

The test suite generation strategy outlined in Subsection 2.1 uses the set RD of all maximal sets of pairwise r-distinguishable states of M in its termination criterion for the traversal sets. As enumerating all those sets can be reduced to the problem of listing all maximum cliques of a graph in which two states are connected if they are r-distinguishable, this can prove computationally expensive for larger FSMs. To facilitate algorithms that use only a proper subset of RD, we have formulated the completeness predicate with respect to a test suite TS = (PS, tps, rds, seps), M , the assumed bound m ≥ |M |, and a subset RD of RD. The predicate is given in the Isabelle formalisation as the function implies completeness for repetition sets and is satisfied if the following properties hold: (1) PS contains (q 0 , P 0 ) and thus the trivial empty preamble, (2) for every (q, P ) ∈ PS, P is a preamble of q and tps(q) contains the traversal set T m (q), (3) all (S, d 1 , d 2 ) ∈ tps(q 1 , q 2 ) are state separators of q 1 and q 2 with corresponding deadlock states, (4) every state q of M is contained in some set in RD , (5) if two traversal sequences x1 /ȳ 1 = x2 /ȳ 2 in tps(q) are each prefix of a sequence in T m (q) terminated by some R ∈ RD and both sequences applied to q reach distinct states in q 1 , q 2 ∈ R, then q 2 ∈ rds(q, x1 /ȳ 1 ) and q 1 ∈ rds(q, x2 /ȳ 2 ), ( 6) if a traversal sequence x/ȳ ∈ tps(q) is prefix of a sequence in T m (q) terminated by some R ∈ RD and reaches some q 1 ∈ R if applied to q, then for any q 2 ∈ R dr \ {q 1 } it holds that q 2 ∈ rds(q, x/ȳ) and q 1 ∈ rds(q 2 , ), and ( 7) for each R ∈ RD , if any traversal sequence is terminated by R, then for each pair of distinct states q 1 , q 2 ∈ R dr it holds that q 2 ∈ rds(q 1 , ) and q 1 ∈ rds(q 2 , ).

To summarise, TS and RD are complete for reduction testing with respect to M and m if they are produced by a strategy such as that described in Subsection 2.1, without specifying many restrictions on the actual implementation of such a strategy. Properties (1) to (4) require the test suite to consist of actual preambles, state separators and traversal sets, whereas properties (5) to [START_REF] El-Fakih | Incremental and heuristic approaches for deriving adaptive distinguishing test cases for nondeterministic finite-state machines[END_REF] describe where ATCs need to be applied in order to distinguish states. Note here that these latter three properties structurally closely resemble conditions 1. to 3. in Theorem 1 of [START_REF] Dorofeeva | An improved conformance testing method[END_REF], which describes the H-method for equivalence testing of FSMs.

Finally observe that the soundness of any test suite TS satisfying the predicate follows directly from the reformulation of the pass relation, as satisfaction requires that application of TS entails only the application of preambles followed by corresponding traversal sets followed by corresponding state separators, and thus only of IO-sequences in L(M ), for which no reduction of M may fail.

Completeness of Test Suites Satisfying the Completeness Predicate

Let test suite TS and subset RD of RD satisfy the completeness predicate with respect to M and an assumed upper bound m ≥ |M |. Then the exhaustiveness of TS follows from a classical state counting argument by establishing a lower bound greater than m on the number of states contained in any M that is not a reduction of M but that passes TS, see for example [START_REF] Hierons | Testing from a nondeterministic finite state machine using adaptive state counting[END_REF] and [START_REF] Sachtleben | A mechanised proof of an adaptive state counting algorithm[END_REF]. We have used this approach in a proof by contradiction: if we assume that M passes TS while also L(M ) ⊆ L(M ) holds, then some minimal sequence to a failure xf /ȳ f extending some preamble sequence xp /ȳ p of some (q, P q ) in the preambles of TS must exist, which is not applied in TS. Hence, some proper prefix x f /ȳ f of xf /ȳ f must be contained in T m (q) and terminated by some R ∈ RD . Now xp x f /ȳ p ȳ f cannot repeat any state of the product of M and M , as this would allow for a sequence to a failure shorter than xf /ȳ f . Furthermore, by construction of the traversal sequences, x f /ȳ f applied after xp /ȳ p together with the preambles in TS must visit states of R at least (m + 1) times in M . These last two properties, in conjunction with M passing all applied state separators of conditions ( 5) to [START_REF] El-Fakih | Incremental and heuristic approaches for deriving adaptive distinguishing test cases for nondeterministic finite-state machines[END_REF] of the completeness predicate, require M to contain at least (m + 1) distinct states, which provides a contradiction to the assumed upper bound |M | ≤ m. Completeness of TS follows from exhaustiveness and the previously established soundness. That is, M passes TS if and only if M is a reduction of M .

A Trustworthy Implementation

Complete Algorithms The calculation of a test suite satisfying the completeness predicate can be separated into five major steps: (1) the calculation of definitely reachable states of M and corresponding preambles, (2) the calculation of r-distinguishable state pairs in M and corresponding state separators, (3) the calculation of a subset RD of RD, (4) the calculation of traversal sets from each definitely reachable state, also storing the corresponding terminating R ∈ RD , and (5) the combination of these results into a test suite by calculating for each definitely reachable state and each traversal sequence from this state the states it must be r-distinguished from. Figure 2 depicts these steps and their corresponding functions in the Isabelle formalisation within the box for function generate test suite greedy. This function implements the test strategy described above using a simple greedy algorithm to calculate a set RD .

Step (1) of the above calculation is realised in the formalisation using function calculate state preamble from input choices to construct a state preamble for a given state q if it exists, based directly on Algorithm 1 of [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF]. It creates a preamble by starting from q and analysing backward reachability, iteratively adding not yet backwardly reached nodes q and inputs x such that all transitions from q for x in M reach nodes added in previous iterations, including q. If this process adds the initial state of M , then the selected states and corresponding inputs induce a valid preamble for q. State separators are calculated in a similar way to establish step (2), starting from the deadlock states of a partial separator, again as described in [START_REF] Petrenko | Adaptive testing of deterministic implementations specified by nondeterministic FSMs[END_REF]. Based on these results, we have formalised two possible implementations for step (3): first by naively enumerating all elements of RD and second by a greedy algorithm that calculates for each state q a set R q ∈ RD by starting from R q := {q} and iteratively adding states that are r-distinguishable from all states currently in R q until R q is maximal. Next, we realise step (4) by performing a straightforward enumeration of paths from each definitely reachable state until the corresponding traversal sequence can be terminated by some R ∈ RD . Finally, the implementation of step (5) follows above description.

Test Suites as Sets of IO-Sequences

To facilitate easier integration with other tools and storage of calculated test suites, we additionally provide algorithms to reduce test suites to finite prefix-free sets of IO-sequences, which might be stored by data structures as simple as lists. The previously introduced Function generate test suite greedy performs this transformation as a final step by extracting from the calculated test suite all IO-sequences xp xt xr /ȳ p ȳt ȳr such that xp /ȳ p is a sequence reaching q in some preamble P q , (q, P q ) is contained in TS, xt /ȳ t is a traversal sequence in T m (q) and xr /ȳ r is a sequence in some state separator applied thereafter that does not reach fail. The resulting finite set of IO-sequences is then simplified by removing all sequences that are proper prefixes of other contained sequences.

Let TS be the calculated test suite represented as defined in Section 3. Then, by construction and depicted as the last step of Figure 1, the reduction of TS to a finite set (or list) TS L of IO-sequences satisfies the following property:

L(M ) ⊆ L(M ) ⇔ passes test suite M TS M ⇔ ∀xxx /ȳy ȳ ∈ TS L : ∀xx/ȳy ∈ L(M ) : ∃xxx /ȳy ȳ ∈ TS L
That is, an SUT representation M passes TS if and only if for any xx/ȳy that is prefix of any sequence in TS L the SUT reacts to x applied after x/ȳ only with outputs y such that xx/ȳy is also prefix of some sequence in TS L . Note here that M is not referenced in the bottom right side of the bi-implications. Test suite TS L can thus be applied to an SUT in practice by applying to the latter each contained IO-sequence (test case) at least k times (to satisfy the complete testing assumption). A test case x 1 . . . x n /y 1 . . . y n is applied by iteratively applying each x i (beginning at x 1 ) and observing the corresponding response y i of the SUT, continuing only if y i = y i . The SUT passes the application of x 1 . . . x n /y 1 . . . y n if and only if the observed SUT response x 1 . . . x j /y 1 . . . y j is prefix of some sequence in TS L . Finally, by the above property TS L must be a subset of L(M ) and hence the SUT passes a test case if and only if the observed response of the SUT to the test case is be admissible in M , as L(M ) is prefix closed.

Refinement and Extensibility Isabelle provides a powerful refinement mechanism to generate more efficient code from definitions, which we have employed in theory file Test Suite Calculation Refined.thy to refine both data structures and algorithms. First, we have used the Containers framework [START_REF] Lochbihler | Light-weight containers for isabelle: efficient, extensible, nestable[END_REF] to represent sets using data structures such as red-black-trees wherever possible, which improves on Isabelles default set implementation as lists. Furthermore, we provide several code equations that allow the code generator to replace function definitions by (provably equivalent) definitions that are more efficient, for example by extracting common subexpressions to avoid repeated evaluation of identical expressions. These refinements have allowed us to use simple definitions that are easy to use within the proofs, while still being able to use more efficient definitions in code generation. They are also extensible as it is possible to add further code equations and overwrite existing ones.

New variations or optimisations of the test strategy described in this paper can furthermore easily be proven complete by establishing that they satisfy the completeness predicate, as we have decoupled implementation details from the proof of completeness via this criterion. To prove complete, for example, an alternative test strategy resulting from replacing the currently used algorithm for calculating state separators by one of the algorithms presented in [START_REF] El-Fakih | Incremental and heuristic approaches for deriving adaptive distinguishing test cases for nondeterministic finite-state machines[END_REF], it is sufficient to prove in Isabelle that this new algorithm generates valid state separators and to provide for the new test strategy a lemma analogous to lemma calculate test suite for repetition sets sufficient and finite, which proves satisfaction of the completeness predicate.

Generated Test Tools

In theory file Test Generator Export Code.thy we generate Haskell code for function generate test suite greedy, which we then use to implement a comprehensive test tool set able to test an SUT given as a function in C against a specification FSM. This tool set is available at the provided online resources (see Section 1) and consists of two parts: a test suite generator which uses the code generated from Isabelle to generate a test suite for a given specification FSM, and a test harness which applies each test case in a given test suite against an SUT, using the above definition of applying test cases, to calculate a verdict on whether the SUT conforms to the specification. This verdict is PASS if and only if all test cases pass. Figure 2 depicts the workflow.

The two tools each contain fewer than 200 lines of code in addition to the generated code and serve only as interfaces between the specification FSM, test suites and the SUT. They can thus be verified manually with little effort. Together with the trustworthiness of the provably correct generated code (see [START_REF] Haftmann | Code generation via higher-order rewrite systems[END_REF]) facilitating the test suite generator, this has important implications on tool qualification efforts of test tools that employ the above tools: First, the fault detection capabilities of each generated test suite are established by mechanised proofs within our formalisation, providing evidence that it is complete for the fault domain of SUTs whose behaviour can be represented by an FSM M that is completely specified, observable, contains at most m states, and has the same nonempty set of inputs as M . Verification of these proofs themselves reduces to verifying the used definitions, as any proof is verified automatically by the small trustworthy inference kernel of Isabelle, even when using sophisticated proof methods (see [START_REF] Blanchette | Automatic proof and disproof in isabelle/hol[END_REF]). Furthermore, as generated test suites are a proper subsets of L(M ), no test case application following the previously described procedure can introduce undetected SUT failures by reporting some test case as passed even though the observed response of the SUT to it is not admissible in the specification. Thus, by verification of the test case application mechanism in the test harness, the first of two hazards introduced by model-based test tools as identified in [START_REF] Brauer | Efficient and trustworthy tool qualification for model-based testing tools[END_REF] can be mitigated. Mitigation of the second hazard identified there, undetected coverage failures due to test executions failing to meet test case specific pre-conditions, can for our fault domain be reduced to verifying that the test harness resets the SUT to an initial state before applying each test case, as this is the only pre-condition we require. Since the integration of the SUT into the test harness is highly dependent on the SUT, we have not included the test harness in the Isabelle formalisation, but we believe that the very small provided implementation can easily be verified for a given SUT. Such a verification of the test harness tool and the integration of the generated code into the test suite generator tool then obviates measures such as replay of observed behaviours against the specification (see [START_REF] Brauer | Efficient and trustworthy tool qualification for model-based testing tools[END_REF]) arising from untrusted test case generators.

Statistical Experiments

We have applied the generated implementation on a synthetic data set containing randomly generated FSMs of varying size and extend of nondeterminism, where we define the degree of nondeterminism of an observable FSM M = (Q, q 0 , Σ I , Σ O , h), denoted d nondet (M ), as the ratio between the number of transitions such that other transition with the same source and input exist, and the overall number |h| of transitions in M :

d nondet (M ) = |{(q, x, y, q ) ∈ h | ∃y , q : (q, x, y , q ) ∈ h ∧ y = y }| / |h|
The synthetic data set contains for each configuration (s, d) with 4 ≤ s ≤ 20 and d ∈ {0.1, 0.2, 0.3, 0.4} a collection of 1000 randomly generated FSMs M with 6 inputs and 4 outputs such that |M | = s and M has been generated for a target value of d nondet (M ) = d using the fsmlib-cpp library 4 , an open source project containing many fundamental algorithms for processing FSMs. We have restricted the range of values for d to comparatively small values, as we believe that specifications of safety-critical systems often exhibit nondeterminism only to a very limited extend. Figure 3 shows the average size (number of test cases) of test suites calculated for this data set, using an upper bound m = |M |, and the average time required for each calculation as measured on a Ryzen 5 3600 CPU calculating test suites for 8 FSMs in parallel. These results indicate that, for a fixed input alphabet, the average size of generated test suites correlates with the extend of nondeterminism in the specification. This follows in particular from the definition of traversal sets, since a higher degree of nondeterminism indicates, on average, a higher number of outgoing transitions for each state and thus an increase in the number of distinct IO sequences originating at each state. Note also that the calculated test suites are significantly smaller than those created using the "brute force" strategy of enumerating all input sequences of length |M | • m, resulting in test suites of size at least |Σ I | m•|M | . We conjecture that the execution time of the generated implementation can be drastically reduced by further refinement and the employment of more sophisticated algorithms in particular for the calculation of state separators.

The data set, instructions on how to employ the generated implementation to calculate test suites, and detailed results for each FSM contained in the data set are available as part of the online resources referenced in Section 1.

Conclusions and Future Work

We have provided the first comprehensive mechanised proof of the test strategy elaborated by Petrenko and Yevtushenko in [START_REF] Petrenko | Adaptive testing of nondeterministic systems with FSM[END_REF] and established the correctness of an implementation of this strategy. As a second main contribution, we have used the mechanised formalisation to generate from it trustworthy executable code and embedded it into a set of test tools that facilitate the calculation and application of test suites. Further investigations are required to quantitatively compare this generated implementation against hand-crafted implementations of the formalised test strategy. The theories and proofs of the formalisation, as well as the implementation of the test strategy itself, have been developed using the Isabelle/HOL tool, indicating the suitability of the latter to perform such undertakings with acceptable effort.

We advocate the use of mechanised proofs of the completeness of test strategies and the use of provably correct automatically generated implementations, because such strategies and guarantees of their fault detection capabilities are of considerable value in model-based testing of safety-critical systems, where undiscovered flaws in test strategies or their implementations might lead to insufficient actual test strength and therefore to the possibility of fatal errors in the system under test being left undiscovered. The use of provably correct automatically generated implementations can furthermore mitigate hazards introduced by model-based test tools and obviate measures against untrusted test case generators, simplifying tool qualification efforts of test tools that employ such implementations.

  TS is finite (is finite test suite TS) TS satisfies the completeness predicate for M and m (implies completeness TS M m) and test suite TS calculated for specification M and upper bound m (calculate test suite greedy M m = TS) by [calculate test suite for repetition sets sufficient and finite]: Assumptions on M , including |M | ≤ m TS is sound: L(M ) ⊆ L(M ) =⇒ passes test suite M TS M [passes test suite soundness]

Fig. 3 :

 3 Fig. 3: Average size (left) and calculation time in s (right) of test suites for randomly generated, completely specified, observable and minimised specification FSMs M for m = |M |, depending on |M | and target value d for d nondet (M ).

  Overview of the workflow of using the test suite generator and test harness command line tools to test an SUT. Dark grey shadings indicate inputs and SUT integration provided by the user, while light grey shadings indicate the trustworthy code generated from the Isabelle formalisation.

		test-suite-generator command line tool
	specification FSM M			parsed FSM M
	[as a .fsm file]			[as a value of type fsm]
		function generate test suite greedy (generated from Isabelle)
		calculate preambles for definitely reachable states of M
		[function d reachable states with preambles]
		calculate state separators for r-distinguishable states of M
		[function r distinguishable state pairs with separators]
		calculate maximal sets of pairwise r-distinguishable states
		[function maximal repetition sets from separators list greedy]
	number a of assumed
	maximum additional		calculate traversal sets
	states in the SUT	[function calculate test paths]
	[as an integer]
		combine results to test suite
		[function combine test suite]
		reduce test suite to a prefix-free set of IO-sequences
		[function test suite to io maximal]
	number k of repetitions to
	perform for each test case		stored test suite
	[as an integer]	[as a file containing one IO-sequence per line]
	test-harness command line tool
	SUT	SUT wrapper [C functions sut init, sut reset, sut]	apply test cases (IO-sequences)
		PASS		FAIL
		verdict?
	The SUT conforms to the specification M w.r.t. the	An IO-sequence x/ȳ ∈ L(SU T ) \ L(M ) is observed
	reduction conformance relation (under the described	during application of the test suite. The SUT hence
	assumptions).		does not conform to the specification M w.r.t. the
	[lemma test harness soundness]	reduction conformance relation.
	Fig. 2:

This strategy has been described, for example, in the lecture notes[START_REF] Peleska | Test Automation -Foundations and Applications of Model-based Testing[END_REF] Section 4.5].

|ΣI | is the size of the input alphabet, n the number of states in the reference model, and m an upper bound for the number of states in the SUT model.

Function application in Isabelle is performed in a functional programming style without braces. For example, f(x,y,z) is written in Isabelle as f x y z.

Publicly available for download at https://github.com/agbs-uni-bremen/ fsmlib-cpp. Random FSMs for a given degree of nondeterminism have been constructed using method createRandomFsm of class Fsm.

Acknowledgements I would like to thank my doctoral thesis supervisor Jan Peleska for several helpful discussions.