Axini develops tools for model based testing (MBT) and model based software engineering (MBSE). Model based testing is a software testing approach in which test cases are automatically generated and executed from a model, a formal specification of the system under test. This approach allows for a high degree of test automation and more thorough testing.

Our modeling and testing platform generates test traces on-the-fly (online testing). During testing, it generates input for possible next steps in the System Under Test (SUT). For example, when testing a webservice, sensible data is required to construct a correct webservice call. Our modeling language allows for the definition of constraints to define sensible data. These constraints are translated to SMT constraints and solved by an SMT solver. This results in data values that, if possible, satisfy these constraints such that a correct service call (a transition) can be made.

The above works fine for a single visit of the transition but often a transition is visited multiple times during a single test run. On these consecutive visits of a transition, we want to generate different data values that all satisfy the constraints and are randomly distributed. An SMT solver, however, cannot do this out-of-the-box. Although an SMT solver can generate random values, it will never guarantee that the values it generates for consecutive calls are randomly distributed. E.g. consider that we have the following constraint for a certain parameter: `i > 10 AND i < 100`. Solving this constraint with an SMT solver will give a correct value (e.g. i = 11). When the solver solves this constraint a second time there is a high chance that it will generate the same value again. This is not what we want. Ideally, we would like the solver to generate values that are somewhat randomly sampled from the domain (in this case 11..99) when the solver is called multiple times. Although there are techniques to force the SMT solver to return different values (such as Counterexample-Guided Extraction Refinement (CEGAR)), these methods do not guarantee random sampling of the domains.

For this assignment, if you accept it, you will investigate different techniques of solving constraints using SMT solvers and apply that to our context of solving constraints for testing. Ideally, you implement a prototype of different ways of handling the sampling and benchmark your result against a real-world test. There is existing research on this topic that you can use as a starting point.

## Possible research questions

There are several puzzles and research questions that students can work on.

## Recent work

Recent work at Axini on this topic:

- Florine de Geus (2020) investigated how an SMT solver can be used to generate data for testing.
- Her work was followed up by Sky Sarah van Grieken (2022), who extended the SMT-based constraint solver with the possibility to use hashes.