Clément Robert

Jérémie Guiochet

Hélène Waeselynck

Vittorio Luca

Sartori

TAF: a tool for diverse and constrained test case generation

Keywords: test, test input generation, fuzzing, autonomous robots, simulation

The generation of test cases may have to accommodate size-varying data structures and semantic constraints between the data elements. This often requires the development of custom generators. In this paper, we introduce a novel generic tool to generate constrained and diverse test cases from a data model. First, the user defines the model using an XML-based domain-specific language. Then TAF generates diverse test cases by combining random sampling with the use of an SMT solver. The capabilities of the tool are demonstrated by four examples of models coming from various application domains: virtual crop fields for testing an agriculture robot, bitmap images with a graduated background, a population of taxpayers in a tax management system, and tree structures of diverse sizes and heights. We show how TAF performs in terms of data diversity and execution time. We also provide some comparison results with an UML-based tool using SMT solving.

I. INTRODUCTION

Many applications require test cases with rich and structured data content. For example, the starting point of this work was the simulation-based testing of mobile robots. In this context, a test case includes the description of the 3D-scene in which the robot is placed. The scene is a data structure composed of elements of various types, the number of elements as well as their attributes having to satisfy some semantic constraints. Beyond this example, size-varying data structures and interdependent data elements are quite common for information processing systems, communication protocols, etc.

The production of synthetic test data for such systems may involve custom test generators, but this paper investigates a more generic solution based on a data model. The candidate approach should: (i) require no user effort other than the declarative specification of the data, (ii) accommodate rich data structures and numerical properties, (ii) provide diversity in the generated data contents and size.

We investigated the numerous existing tools for test generation. Surprisingly, we did not find any tool that could match the three objectives at the same time. In particular, the approaches using constraint solving seemed promising. They fit well with declarative models. A number of mature solvers are available off-the-shelf, including SMT (Satisfiability Modulo Theories) solvers that can handle numerical

The research presented in this paper has been partly funded by European Union's EU Framework Programme for Research and Innovation Horizon 2020 under Grant Agreement No. 812.788 (Safer Autonomous Systems). constraints. However, they fail short of our objectives for two reasons. First, the backend solvers work in a fixed universe, i.e., with a fixed set of variables and constraints. They offer little support for exploring size-varying data structures, when the number and type of contained elements is not fixed, and the creation of data instances yields an evolving set of variables and relations. Second, the solvers are deterministic and return one solution, which is (in some way) the most obvious one they find to satisfy all constraints. This is not satisfactory for test generation, as one would like to generate multiple test cases and obtain diversity in the coverage of the valid data space.

This paper presents the solution we designed to address these issues. It proposes a novel way to harness the constraint solving, which ensures diverse data contents and size. The harness dynamically updates the constraints as data instances are generated, and combines random sampling with constraints solving to enforce diversity. In particular, the generation injects random values into the queries sent to the solver.

TAF (Test Automation Framework) [START_REF]Testing Automation Framework[END_REF] prototypes this approach on top of the Z3 SMT solver [START_REF] De Moura | Z3: an efficient SMT solver[END_REF]. The user specifies a data model in an XML-based language. The tool then offers data generation, completion, and export facilities. We demonstrate the capabilities of the tool by four case studies exemplifying different types of data models: virtual crop fields for testing an agriculture robot, bitmap images with a graduated background, tree data structures of diverse sizes and heights, and a population of taxpayers in a tax management system.

The structure of the paper is as follows. Section II presents related work on test case generation. Section III gives an overview of the tool, and introduces our motivating example. Our test case description language is detailed in Section IV, then Section V presents the generation algorithms. Section VI shows the use of the tool on four case studies. We also provide some comparison results with an alternative tool. Finally, Section VII concludes.

II. RELATED WORK

We discuss related work that addresses the generation of test cases from rich input data models. Here, we do not consider approaches that derive the test data from the source code. Rather, we focus on black box approaches for systemlevel testing or when the source code is not available. The generation proceeds from data models expressed in XMLbased languages [START_REF] Banks | Snooze: Toward a stateful network protocol fuzzer[END_REF], [4], first-order languages [START_REF] Marinov | Testera: a novel framework for automated testing of java programs[END_REF], [START_REF] Dutra | SMTSampler: Efficient stimulus generation from complex SMT constraints[END_REF], formal grammars [START_REF] Purdom | A sentence generator for testing parsers[END_REF]- [START_REF] Kifetew | Generating valid grammarbased test inputs by means of genetic programming and annotated grammars[END_REF], UML [START_REF] Cantenot | Test generation with satisfiability modulo theories solvers in model-based testing[END_REF]- [START_REF] Soltana | Practical constraint solving for generating system test data[END_REF], or even general-purpose languages [START_REF] Claessen | Quickcheck: A lightweight tool for random testing of haskell programs[END_REF]- [START_REF] Poulding | Generating structured test data with specific properties using nested monte-carlo search[END_REF].

As soon as the data model involves semantic properties, the production of valid instances becomes an issue. We classify the generation approaches in three broad categories, depending on whether they rely on many successive trials, or they tune the generation process for the specific model under consideration, or they delegate the generation to constraint solvers.

A. Generate-then-filter approaches

In practice, many approaches implement a form of the generate-then-filter algorithm. It consists in producing a candidate data instance, checking it, and discarding it if it is semantically invalid. The process is repeated.

The property-based approaches popularized by QuickCheck [START_REF] Claessen | Quickcheck: A lightweight tool for random testing of haskell programs[END_REF] work according to this principle: they randomly generate inputs and discard the ones that do not fulfill the precondition of the property to check. Another example is Yagg [START_REF] Coppit | Yagg: An easy-to-use generator for structured test inputs[END_REF], a generation framework based on attribute grammars. Yagg uses the context-free part of the grammar to produce the candidate test cases, and then apply the context-sensitive checks to filter out the invalid ones.

Our framework TAF addresses generation problems where such an approach is inefficient, and yields a high rate of invalid candidate test cases.

B. Approaches that tune the generation process

The rate of invalid cases can be decreased by tuning the generation process. It requires the introduction of applicationspecific knowledge on how to build the data.

Several approaches annotate the data model with usersupplied code fragments. The commercial fuzzer Peach [4] (now integrated in DevSecOps) has an XML-based language with constructs for inserting references to external functions. This provides a means to aid in the generation of valid data at the expense of some coding effort. Similarly, in the framework of formal grammars, Maurer [START_REF] Maurer | Generating test data with enhanced context-free grammars[END_REF] attaches Action routines to the production rules. Part of the data may then be generated based on the context. The grammar annotation scheme by Kifetew et al. [START_REF] Kifetew | Generating valid grammarbased test inputs by means of genetic programming and annotated grammars[END_REF] manages a context that carries information about the data types, which proved helpful to build valid integer or float expressions. Some authors have used higher-order attribute grammars (HAGs), for which the separation between the semantic attributes and the syntactic constructs disappears. The mutation-based fuzzer in [START_REF] Pan | Efficient model-based fuzz testing using higher-order attribute grammars[END_REF] leverages this facility: the user-supplied annotations can manipulate the syntax tree of the test cases to keep the data valid after a mutation.

For weighted grammars and other stochastic models, an alternative way to improve the generation process is by tuning the probabilities of the choices. In [START_REF] Poulding | Generating structured test data with specific properties using nested monte-carlo search[END_REF], these probabilities are optimized by search-based techniques. In [START_REF] Kifetew | Generating valid grammarbased test inputs by means of genetic programming and annotated grammars[END_REF], they are learned from an existing pool of valid test cases. Note that the latter work also proposes a grammar annotation scheme (mentioned in the previous paragraph), which produces a higher number of valid data than the learned probabilities. In [START_REF] Cekan | A probabilistic context-free grammar based random test program generation[END_REF], a grammar rule can change the probability of another one, providing yet another scheme to manually adapt the choices to the context.

All these approaches require an effort from the user to customize the generator. The effort is to be done for each new application. In contrast, our framework TAF offers a generic solution that works out of the box. The user only has to specify the data structures and the desired properties. The model is kept declarative and free from programmatic annotations.

C. Approaches that use constraint solving

A solution to spare the tuning effort is to delegate the construction of valid test cases to off-the-shelf constraint solvers (as we do in TAF).

In the context of SAT solving, Alloy [START_REF] Jackson | Alloy: a language and tool for exploring software designs[END_REF], [START_REF]Automating first-order relational logic[END_REF] is worth mentioning. The core first-order language is well suited for expressing structure-rich models. The analyzer is able to create model instances, making it usable for test generation. For example, TestEra [START_REF] Marinov | Testera: a novel framework for automated testing of java programs[END_REF] is a framework for testing Java programs based on Alloy. It uses the Alloy analyzer to enumerate the set of all non-isomorphic valid inputs up to a certain size. Note that, in this case, the aim is to perform bounded exhaustive testing, which induces a focus on small data sizes. Also, since Alloy is connected with SAT-based analysis, the approach does not support numerical constraints over real variables.

UMLtoCSP [START_REF] Cabot | On the verification of uml/ocl class diagrams using constraint programming[END_REF] uses constraint logic programming (CLP) to analyze UML models including constraints in OCL (Object Constraint Language [START_REF]Object Constraint Language[END_REF]). It supports numerical constraints. Like Alloy, the framework is able to create model instances with a bounded size. The authors recommend that the size be kept small. Dewey et al. [START_REF] Dewey | Automated data structure generation: Refuting common wisdom[END_REF] demonstrate the efficiency of CLP to generate data structures, but observe that CLP specifications may become obscure. They recommend the design of small frontend languages with loops and variable assignments, for which an efficient translation to CLP would be investigated.

Other approaches use SMT solving to address UML models with numerical constraints. Cantenot et al. [START_REF] Cantenot | Test generation with satisfiability modulo theories solvers in model-based testing[END_REF] generate tests in a fixed universe: the user has to predefine the desired class instances in an object model. The PLEDGE framework [START_REF] Soltana | Practical constraint solving for generating system test data[END_REF] directly generates the class instances and their contents from the UML class diagram. It addresses the lack of scalability of constraint solvers by hybridizing metaheuristic search and SMT. The authors show that this strategy is able to create larger model instances than Alloy and UMLtoCSP. The hybrid strategy also outperforms the pure search-based one using the metaheuristic only.

Among all generation approaches, PLEDGE is the closest one to ours since TAF hybridizes random sampling and SMT. The hybridization algorithms are however different. PLEDGE has randomness in the creation of class instances but does not attempt to ensure diversity of their contents. It takes the solution returned by the SMT solver. TAF has randomness in both the instantiation process and the production of data contents, with the aim of maximizing diversity. It forces the solver to produce different solutions.

To the best of our knowledge, this contribution is novel. As noted by Dutra et al. [START_REF] Dutra | SMTSampler: Efficient stimulus generation from complex SMT constraints[END_REF], the generation of multiple diverse solutions has been little studied for SMT constraints. The authors have addressed the problem for theories of bit vectors and bit-vector arrays used in hardware verification. Their approach relies on combinations of bitflips to explore the diverse solutions in a fixed universe. With TAF, we propose another approach targeted at size-varying data structures with numerical constraints. In addition to providing diversity, the approach is also efficient for creating data instances of a realistic size, as will show the evaluation against PLEDGE in Section VI.

III. FRAMEWORK OVERVIEW

In order to illustrate the facilities offered by the TAF framework, let us first provide a motivating example inspired by [START_REF] Robert | The virtual lands of oz: testing an agribot in simulation[END_REF]. It concerns the simulation-based testing of an agriculture robot, an autonomous weeder that operates in fields of vegetables. A test case for this system consists of a weeding mission in a virtual crop field (see Figure 1). A crop field is composed of an arbitrary number of crop rows. The robot has to navigate along them. When it arrives at the end of a row, it makes a U-turn to weed the next one. We assume a monoculture environment, hence the field contains a single type of vegetables, which can be cabbages or leeks. One of the mission parameters, is first track outer, indicates whether or not the robot starts at the external side of the field.

The generation of such virtual test cases can proceed in two steps. The first step generates abstract cases from a data model, while the second one produces the concrete test artifacts to be fed into the test platform. By having these two separate steps, it is possible to keep the modeling focused on high-level data elements, without being overwhelmed by the complexity of concrete details or formatting issues. For example, an abstract test case of the autonomous weeder only specifies a number of crop rows and a vegetable type. It is then concretized by creating a scene description file in a format understood by the simulator, e.g., in terms of a list of vegetable meshes to be placed at designated coordinates.

The TAF framework supports this test generation process (see Figure 2). It provides an XML-based language to specify test templates, i.e., structured models of the data composing an abstract test case. The data factory generates abstract test cases according to the template. To facilitate the final concretization step, TAF also creates a code skeleton, in which export functions are attached to the various data elements. These export functions are initially empty, the user should add the custom export code in order to convert the produced test cases (in XML) into the required file format.

A salient feature of TAF is its possibility to accommodate semantic constraints. In the motivating example, the various data elements cannot take independent values. If the crop field has only one row, then the weeding mission necessarily starts at an external side of the field. Consecutive rows must have nearly the same length, say by +/-10%. We furthermore require that the lengths of the first and last row are also close by +/-10%. Such constraints can be expressed into the template and make the test generation challenging. On the one hand, a random generate-then-filter strategy would be inefficient. Suppose we have tens of rows: it would take a huge number of trials before obtaining a set of consistent row lengths. On the other hand, the use of a constraint solver would return a single solution, possibly the simplest one, like all rows having the same length, and this length is the minimal one allowed for a row. To avoid both pitfalls, the data factory combines random generation with constraint solving, allowing for the efficient production of diverse test cases that satisfy the constraints. The framework offers tunable random generation functions for each basic type of data, and uses the SMT solver Z3 for the satisfaction of constraints.

Another convenient facility is the possibility for the user to supply a partially instantiated test case. This input file is optional. It allows for setting the values of any subset of the basic data elements. For example, the user can request a crop field with a maximal number of rows, or request the combination of this number of rows with a cabbage type of vegetables. The data factory will generate the missing data elements to produce a complete and valid test case. This test case completion facility gives great flexibility to explore subsets of the input space or cover extreme cases. Moreover, the choice of XML-based file formats is intended to facilitate the implementation of test strategies on top of TAF. Both the template and partial instance files can be manipulated to request specific values, add or remove constraints, or change the default generation function for a given data element.

The following sections provide more details about the data factory: the XML-based description language it accepts, and its generation algorithm.

IV. TEST CASE DESCRIPTION LANGUAGE

This section describes the language used in the XML files Template and Partial instance from Figure 2. It features a markup-based declaration of the data elements and embeds constraints. The language was designed with the ontology presented in Figure 3. The .dtd and the BNF are provided on the Git repository [START_REF]Testing Automation Framework[END_REF]. In order to illustrate the main concepts, we will use the template file in Figure 4 that gives the data model of our motivating example. We first present how the data structure is declared, from composite elements to parameters having a basic type. We also explain how the parameters are attached a default generator. Then, we introduce the expression of constraints between parameters. Finally, we present how to assign values to parameters in a partially instantiated test case.

A. Data structure

As shown in Figure 3, a test case template involves four different types of XML elements: Root, N ode, P arameter, and Constraint. Every element must have a "name" attribute. Elements are nested to form a tree starting from the root. The root and nodes are composite data structures with child The root is unique and mandatory, but both the parameters and nodes have a "nb instances" (-number of instances-) meta-attribute that allows for multiplicity. If multiplicity is not explicitly declared in the template, the number of instances is supposed to be 1.

The template in Figure 4 illustrates these structural concepts. The test case root (Line 3) is composed of a node "field" (L4) and a node "mission" (L19). The node "field" has one instance (L4), and contains a parameter "vegetable" (L5) that can take the values "leek" or "cabbage". A field is composed of multiple rows. In the declaration of the "row" node (L6), the allowed number of instances is specified by its min and max values (1 and 40). Each row element contains a parameter "length" (L7), with min and max values as well (10 and 100). As a general rule, all numerical parameters (real or integer) must have an explicit definition range, and all string parameters must have a set of candidate values.

B. Default generators

TAF attaches a default generator to each parameter in the structure. Its aim is to produce diverse values from the parameter type. If nothing is specified in the template, uniform sampling over all possible values is used as the default. For instance, in Figure 4, L7, the parameter "length" will be determined in the range [10, 100] with a uniform sampling. But the user also has the possibility to select other default generators. This is done when the parameter is declared, by 1 <? xml v e r s i o n =" 1 . 0 " ?> 2 3 <r o o t name=" t e s t c a s e "> 4 <node name=" f i e l d " n b i n s t a n c e s =" 1 "> 5 <p a r a m e t e r name=" v e g e t a b l e " t y p e =" s t r i n g " v a l u e s =" c a b b a g e ; l e e k " w e i g h t s =" 5 ; 7 " /> 6 <node name=" row " min=" 1 " max=" 40 "> 7 <p a r a m e t e r name=" l e n g t h " t y p e =" r e a l " min=" 1 0 . 0 " max=" 1 0 0 . 0 " /> 8 <c o n s t r a i n t name=" i n t e r v a l " t y p e s =" f o r a l l " using dedicated attributes (e.g., the weights attribute appearing in the note on the Parameter class of Figure 3).

The set of available generators depends on the data type. Boolean and string parameters can have weighted choices. For instance, in Figure 4, L5, the declaration of the vegetable parameter introduces a biased sampling of values, where the choice "leek" (of weight 7) is more likely than "cabbage" (of weight 5). It is required to have as many weights as values. For integer or real parameters, there are two alternatives to uniform sampling over their definition range. The user can assign weights to subranges of values, or request sampling according to a normal distribution with some mean and variance. The parser of the template will check that the requested generator is compatible with the parameter type.

C. Constraints

Constraints consist of expressions that specify semantic properties in a descriptive way. The language syntax lets the user specify a list of one or more expressions separated by a semi-colon (Figure 4,L8,L13,L21).

The expressions may involve logical (not, and, or, implies), arithmetic (+, -, *, /), and relational (==, !=, <, <=, >, >=) operators. The concrete syntax ensures that the file can be parsed by any regular XML parser. In particular, the relational operators are written as EQ, DIF, INF, INFEQ, SUP, SUPEQ to avoid issues with characters < and >. For easier interfacing with Z3, the structure of the expressions follows the Z3 syntax (e.g., for expressions with logical operators as in L22 of Figure 4, the operator is first, and the operands come after).

The variables can be any parameter of the test case structure. They are referenced by an access path relative to the location where the constraint is declared. The path syntax uses the windows file system notation with separators "\", to avoid ambiguity with the division symbol. Moreover, "." and ".." refer to the current node and the parent node. Paths can include indices to refer to the instances of nodes. In Figure 4,L9, row[i]\length refers to the length parameter of the ith row.

Our language also provides quantification over finite structures. For instance, the constraint named "interval" (L8-12) has a universal quantification (f orall) over all row instances. It has a single quantified variable (i in L11) taking the value of row indices (L12). The language also provides existential (exist) quantification (not used in our motivating example). Note that it is possible to use nested quantifiers of universal and existential types. An example is given in the tax payer template on the git repository in the "templates" directory [START_REF]Testing Automation Framework[END_REF].

D. Partially instantiated test cases

An important feature is the possibility to feed partially instantiated test cases into TAF. If possible, the test case is completed according to the template model.

The partial test case file has a structured description of a subset of element instances. Some parameters are forced to a desired value. They appear with their name and a value attribute. Figure 5 shows an example where the length of the third row (with row numbering starting at 0) is forced to 40. Accordingly, TAF will consider that the template is augmented with two constraints: that the number of the row instances is > 2, and that the third row has a specific length. If the desired length is out-of-range, the parsing will detect it and abort the generation. For the convenience of the user, predefined keywords facilitate the assignment of some values of interest (e.g., "max" for the maximal value of a numerical parameter, "first" for the first possible value of a string parameter).

Note that the user who creates a partially instantiated test case is not necessarily human. A program may produce the partial instances according to some test strategy, and rely on TAF to complete them. The generation adopts a top-down, layered approach that follows the structure of the XML template. The parsing of the template file builds an initial tree. It contains placeholders for the elements defined in the template according to the containment hierarchy. As the generation proceeds, the tree is updated to insert the created element instances, and assign values to their parameters.

Figure 6 illustrates the top-down approach on our running example. The root test case node is at depth 0 of the tree, its mission and crop field children at depth 1, and so on. All elements at a given depth d are generated at the same step, after the elements at depth d -1 and before the ones at d + 1. The number of instances to create at each layer is a parameter <element name>.nb instances that belongs to the immediately upper layer, the one of the parent node. It guarantees that the number of instances is always defined before building the related objects. If the template lets this parameter implicit, it takes the default value one. In the running example, the number of mission and crop field instances is set to 1, hence we build one instance of each of them. In contrast, the template specifies any number of rows in a [min, max] range: a number will be chosen at depth 1, when the parent crop field node is processed.

Each constraint defined in the template is also assigned a depth: it takes the maximal depth of all the parameters that it refers to. In the running example, there is a constraint between row.nb instances and is f irst track outer, respectively of depth 1 and 2. According to the previous rule, this is a depth 2 constraint. It means that row.nb instances will be generated first, and later the generation will try to find a value of is f irst track outer that satisfies the constraint. This approach can obviously lead us to a dead-end as the parameters generated from the previous layers may produce unsolvable constraints. Hence the generation uses backtracking.

Algorithm 1 shows the layered generation with backtracking. The main loop (Lines 6-18) iterates until either the generation is complete or the maximal budget for backtracking is reached (M AX B). This budget is configured by the user. At each iteration, function generate depth() attempts the generation of the elements at the current depth. If it succeeds, the generation continues at the next depth (Line 8). If it fails, the choices made at the current depth are undone, and the generation goes back to the previous layer (Lines [START_REF] Xu | A toolkit for generating sentences from context-free grammars[END_REF][START_REF] Pan | Efficient model-based fuzz testing using higher-order attribute grammars[END_REF][START_REF] Cekan | A probabilistic context-free grammar based random test program generation[END_REF]. After exiting the loop, the tool reports on its failure (Line 20) or success (Line 23). In the latter case, an XML version of the test case is created for archiving purposes.

Algorithm 1 main

Require: path 1: tree ← parse template(path) 2: create export code skeleton f ile(tree) 3: preprocess(tree) 4: counter ← 0 5: depth ← 0 6: while counter < M AX B AN D depth ≤ tree.max depth() do 7:

if generate depth(tree, depth) then Algorithm 2 describes how a given layer is generated. First, it extracts the parameters p and the constraints c of the current depth. Then, there is a triage between dependent and independent parameters, according to whether they are involved in any of the constraints (Lines 3-4). Independent parameters are simply generated using the default random generators (Lines 5-7). If there is no constraint, the generation of the layer is done (Lines 8-10). Otherwise, a problem object is created with the dependent parameters and the constraints (Line 12). If the problem fails the satisfiability check in Z3, the layer is not generated and the function returns F alse (Line 14). This will cause backtracking in the main algorithm. If the problem is satisfiable, the dependent parameters are processed. Their generation mixes constraint solving and randomness in order to ensure diversity in the solutions. Such a process is described in Algorithm 3 to be presented shortly. Finally, before returning success, the algorithm prepares the next layer according to the newly generated values of <element name>.nb instances parameters (Lines 9 or 17): the appropriate number of element nodes is created and inserted into the tree.

Algorithm 2 generate depth

Require: tree, depth Algorithm 3 takes a problem object as input and solves it with diversity. We know that the problem is satisfiable (from the previous algorithm), but want to force the solver to produce a different solution than the one it would normally return. For this, the principle is to assign random values to as many parameters as possible before solving the constraints. In the inner loop at Lines 5-12, we keep adding new constraints p = v until the problem becomes unsatisfiable. It yields a new solvable version of the problem where some parameters take random values. The process is repeated multiple times according to a diversity budget M AX D (outer loop starting at Line 3). At each iteration, we keep track of the best problem in terms of the number of randomly chosen parameters (Line 14). Lastly, the best problem is solved, and all the parameters are updated accordingly (Lines 17-18). The TAF test case factory implements the above algorithms in Python. For simplification purposes, the presentation has focused on the template-based generation, omitting the test completion facility. In practice, the submission of a partially instantiated test case only impacts the preprocessing of the tree structure in Algorithm 1. It adds new constraints to force the desired parameter values, then the layered generation proceeds as described. The user may also request the generation of N test cases, rather than just one. Both the backtracking and diversity budgets (M AX B and M AX D) can be easily configured, should the default setting be insufficient for the target generation problem.

Algorithm 3 solve with diversity

VI. CASE STUDIES

In this section we demonstrate the use of TAF on four case studies coming from different application domains. We assess its performance and the data diversity it supplies. P erf ormance is measured by the execution time needed to generate 100 valid test cases from each of the four models. The generation is repeated 10 times, and the median, min, max times are reported. Data diversity is analyzed in terms of the coverage of the data space. For each case study, we manually derive a set of cases to be covered, considering both the raw definition domains of the parameters (e.g., a range decomposed into subranges to be covered) and some application-specific aspects related to the semantics of the data. We monitor the accumulated percentage of covered cases while the generation proceeds and identify the missing cases at the end.

TAF is also compared with two alternative strategies: generate-then-filter and PLEDGE [START_REF] Soltana | Practical constraint solving for generating system test data[END_REF]. From our analysis of related work (see Section II), PLEDGE emerges regarding its ability to handle size-varying data structures and numerical constraints. Moreover, the hybridization of metaheuristic search and SMT allows it to create larger data instances than the other solver-based approaches.

A. Data models of the four case studies

We used our XML-based language to model the following four case studies. The corresponding template files are available on the git [START_REF]Testing Automation Framework[END_REF].

Oz: This is the industrial case study of an agriculture robot [START_REF] Robert | The virtual lands of oz: testing an agribot in simulation[END_REF], from which our motivating example is extracted. The complete model has 7 composite elements, 15 parameters, and 5 constraints. The structure is presented as a class diagram in Figure 7. Compared to the smaller motivating example, the few additional constraints are on the number of instances of the new elements. For example, the number of row spacing values (element inner track width) must be consistent with the number of rows. The motivating example reproduces the most challenging constraints in this case study (the ones on the row lengths) and already gives a good idea of what the complete Oz model is like in TAF.

Bitmap: The aim is to create a gradient image in the bitmap format. The darkest pixel is at the bottom left corner and the lightest one at the upper right (see Figure 8). The content of the image is structured as a set of pixel rows, where each pixel contains a grayscale value. A padding parameter determines the number of bytes to add after each row, so that the total number of bytes is a multiple of 4. The model is concise, having two composite elements, 2 parameters, and 4 constraints. Formatting issues are delegated to the export code, e.g., to produce the image header given the size of the data and a predefined encoding option. Note that the generation of the image content may be challenging for constraint solving, as each pixel instance depends on its upper and right neighbors. The value of the row padding is specified by a constraint involving modulo operations.

Tree: We study the generation of tree structures of diverse sizes and heights. TAF does not allow recursive definitions, hence it is not possible to model a tree as a composite element that would contain child trees. Rather, we have to consider a flattened set of tree nodes, and introduce the tree properties by quantification over this set. In our model, a node has two parameters: a f ather (containing the id of the parent node) and a depth. Figure 9 shows the encoding (XML in a tree structure) of a tree instance of size 4 and height 2. Except for node[0], which is the tree root, the other nodes may have an arbitrary position in the tree, as determined by the value of their parameters. We simply require that a node has the depth of its father +1, that no node has a depth greater that the global tree height, and that at least one node has a depth equal to the global height. These constraints remain abstract, not being prescriptive in how to generate the father relations consistently with the height. This may be challenging for the solver.

TaxPayer: This case study is the running example of the PLEDGE paper [START_REF] Soltana | Practical constraint solving for generating system test data[END_REF]. Its UML model is shown in Figures 10 and11. It describes the data for an income tax management application. In this model, "Tax payer" is a "Physical person" that can support "Child" and earns 1 or more "Income". There are five OCL constraints (C1 to C5). For instance, C3 states that Taxpayers are not resident if they earn local incomes but do not have any address is Luxembourg. None of the OCL constraints is difficult to express in TAF. More difficult are object paradigms such as inheritance (e.g., "Child" Fig. 9. A tree instance: XML encoding and graphical export Fig. 10. UML of the tax payer case study inherits from "Physical person") and bidirectional association (a "Physical person" resides at an "Address"). Indeed, TAF only supports composition relations. We modeled the inheritance relation by "flattening" the inheritance (redistribute information in sub-classes). Our model is thus less concise than the original one, as some declarations and constraints are duplicated. Regarding the associations, as they were oneto many relations we were able to encode them as a unidirectional composition. A more generic solution would add parameters and encode symmetric indices in associated nodes. The TaxPayer model in TAF involves 9 composite elements, 12 parameters and 7 constraints.

The four case studies illustrate various types of data (from a matrix of pixels to Person elements), of structural relations (from hierarchical containers to other architectural relations), and of constraints (from simple logical constraints to more complex ones with nested quantification and arithmetic expressions). In addition to modeling them in the XML-based language, we developed external programs to check the valid-1 c o n t e x t P h y s i c a l p e r s o n i n v C1 : 2 s e l f . b i r t h y e a r >=1920 and s e l f . b i r t h y e a r <2020 3 4 c o n t e x t P h y s i c a l p e r s o n i n v C2 : 5 i f ( s e l f . d i s a b i l i t y t y p e = D i s a b i l i t y : : None ) 6

t h e n ( s e l f . d i s a b i l i t y r a t e = 0 ) 7 e l s e ( s e l f . d i s a b i l i t y r a t e > 0 and 8 s e l f . d i s a b i l i t y r a t e <= 1 . 0 ) e n d i f ity of the generated data samples in each case. The checkers allowed us to confirm that the models encoded the intended properties and that the generation process was not flawed.

B. Performance

The performance of TAF heavily relies on the performance of the used solver. On the positive side, the solver processes only parts of the data. The layered approach decomposes the generation problem into subproblems. Furthermore, in a layer, only the dependent parameters are to be solved. On the negative side, the search for diversity involves multiple calls to the solver, which may be very costly. A question is whether the approach is practical with a state-of-the-art solver like Z3.

Table I shows the generation time of 100 test cases for each case study. The experiments are done on a 2017 Mac-BookPro14,2 dual-core (3.5 GHz Intel Core i7, RAM 16 GB). The backtracking and diversity budgets are both set to 10. The size of the generated data may vary in each test case and has the upper bound indicated in the second column of the table. For example, for Oz, the number of crop rows has its definition domain in 1..100. We stop a run if it is longer than two hours.

Tree is the most challenging case study for the solver. It failed to produce the 100 test cases within two hours when the tree size is up to 100 nodes. In the layered generation approach, the global height is decided first, and then the local decisions on node parameters have to comply with it. From our analysis, the long solving times are when the randomly injected father and depth values yield an unsat problem, but the solver does not detect this and keeps trying possibilities. By taking a max size of 50 nodes, the generation is feasible in less than 50 minutes. The easiest case studies are Oz and TaxPayer, for which 100 test cases are produced with a median time of respectively 17.62 and 133.9 seconds. For Oz, the data size is realistic since the crop fields in which the real robot operates usually have less than 100 rows. As regards TaxPayer, the loose coupling between person elements makes it possible For comparison purposes, we considered the performance of two baseline strategies. The first one is generate-then-filter. We removed the semantic constraints from the data models, and used the external validity checker to filter the data generated by TAF. A first 2-hours run failed to produce any valid data except in the case of TaxPayer, which produced 46 test cases (out of 33,290 trials). Additional runs for TaxPayer never managed to obtain 100 valid cases in two hours (the best run obtained 55 cases). Moreover, all valid cases merely consisted of data instances with a single taxpayer. The generate-thenfilter strategy is thus highly inefficient for our case studies. The second baseline is PLEDGE [START_REF] Soltana | Practical constraint solving for generating system test data[END_REF] which represents a more complex strategy similar to ours. PLEDGE uses the same backend solver as TAF (i.e., Z3) but harnesses it in a different way. The generation strategy combines metaheuristic search and SMT with the aim to use each technique where it is the most efficient. It distributes tasks to one technique or the other. In contrast, TAF has an intertwined usage of random sampling and SMT. We modeled Oz and TaxPayer in UML to supply them to PLEDGE. Table II shows the corresponding generation times. They were an order of magnitude longer than with TAF, even when the size of the data was reduced (TaxPayer).

To conclude, the Z3 solver is efficient enough for the proposed solve-with-diversity approach to be practical. Despite the multiple calls to the solver, the time for generating samples of medium-sized constrained data may be workable. The strategy allowed us to address four case studies for which a simpler generate-then-filter strategy fails. The comparison with the state-of-art tool PLEDGE shows that TAF can be very competitive in terms of performance.

C. Diversity of the test cases

We analyze the data space coverage provided by TAF. In the models, each numerical parameter or number of instances has a min-max definition range: we systematically split it into three subranges to cover, yielding low, medium and high cases. We count a case as covered if any instance of the parameter has a value in the subrange. When a parameter has an enumerated type, we require the coverage of each value individually. We then add cases derived from the constraints and other semantic concerns, that address the relations between parameters. These cases are presented below.

Oz: The relative length of consecutive rows has to cover the +/-10% range split into low, medium and high cases. The same is required for the constraint between extremal rows, but we count coverage only if there are strictly more than two rows (i.e., if the first and last rows are not consecutive). We further require that the first row takes diverse values in its definition range.

Bitmap: The difference between a pixel value and the one of its upper (resp. right) neighbor has to range over 0..255, yielding low, medium and high cases. We also analyze the variation in an entire row or column of pixels, measuring the difference between the first and last pixel. Finally, we require that the darkest (resp. lightest) pixels takes diverse values in the images.

Tree: We require diversity in the ratio of the height to the number of nodes, to span the cases from a shallow tree with all nodes under the root, to a linear tree with the maximum possible height. We also require diversity in the balancedness of the trees. We retain three alternative definitions of balancedness (e.g., see [START_REF] Cha | On complete and size balanced k-ary tree integer sequences[END_REF]), each yielding low, medium and high cases to cover. Given a height h, we measure Leaf-balancedness by the rate of leaves that are either at depth h or h -1. The height-balancedness metric is the rate of internal nodes that introduce subtrees of similar heights (+/-1), and similarly for size-balancedness. To exclude degenerate covering cases, we only report balancedness for trees having at least 5 nodes, and a height strictly greater than 2.

TaxPayer: We consider three cases for the addresses of a taxpayer: the taxpayer has no address in Luxembourg, at least one address in Luxembourg and another one elsewhere, or all the addresses are in Luxembourg. From constraint C4, we also extract cases combining the various types of local incomes (pension, employment, other) with no address in Luxembourg.

Table III reports the total number of cases to cover for each case study, as well as the coverage results. The complete list of cases to cover is available in our repository [START_REF]Testing Automation Framework[END_REF]. For example, there are 51 cases to cover for Oz. From Table III, 100% of them are covered by each of the 10 test sets. The full coverage is reached after a median number of 16.5 data have been generated (8 in the earliest case, 49 in the latest one). As can be seen, TAF succeeds in supplying a high coverage for all case studies. For Tree, we consider that this was challenging, because the measured properties of the tree structure only indirectly emerge from the instantiation of parameters. There is no notion of balancedness in the model, and still TAF managed to generate trees with diverse balancedness metrics. The only case study for which full coverage is not reached is Bitmap. The missing cases concern high values for the darkest pixel in an image (hence yielding a nearly completely white image) , and similarly low values for the lightest pixel (nearly In comparison, PLEDGE does not provide data diversity. Using PLEDGE, the ten test sets supply a coverage of respectively 52% for Oz and 51% for TaxPayer. The generation manages well a varying number of instances in class architectures, but the data content is the simplest solution returned by the solver. For example, for Oz, the generated fields have a varying number of crop rows, but all rows have an identical length of 10m (the minimum of the interval), the noise in the alignment in crop plants is zero, and so on. For TaxPayer as well, the population of taxpayers lacks diversity, e.g., all taxpayers are born in 1920 (the minimal birth date), their address is never in BE or DE. The authors acknowledge the lack of diversity [START_REF] Soltana | Practical constraint solving for generating system test data[END_REF]: they argue that diversity can be effectively enforced by dynamically updating the OCL constraints with new inequalities.

However, this is not as satisfactory as built-in diversity. The user has to very explicitly manage the generation of each numerical parameter, and may still get limited diversity.

For instance, consider how to enforce diverse row lengths for Oz. By default, all rows have the minimal length (10m). We may enforce the first and last rows to be different: the generated lengths are then 10m, ..., 10m, 10.5m. If we further require all rows to be different, the generation time is longer and the different values are still between 10m and 10.5m. We would need additional constraints to cover other values (up to 100m) and other variation patterns between consecutive rows (up to +/-10%). This becomes heavy. The constraints grow more complex than mere inequalities. In contrast, TAF natively provides diverse values and variation patterns.

To conclude, TAF was successful in generating constrained data that provide a high coverage of the data space. To the best of our knowledge, there is no comparable tool that would offer a similar facility based on SMT solving.

VII. CONCLUSION

The paper has presented TAF, a tool that automatically generates test cases from high-level XML-based data models. This tool introduces a novel way to generate diverse instances of data elements in the size-varying data structures. The core feature of TAF is the function "solve with diversity", that mixes constraint solving and random sampling. It assigns random values to as many parameters as possible before solving the constraints, in order to force diversity in the obtained solutions. The function is part of a main algorithm that uses a layered generation approach with backtracking. The top-down decomposition into layers ensures that the data elements are generated only after their number of instances is decided.

TAF has been applied to four case studies. It successfully generated valid and diverse test cases for all of them. The comparison with an alternative tool using the same backend solver showed that the generation time is competitive, while allowing for a much better coverage of the data space.

Regarding improvements of TAF, three main aspects may be envision. First, a connection with de facto standard languages like UML, would improve the usability of our tool. A second point is the native inclusion in TAF of some object-oriented concepts such as inheritance, bidirectional or recursive associations. Particularly, implementing (bounded) recursive associations would allow a more direct expression of some structural properties, which are currently specified by means of quantified predicates rather than by recursive definitions. The third improvement is to interface TAF with a generic language for solver facilities. For instance, an interfacing with SMT-LIB would allow TAF to use several solvers as an alternative to Z3.

Finally, TAF can be used as a test generation tool by itself, but we plan to integrate it in a larger test automation framework. Our future work will consider the integration into a framework that leverages the test completion facility of TAF. We envision an approach where test objectives are produced under the form of partially instantiated test cases, completed by TAF, submitted to the system under test, and then analyzed to produce new objectives. This approach will be experimented in our on-going work on testing autonomous robots in complex 3D environments.

Fig. 1 .Fig. 2 .

 12 Fig. 1. A virtual test case for the autonomous weeder

Fig. 3 .

 3 Fig. 3. TAF DSL ontology with a UML class diagram

Fig. 4 .

 4 Fig. 4. Template file example for the autonomous weeder simulation

<Fig. 5 .

 5 Fig. 5. Partially instantiated test case

Fig. 7 .

 7 Fig. 7. Oz complete case study structure with a UML class diagram

Fig. 11 .

 11 Fig. 11. OCL code of the tax payer case study

  1: p ← extract parameters(tree, depth) 2: c ← extract constraints(tree, depth) 3: dependent p ← f ilter dp(p, c) 4: independent p ← f ilter indp(p, c) 5: for p in independent p do 6:

		p .def ault generate()
	7: end for
	8: if c is empty then
	9:	create next depth instances(p)
	10:	return T rue
	11: end if
	12: problem ← init problem(dependent p, c)
	13: if N OT problem.check sat() then
	14:	return F alse
	15: else
	16:	solve with diversity(problem)
	17:	create next depth instances(p)
	18:	return T rue
	19: end if

TABLE I GENERATION

 I TIME USING TAF (10 RUNS, 100 TEST CASES PER RUN)

	Case study	Max data size Tmin	Tmax	Tmedian
	Oz	100 rows	16.36 s	18.79 s	17.62 s
	Bitmap	100x100 px	636.7 s	1554 s	746.6 s
	Tree	100 nodes	>2 h	>2 h	>2 h
		50 nodes	1961 s	2995 s	2664 s
	TaxPayer	100 taxp.	123.9 s	161.9 s	133.9 s
			TABLE II
	GENERATION TIME USING PLEDGE (10 RUNS, 100 TEST CASES PER RUN)
	Case study	Max data size Tmin	Tmax	Tmedian
	Oz	100 rows	1073 s	1327 s	1108 s
	Tax payer	100 taxp	>2 h	>2 h	>2 h
		50 taxp	1640 s	2651 s	1804 s
	to obtain a large population by generating multiple smaller
	populations and merging them together.


Julie Marteau
email: julie.marteau@utc.fr

Karine Anselme

Laurent Pieuchot

Pierre-François Chauvy

Maxence Bigerelle

Topography characterization of sinusoidal surfaces obtained with electrochemical machining

Keywords: sinusoidal, topography, functionality

The study and understanding of functionality and its link with surface topography requires surfaces that enable us to decouple the examined effect. The sinusoidal function offers an easy solution for the decoupling of amplitude and frequency. However, the corresponding surfaces would require very good characteristics: shape regularity, low waviness and low microroughness. This study thoroughly characterized sinusoidal surface (egg-box shapes) having periods ranging from 30 µm to 300 µm and peak-to-valley amplitudes comprised between 3 and 30 µm. The microroughness of the examined surfaces was quantified with the arithmetic mean deviation Sa and was found to be around 1 nm for most examined surfaces. The waviness of the surfaces, which was also quantified with Sa, was lower than 0.15 µm for all the surfaces. The relative error computed for the period of the sinusoidal surfaces was lower than 1.3%. Finally, the shape regularity was assessed by comparing the measurements to a mathematical function and the computed average residues were smaller than 0.8 µm. These characteristics highlighted the very good noise-to-signal ratio of the produced surfaces, which can be used in very different fields (biology, mechanics, optics…) to examine topography effect on functionality (cell adhesion, brightness…).

Introduction

There is currently a growing interest in surface texturing for the improvement of surface functionality. However, the improvement of functionality requires a good understanding of the link between morphology and functionality. It is currently difficult to dissociate the effects of amplitude, frequency and anisotropy on functionality. Tackling this issue requires finding the appropriate surface shape covering classic surface data (i.e. amplitude and frequency ranges of commonly examined phenomena). In our opinion, the best shape to decouple the effects of amplitude and frequency is the sinusoidal function. The sinusoidal function offers an easy modelling of topography using only two independent parameters (amplitude and frequency). It can be seen as an elementary surface having "no frequency artefact" thus offering a perfect decomposition into Fourier series. Such qualities facilitate parameter identification in the search for analytical solutions or model fitting. Furthermore, the possibility of having a sinusoidal shape in one direction (corrugated surface) or in two directions (egg-box like surfaces) with fixed amplitude and frequency is of interest for the examination of anisotropy effects.

However, the sinusoidal shape remains very difficult to achieve: the slightest defect will introduce artefacts during the topographical analysis. Several processes can be identified in the literature for the building of sinusoidal surfaces. Song et al. [START_REF] Song | Sinusoidal wavy surfaces for curvature-guided migration of T lymphocytes[END_REF] used X-ray lithography on polymers to create corrugated surfaces for the study of the migration of cells. Surface winkling of polymers is often chosen to create corrugated surfaces in polymers: Skedung et al. [START_REF] Skedung | Feeling Small: Exploring the Tactile Perception Limits[END_REF] used this process to examine the tactile perception of textured surfaces while Bukowsky et al. [START_REF] Bukowsky | Slip-stick wetting and large contact angle hysteresis on wrinkled surfaces[END_REF] applied it for the investigation of wettability. Similarly, Yang et al. [START_REF] Yang | Transfer printing enabled soft composite films for tunable surface topography[END_REF] used transfer printing to obtain soft composite films exhibiting corrugation to experimentally validate the mechanics of tension-induced corrugation. Antos et al. [START_REF] Antos | Spectroscopic ellipsometry on sinusoidal surface-relief gratings[END_REF] proposed to use polymer grating to produce twodimensional sinusoidal surfaces and examined the quality of the sinusoidal shape with spectroscopic ellipsometry. Lu et al. [START_REF] Lu | Diamond machining of sinusoidal grid surface using fast tool servo system for fabrication of hydrophobic surface[END_REF] produced sinusoidal grid surfaces by diamondmachining copper roller and then performed a UV-molding technique to replicate the topography on a plane surface. Chen et al. [START_REF] Chen | Large-area profile measurement of sinusoidal freeform surfaces using a new prototype scanning tunneling microscopy[END_REF] used three-dimensional surface produced with diamond machining to investigate the characteristics of a specially developed tunnelling microscope. Recently, Temmler et al. [START_REF] Temmler | Numerical and experimental investigation on formation of surface structures in laser remelting for additive-manufactured Inconel 718[END_REF] examined surface structuring by laser remelting using finite element modelling and experimentation. They obtained local topographies having sinusoidal shapes. These few examples highlight the interest in sinusoidal surfaces in different fields: biology (cell migration [START_REF] Song | Sinusoidal wavy surfaces for curvature-guided migration of T lymphocytes[END_REF][START_REF] Rougerie | Topographical curvature is sufficient to control epithelium elongation[END_REF][START_REF] Fedele | Azobenzene-based sinusoidal surface topography drives focal adhesion confinement and guides collective migration of epithelial cells[END_REF], tactile perception [START_REF] Skedung | Feeling Small: Exploring the Tactile Perception Limits[END_REF]), mechanics (wettability [START_REF] Bukowsky | Slip-stick wetting and large contact angle hysteresis on wrinkled surfaces[END_REF][START_REF] Lu | Diamond machining of sinusoidal grid surface using fast tool servo system for fabrication of hydrophobic surface[END_REF], metrology [START_REF] Chen | Large-area profile measurement of sinusoidal freeform surfaces using a new prototype scanning tunneling microscopy[END_REF][START_REF] Leach | Metrological characteristics for the calibration of surface topography measuring instruments: A review[END_REF], adhesion [START_REF] Hu | Adhesion of a micro-/nano-beam/plate to a sinusoidal/grooved surface[END_REF]). Numerous numerical studies are also based on the examination of sinusoidal surfaces. Xie et al. [START_REF] Xie | Calculation of wear on a corrugated rail using a threedimensional contact model[END_REF] investigated rail head wear. Peng et al. [START_REF] Peng | Peeling behavior of a thin-film on a corrugated surface[END_REF] studied peeling behaviour while Declercq et al. [START_REF] Declercq | Diffraction of homogeneous and inhomogeneous plane waves on a doubly corrugated liquid/solid interface[END_REF] used sinusoidal surfaces to examine the diffraction of sound. Thenard et al. [START_REF] Thenard | A Cellular Potts energy-based approach to analyse the influence of the surface topography on single cell motility[END_REF] used three-dimensional modelling to examine the influence of surface topography on cell motility: sinusoidal parallel grooves were among the tested topographies. Recently, we manufactured three-dimensional surfaces having very smooth surface and shape accuracy to examine the effect of curvature on cell migration [START_REF] Pieuchot | Curvotaxis directs cell migration through cell-scale curvature landscapes[END_REF]. This paper aims at thoroughly charactering the topography of these surfaces. Then, these surfaces are compared to the surfaces described in the literature and their applications on the study of surface functionality are discussed.

Materials and Methods

Specimens

The discussed sinusoidal surfaces were created using a two-step process, illustrated in Figure 1. First, preforms were prepared using mask electrochemical micromachining [START_REF] Landolt | Electrochemical micromachining, polishing and surface structuring of metals: fundamental aspects and new developments[END_REF]. Then, the sharp edges of the preforms were smoothened by mass transport-limited dissolution. The parameters used for the preforms and dissolution, which are required to create a final sinusoidal topography, were determined using numerical simulations of the process based on the work of West et al. [START_REF] West | Shape changes during through-mask electrochemical micromachining of thin metal films[END_REF]. Images extracted from the simulated process are shown in Figure 1: part (a) to (c) correspond to the first step (i.e. preform creation through mask electrochemical micromachining) while part (d) to (f) illustrate the second step (i.e. mass transport limited dissolution of the preforms after removing the masks). Four three-dimensional sinusoidal surfaces (similar to egg boxes) were produced in AISI 316L stainless steel, which is a common austenitic stainless steel. Table 1 summarizes the main targeted geometric characteristics of the studied surfaces (amplitudes and periods). Figure 2 shows examples of topography measurement of the examined specimens.

Sample name

Measurements

Topography measurements were performed with a white-light interferometer (Zygo NewView TM 7300, Zygo Corp., CT, USA) with 100x objective. The lateral resolution was equal to 0.22µm and the vertical accuracy was about 1 nm. This objective gave elemental surface measurements of 69.5 µm x 52.1 µm. These elementary surfaces were then stitched with an overlapping of 20% to obtain large measurement areas (1004 µm x 1004 µm for 030_03, 100_03 and 100_10 specimens and 1997 µm x 1997 µm for the specimen called 300_30). Large measurements with high accuracy were required to allow us to easily rotate the areas to correct the sine alignment and to extract areas containing five sine periods for the assessment of the surface quality (waviness, period quality, sine shape quality). Then, non-measured points were filled based on the height of the neighboring points. Finally, the measured areas were rectified using a polynomial of degree 1 to correct any rectitude issues, which are not part of the metrology quantification.

Results

First, the microroughness on the sinusoidal surfaces was assessed. It was found that the stitched measurements could not be used for this quantification as stitching can introduce local errors in the measurements. Figure 3 illustrates the local defaults introduced by stitching: in part a of this figure, an area of 100 µm x 100 µm was extracted from the measurements of 300_30 while in part b, the same area was filtered with a high-pass Gaussian filter with a cut-off of 3 µm. This filtering enabled us to remove the sine shape to examine the microroughness of the surface. In the example shown in Figure 3.b, the maximum height Sz is equal to 0.71 µm. This value is small but may introduce some error in the determination of the microroughness. As a consequence, the elemental measurements of 69.5 µm x 52.1 µm were used to assess the microroughness of the surface. To remove the form, a high-pass spline filtering [START_REF] Standard | ISO 16610-62 -Geometrical product specifications -Filtration -Part 62: Linear areal filter -Spline filter[END_REF] with a cutoff of 5 µm was used. Finally, the arithmetic mean deviation Sa [START_REF] Standardization | [END_REF] was computed for each elemental surface. Some elemental measurements were removed because there were outliers or measurement disturbances therefore 4000 elemental surfaces were used for each case. Table 2 shows the average and standard deviations of Sa obtained for the four cases, as well as the ratio of the peak-to valley amplitude by the average of Sa.

Specimen name Average Sa (nm) Standard deviation Sa (nm)

A/Sa

030_03 12 1 261 100_03 1 1 4286 100_10 1 1 16667 300_30 1 1 60000
Table 2: Average and standard deviation of Sa computed for each specimen, using elemental surface measurements. The ratios of the peak-to-valley amplitude of the surface by the average Sa is also provided.

The values found for the average and standard deviation of Sa are very low: The computed values were around 1 nm. Moreover, the ratios of the peak-to-valley amplitude of the surfaces by the average Sa ranged between 261 and 60000, highlighting the smoothness of the surfaces.

To explain the differences of values, examples of microroughness are given in Figure 4 for all the specimens. It can be seen that some pitting took place in specimen 030_03, thus explaining the higher value of the average Sa. In Figure 4 b and c (corresponding to 100_03 and 100_10), the grain boundaries of the metal can be observed. Local holes can also be present and were caused by the process. The waviness of the sinusoidal surfaces was then quantified, using square areas containing 5 x 5 periods. A low-pass Gaussian filter [START_REF] Standard | ISO 16610-61 Geometrical product specification -filtration -Part 61: Linear areal filters -Gaussian filters[END_REF] with a cut-off equal to the length of the measurement divided by 1.66 was found to be correct to remove the sine shape. Examples of computed waviness are given in Figure 5. The arithmetic mean deviation Sa was computed on each resulting surface. This method was performed five times for each configuration. Table 3 summarizes the average and standard deviations of Sa obtained for the four cases , as well as the ratio of the peak-to valley amplitude by the average of Sa. Some waviness was detected as the average Sa was comprised between 0.04 µm and 0.15 µm. However, the ratios of the peak-to-valley amplitude of the surfaces by the average Sa remained large, thus emphasizing the quality of the surfaces obtained with the two-step process. The average Sa values were found to be higher with an increase of the amplitude or period. This could be partly explained by an increase of the area size used in the computation. However, specimen 100_03 and 100_10 have both the same area size and the average Sa was found to increase with an increase of the amplitude of the sinusoidal shape. New specimens would be required to confirm this trend.

The accuracy of the sine period was assessed using image segmentation: the watershed algorithm [START_REF] Standardization | [END_REF] allowed us to decompose square areas containing 5 x 5 periods into motifs. Then, the minimum pitch between two identified peaks was computed. This method was applied five times per specimen. Figure 6 shows an example of segmentation for a measurement of specimen 100_10. The average results obtained for the pitch are presented in Table 4. The relative error corresponding to the subtraction of the aimed period from the identified pitch, divided by the aimed period was also computed and is shown in Table 4. The identified average minimum pitches were slightly lower than the aimed periods, for all the specimens. Specimen 100_03 showed the maximum relative error. This specimen had the only configuration in which the period-to-amplitude ratio was different from 10. This difference may explain the increased maximum relative error. The minimum relative error was found for the larger motifs i.e. for specimen 300_30. The relative error remained lower than 1.5% for all the specimens, which highlighted the regularity of the period.

Finally, the regularity of the sine shape was assessed by minimizing the differences of shape between square measurement areas containing 5 x 5 periods and the following mathematical function:

𝑍 = 𝐴(cos ( 𝑋 𝑃 + 𝜑 1 ) * cos ( 𝑋 𝑃 + 𝜑 2 )) (1)
where Z is the height, X are the in-plane coordinates, P is a parameter proportional to the period, A is the amplitude and φ1, φ2 are the phases. It should be noted that the chosen mathematical model only contained two main parameters A and P as φ1, φ2 were only part of the equation to adjust the beginning of the sine shape to the cutting of the sine shape measurements. The choice to use of only two main parameters in the description was made to be "mathematically unfavorable" i.e. it minimized the degrees of freedom in the minimization, thus hardening the quality criteria.

Once the parameters of the mathematical function were identified thanks to a non-linear regression, the quality of the surface shape was quantified through the computation of the residue, which is the standard deviation of the height of the identified mathematical function subtracted by the height of the measured surface. Again, this methodology was applied five times per specimen. Figure 7 shows an example of measured surface, the computed surface obtained with the identification of the parameters and the surface obtained by the subtraction of both surfaces, with which the residue was computed. Table 5 summarizes the results obtained for the computed residues. Again, low values were found for the residue average. This result is highlighted by the computation of the ratio of the peak-to-valley amplitude of the surfaces by the residue average: values ranging from 16 to 39 were found. These ratios may seem lower than the ones previously computed, however, the residue average contained all possible errors on the sinusoidal shape.

The residue standard deviations were also small thus showing good repeatability of the results.

Discussion

The analyses of topography measurements showed that the presented three-dimensional surfaces had very good characteristics: low waviness, very low residual micro-roughness on the sine shape and an accurate sine shape with very regular period. Such three-dimensional sinusoidal surfaces, at the microscale, are rarely reported in the literature. Only three studies showing three-dimensional sinusoidal surfaces having comparable microscale motifs were identified in the literature: the corresponding characteristics of the surfaces are listed in Table 7. First, it should be noted that the period/amplitude ratios were either equal to 10 or 33 for the surfaces presented in this paper while this ratio is between 25 and 750 for [START_REF] Chen | Large-area profile measurement of sinusoidal freeform surfaces using a new prototype scanning tunneling microscopy[END_REF] and is equal to 25 and 1000 for [START_REF] Shimizu | Surface characterization of a diamond turned XY sinusoidal grating[END_REF] and [START_REF] Gao | Precision nano-fabrication and evaluation of a large area sinusoidal grid surface for a surface encoder[END_REF], respectively. Chen et al. [START_REF] Chen | Large-area profile measurement of sinusoidal freeform surfaces using a new prototype scanning tunneling microscopy[END_REF] compared the characteristics of the surface given by the manufacturer to the measurements made with scanning tunneling microscope. Deviations were found to be small for amplitude and period. As an example for the aimed period of 550 µm, they measured a period equal to 547.64±1.15 µm in the X-direction and 548.97±0.96 µm in the Y-direction, thus giving relative errors of -0.43% and -0.19%, respectively. These errors are of the same order of magnitude as the sinusoidal surfaces examined in this paper. The surface measurements of Chen et al. [START_REF] Chen | Large-area profile measurement of sinusoidal freeform surfaces using a new prototype scanning tunneling microscopy[END_REF] are shown to be around 1000 µm x 1000 µm thus indicating low waviness. However, no comments were made on possible micro-roughness. A closer look at the given figures show local defects on the summits thus possibly indicating micro-roughness on the sinusoidal shape. Shimizu et al. [START_REF] Shimizu | Surface characterization of a diamond turned XY sinusoidal grating[END_REF] used a three-dimensional sinusoidal surface to compare the results given by three devices: a confocal microscope, a white-light interferometer and an atomic force microscope. The different devices gave similar results for pitch and amplitude, confirming the dimensions given by the manufacturer. However, the use of two-dimensional discrete Fourier transform for the analysis of the measurements indicated a form error caused by the round geometry of the tool. Gao et al. [START_REF] Gao | Precision nano-fabrication and evaluation of a large area sinusoidal grid surface for a surface encoder[END_REF] gave similar results but showed that tool radius compensation was possible: the amplitudes of the error caused by the round-tip of the tool were reduced to several nanometers.

Reference

The previous comparisons remained limited but enabled us to identify a possible competing process: the use of a fast tool servo in diamond machining. This process produced sinusoidal surfaces having very good shape qualities. However, machining of metallic materials probably induced local strain-hardening or added residual stresses. The two-step process used to obtain the sinusoidal surfaces described in this paper did not induce any changes of sub-surface mechanical properties. This is a real asset for the examination of the link between surface morphology and functionality because it guarantees a decoupling of the examined effects. Topography effects are too often coupled with local changes of sub-surface mechanical properties thus introducing biases or errors in the results. As an example, this decoupling is particularly important in contact or wear study. Finally, through the characterization of sinusoidal surfaces, we were able to detect stitching errors in the measurements. These errors were minor at large scales but could have introduced some bias at the microscale when determining the microroughness. It seems that the quality of the examined sinusoidal surfaces i.e. their very good signal-to-noise ratio led to difficulties in local fitting of the elementary surfaces thus introducing stitching errors.

Conclusion

The topography of three-dimensional sinusoidal surfaces obtained with a two-step process were thoroughly characterized. It was shown that the two-step process consisting of electrochemical machining followed by mass transport-limited dissolution produced surfaces having very low microroughness: the Sa values used to quantify the microroughness ranged between 1 nm and 12 nm. The largest value was found to be caused by local pitting in a given specimen. The waviness of the surfaces was also quantified using the Sa parameter and the largest value was found to be equal to 0.15 µm. Higher values of waviness were noted with an increase of the amplitude or period of the sinusoidal surfaces but the production of other surfaces would be required to confirm this trend. The maximum relative error computed for the period was equal to -1.3% and was identified for the configuration having a period-to-amplitude ratio different from 10. Finally, the quality of the sinusoidal shape was assessed by minimizing the difference of height between the measurements and a corresponding mathematical function. Again, the computed residues were very small. A comparison of these results with the literature was difficult as the conditions or chosen data did not exactly match. The use of a fast tool servo in diamond machining was found to produce three-dimensional sinusoidal surfaces showing very good characteristics too. However, mechanical machining usually introduces local changes in the sub-surface properties. The two-step process used to build the sinusoidal surfaces examined in this paper avoids any local changes of mechanical properties. This is a real asset for the decoupling of the effects of the surface topography from the effects of residual stresses when examining a given functionality. Such decoupling would be particularly useful in the examination of contact and wear. Other perspectives of use can be mentioned for these surfaces:

-the addition of controlled microtexturation on the sinusoidal shape. This addition could help decoupling the effects of topography at different scales (sine shape and microtexture scales). Different fields could be interested by such applications: mechanics, biology, optics… -the addition of a thin film could be used to examine the influence of the topography of the interface on the adhesion of the film.

Figure 1 :

 1 Figure 1 : Images extracted from the simulated two-step process used to obtain sinusoidal surfaces having an amplitude of 10 µm and a period of 100 µm: (a) to (c) preform creation through mask electrochemical micromachining), (d) to (f) mass transport limited dissolution of preforms after mask removal.

Figure 2 :

 2 Figure 2 : Example of topography measurements for (a) specimen 030_03, (b) specimen 100_03, (c) specimen 100_10 and (d) specimen 300_30.

Figure 3 :

 3 Figure 3: (a) Extraction of an area 100 µm x 100 µm from a measurement of 300_30 and (b) corresponding area filtered with a high-pass Gaussian filter with a cut-off of 3 µm.

Figure 4 :

 4 Figure 4: Examples of microroughness for (a) specimen 030_03, (b) specimen 100_03, (c) specimen 100_10 and (d) specimen 300_30.

Figure 5 :

 5 Figure 5: Examples of waviness computed for each specimen.

Figure 6 :

 6 Figure 6 : (a) Example of a measurement of 100_10 containing 5x5 periods and (b) the decomposition of this measurement into motifs using the watershed algorithm. Specimen name Average minimum pitch (µm) Standard deviation (µm)

Figure 7 :

 7 Figure 7: Example of measured surface for 10_03, of the computed surface obtained with the identification of the parameters and of the surface obtained with the subtraction of the computed surface from the measured surface.

Period (µm) Peak-to-valley amplitude (µm) 030_03

		30	3
	100_03	100	3
	100_10	100	10
	300_30	300	30

Table 1 :

 1 Main targeted geometric characteristics of the sinusoidal surfaces

Table 3 :

 3 Average and standard deviation of Sa computed for the waviness of each specimen. The ratios of the peak-to-valley amplitude of the surface by the average Sa is also computed.

	Specimen	Area size	Average Sa	Standard deviation Sa	A/Sa
	name	(µm 2 )	(µm)	(µm)
	030_03	150 x 150	0.04	0.02	70
	100_03	500 x 500	0.04	0.01	73
	100_10	500 x 500	0.08	0.03	133
	300_30	1510 x 1510	0.15	0.05	205

Table 4 :

 4

Average and standard deviation of the minimum pitch between two peaks and the relative error, computed for each specimen.

Table 5 :

 5 Average and standard deviation of the residue. The ratios of the peak-to-valley amplitude of the surface by the average residue is also computed.

	Specimen	Residue	Residue standard	A/Residue average
	name	average (µm)	deviation (µm)
	030_03	0.185	0.016	16
	100_03	0.102	0.006	29
	100_10	0.339	0.019	29
	300_30	0.762	0.012	39

Table 6 :

 6 Table 6 summarizes the main characteristics of the examined sinusoidal surfaces. Summary of the characteristics of the examined sinusoidal surfaces.

	Specimen	Microroughness: Sa	Waviness: Sa	Period relative	Residue (µm)
	name	(nm)	(µm)	error (%)
	030_03	12±1	0.04±0.02	-0.7	0.185±0.016
	100_03	1±1	0.04±0.01	-1.3	0.102±0.006
	100_10	1±1	0.08±0.03	-0.4	0.339±0.019
	300_30	1±1	0.15±0.05	-0.1	0.762±0.012

Table 7 :

 7 Characteristics of the three-dimensional sinusoidal surfaces of the literature.

		Process			Peak-to-valley amplitude	Period
	Chen et al.	Fast	tool	servo	2 µm (measured to be	150 µm
	[7]	(diamond machining)	1.96±0.045 µm)
					2 µm (measured to be	300 µm
					1.93±0.060 µm)
					0.6 µm (measured to be	450 µm
					0.58±0.035 µm)
					22.06±0.7 µm (measured to	550 µm (measured to
					be 21.95±0.11 µm)	be 547.64±1.15 µm
						in the X-direction
						and 548.97±0.96 µm
						in the Y-direction)


I Dragomir
email: idragomir@gmv.com

M Bozga

I Ober

D Silveira
email: daniel.silveira@gmv.com

T Jorge

E Alaña
email: ealana@gmv.com

M Perrotin
email: maxime.perrotin@esa.int

FORMAL VERIFICATION OF SPACE SYSTEMS DESIGNED WITH TASTE

Model-Based Systems Engineering (MBSE) is a development approach aiming to build correct-by-construction systems, provided the use of clear, unambiguous and complete models to describe them along the design process. The approach is supported by several engineering tools that automate the development steps, for example the production of code, documentation, test cases and more.

 to enable the formal verification of properties on TASTE designs. The approach is currently under development in the ESA MoC4Space project.

INTRODUCTION

Developing space systems is a difficult task, where the engineers need to address two challenges: (1) how to design large and complex systems with minimal effort and cost, and (2) how to ensure that the designed system is correct with respect to its requirements. Model-Based Systems Engineering (MBSE) is an adopted development approach aiming to address the above challenges by enabling correct-by-construction system design from which the implementation could be generated and deployed on the target platforms.

More specifically, MBSE allows to produce unambiguous, consistent and coherent designs of the system which can be subject to validation and verification with respect to system properties during the development cycle. By design we understand system architecture, behaviour and data types, as well as deployment strategy. By validation and verification we understand an assortment of techniques including design review, testing, interactive simulation and model-checking. While the first three methods allow to detect errors within the design in a lightweight manner (i.e., only a subset of the system's behaviours are evaluated), model-checking exhaustively analyses the system's behaviour and gives a verdict for property satisfaction. TASTE [START_REF] Taste | The Assert Set of Tools for Engineering[END_REF] is an MBSE toolset supported by ESA which enables system design and validation. Several languages are available for system design: ASN.1 for data types, a flavour of AADL for hierarchical architecture, SDL for behaviour modelling, and Ada/C/C++ when manual coding is needed. The toolset offers as features static type analysis, real-time scheduling analysis, code generation and binary applications generation for target platforms, as well as simulation, debugging and testing. A feature not yet supported by the toolset is the formal verification of the system design with respect to system properties.

The ESA Model-Checking for Formal Verification of Space Systems (MoC4Space) project aims to develop and 1 integrate in TASTE various model-checking tools to automate the formal verification of system properties. In the following we describe the approach considered and the development status.

MODEL-CHECKING TASTE DESIGNS

Overview

The proposed model-checking approach for a TASTE design and related properties, consists of the following steps as illustrated in the workflow from Figure 1: 1) The user designs the system with TASTE. The design consists of data view (ASN.1 data types), interface view (AADL hierarchical system architecture), SDL state machines/C implementation/GUI function (system behaviour).

2) The user specifies with TASTE the safety properties the system shall fulfil. Properties can be specified in three 3) The user invokes the model-checker. The user selects the properties to be checked from those specified and sets the configuration of the modelchecker. The model-checker works on the system design and the specified properties. The system behaviour is explored and the properties satisfaction is checked on all possible behaviours. A result is provided to the user: either the properties are validated and a message is displayed, or a property is violated and diagnostic traces are produced.

4) The user checks the result provided by the model-checker. If the properties are satisfied, then the workflow stops. If the property is not satisfied, the obtained diagnostic traces are played in TASTE and assessed individually.

If the diagnostic trace shows a valid behaviour for the system, then the defect is corrected and the process starts again. If the diagnostic trace shows an invalid behaviour, the next available diagnostic trace is analysed or the process stops. (Note that the model-checker will intentionally explore a superset of the system's executions, in particular by relaxing certain scheduling constraints. In consequence, diagnostic traces can show invalid behaviours.)

Tool Design

To enable the workflow explained above, the following extensions are required:

(1) property specification in TASTE, (2) model-checker for TASTE designs and properties and (3) seamless integration of the approach in the TASTE GUI.

Property Specification in TASTE

Three types of properties are considered for model-checking: Boolean stop conditions (BSC), Message Sequence Charts (MSC), and dynamic observers.

Boolean stop conditions describe invalid behaviour of the system, e.g., stop if (battery_level < 10). These properties are Boolean expressions that express system invariants (through their negation) and that should not evaluate to true at any point during the execution. Informally, the satisfaction of the Boolean condition means that an undesired state has been reached, and therefore the system design is not correct. Such properties are modelled in TASTE as dynamic observers in OpenGEODE (see below). The user will select BSC property from a dedicated menu in the TASTE GUI, and an SDL observer (with 2 states and 1 decision) is generated and displayed using OpenGEODE. Then the user can directly specify the condition with the available SDL syntax for observers.

MSC properties describe the (un)desired behaviour of the system as a sequence of I/O events happening between the system's functions. Such properties are specified using the MSC editor available in TASTE. The user will select MSC property from the dedicated TASTE GUI menu, and the MSC editor is opened for the user to specify the property. The meaning of an MSC as a system property depends of specific annotations: Verify indicates that all system executions must comply with (a prefix of) the MSC. From-start indicates that the MSC shall be matched from the beginning of the execution between the specified functions. Nonstrict indicates that other I/O events that are not specified can happen between the functions. Intended indicates that the MSC is a desired execution sequence, while unintended indicates that the MSC is an undesired sequence. Then the model-checker will provide a result consistently with the type of property indicated by the user.

Dynamic observers describe both desired and undesired behaviour of the system in the form of state machines. They are the most expressive properties considered, as they can monitor the system execution, but also alter it for example to guide the verification process. Observers are represented as SDL state machines in OpenGEODE. The user will select the Observer property in the dedicated TASTE GUI menu, and OpenGEODE will be displayed in which the property is modelled. The user has then access to the SDL extensions for observers that allow them to observe (1) the state of the TASTE system at a point in its execution (specifically, the values of variables and state machine location for the functions) and (2) the events that occurred during the last atomic transition taken by one of the SDL functions of the TASTE system. The user specifies whether the execution is desired or undesired by labelling the states of the observer with success or error accordingly. Then the model-checker will correctly assess the property on the system executions.

Integrated Model-Checking

Model-checking ([2], [START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF]) is a well-known formal verification technique for the system correctness with respect to a set of properties. It consists in building a finite state-space model of the system under analysis and checking the properties on this model. The check itself amounts to a complete or partial exploration of the state space, potentially guided by the properties. The main advantage of model-checking is that it can be fully automated. Moreover, it allows for the production of diagnostic traces when a property is not verified, that can help the engineer to correct the design. The main drawback is, however, the potential size of the state-space model which depends on the system complexity and which could make model-checking infeasible.

Several solutions can be considered for developing a model-checker for TASTE: (1) re-use of an existing off-the-shelf model-checker (e.g., IF [START_REF]The IF toolset[END_REF], UPPAAL [5]), ( 2 Property transformation implies obtaining an IF observer for each TASTE system property. A dynamic SDL observer is transformed to an IF observer (OBS2IF) in mostly the same way as an SDL state machine is transformed to an IF process. In fact, the OBS2IF component is an extension of SDL2IF component with the specific handling of the observers' syntax and semantics. A BSC property is modelled as an SDL observer, so the same OBS2IF component is used for obtaining an IF observer from them. Finally, an MSC property is also transformed into an SDL observer (MSC2OBS). This transformation has the benefit of obtaining and displaying graphically the property to be checked into another formalism known by the user, i.e., SDL. Also, the user has the possibility of enhancing the property represented as SDL observer as desired, since observers are more expressive than MSC properties. Then the OBS2IF is called on the SDL observer representation of the MSC to obtain the corresponding IF property that will be checked.

Diagnostic transformation implies obtaining an MSC from the diagnostic traces provided by IF (SCN2MSC). The IF model-checker provides diagnostic traces as a sequence of IF transitions steps, each including labels of the actions executed (inputs, outputs, process creation, deletion, etc.). MSC is the most usable formalism to visualize such diagnostic traces and to replay them in the TASTE environment, thus easing the understanding of the result(s).

To provide a seamless integration in TASTE of the model-checker, the TASTE GUI is extended with a model-checker configurator and launcher (see Figure 3). The configurator allows to specify the environment of the system under validation, the properties to be checked and the model-checker options (e.g., number of diagnostic traces generated, number of states explored), The launcher allows to call and stop the IF model-checker. The TASTE build system is also extended to invoke the above-mentioned transformations and model-checker.

Tool Validation

The TASTE model checking approach is validated on two industrial case studies: the IXV mission and the ERGO planetary scenario [START_REF]European Robotic Goal-Oriented Autonomous Controller (ERGO) H2020 project[END_REF]. The IXV mission aimed to define the basic needs for re-entry from Low Earth Orbit. The case study considered in this activity is a subset of the fully-automated on-board software that focuses in the flaps control system. The ERGO planetary scenario is inspired by the Mars Sample Return (MSR) mission that covers the concepts and requirements of the Martian Long Range Autonomous Scientist. The case study considered in this activity consists of a subset of functionalities, "simulating" (simplified) traverse and sample collection, image acquisition, as well as system commanding in E1 (telecommanding) and E4 (goal commanding) autonomy modes. Both case studies have been modelled in TASTE with the concepts supported by the model-checker and several properties of each type have been defined for both (the complete TASTE design is available at [START_REF]MoC4Space GitLab[END_REF]). The model-checking approach will be used to check the correctness of the modelled systems with respect to their properties. Also, errors are specifically introduced in the system design to validate the model-checking results.

DISCUSSION

The MoC4Space project aims to develop formal verification system designs and properties modelled with TASTE. The model-checking approach has been defined, as well as the tool architecture based on the existing IF model-checker as backend. The implementation of the integrated model-checking tool (property modelling editors, ASN2IF and SDL2IF) is ongoing. The approach and tool are validated and will be used to verify two space systems case studies fully developed with TASTE for the purpose of the activity.

  property type: search [[from-start|nonstrict]] ((intended|unintended)) or property type: verify [[from-start]] intended, where [[ ]] denotes an optional part and | denotes a choice.Search indicates that the model-checker will look for a system execution complying with the MSC.

Figure 2 .

 2 Figure 2. Examples of properties with TASTE: (a) Boolean stop condition / dynamic observer modelling an error if the battery level is lower than 10 units, (b) MSC property modelling that if the battery level drops below 15 the FDIR stops the system.

  ) re-use an existing open model checker platform (e.g., LTSmin [6]) or (3) develop a dedicated model-checker. From the trade-off analysis of the different options, we have selected to re-use the IF toolset as model-checking back-end. The IF toolset [4] is an environment for modelling and validating real-time systems, characterised by the following key features: (1) a modelling formalism (also called IF) based on extended Timed Automata with urgencies and asynchronous FIFO-based communication, syntactically and semantically close to SDL, (2) properties specification to be validated on models as dynamic observers, (3) combined use of various validation techniques including modelchecking, static analysis of the IF model representation and simulation, (4) generation of diagnostic traces in the case of property violations, and (5) support for high level modelling with formalisms such as SDL, UML, SysML used in industrial CASE tools, through translation of high level models into the IF notation. Using the IF model-checker as back-end requires that bidirectional transformation are defined between TASTE and IF. These transformations cover (1) generating the IF system model from the TASTE design views, (2) generating the IF observers from the TASTE system properties, and (3) generating TASTE MSC representation from the model-checker diagnostic traces. An overview of the tool architecture in provided in Figure 3.

Figure 3 .

 3 Figure 3. TASTE model-checking tool architecture. Boxes in red represent new/enhanced modules, black arrows existing information/ dependency flow, and red arrows new information/dependency flow. Model transformation implies obtaining an IF representation from the TASTE design. This module is composed of several components. ASN2IF transforms the ASN.1 datatypes specified in the TASTE data view to IF datatypes. AADL2IF transforms the system structure specified in the TASTE interface view to an IF model. This component also handles the specific transformation for GUI functions (modelling the environment), C functions behaviour and timers

  This paper was presented at ESA's Second Virtual Workshop on Model Based Space Systems and Software Engineering (MBSE2021). https://indico.esa.int/event/386 ways, from the least to the most expressive: Boolean stop conditions, Message Sequence Chart properties, and dynamic observer properties.

	This project is funded by the European Space Agency under contract number 4000133658/21/NL/CRS.

1