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.
This proposal introduces a novel approach to improve test case generation in Model-Based Testing (MBT) by integrating symbolic execution with the Z3 theorem prover. Symbolic execution systematically explores program paths within models by abstracting inputs into symbolic values, allowing exhaustive analysis of the execution space. The Z3 SMT solver is then utilized to resolve conditions along these paths, generating precise and practical test cases.
This methodology aims to overcome the limitations of traditional test case generation methods, which often produce redundant or irrelevant tests. By ensuring comprehensive coverage of all modeled behaviors, this approach enhances the efficiency and thoroughness of software testing, contributing to the reliability and robustness of applications.
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.