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.
Example
Consider a simple model method:
def discount(price, customer_type)
if customer_type == :student && price > 50
return price * 0.9
else
return price
end
end A traditional random generator might test prices {10, 20, 100} and customer types {:student, :regular}, missing some edge cases.
With symbolic execution, the solver explores the conditions:- customer_type == :student ∧ price > 50
- customer_type == :student ∧ price ≤ 50
- customer_type ≠ :student
From this, Z3 generates concrete test inputs such as:
- (price = 60, customer_type = :student) → discount applied
- (price = 50, customer_type = :student) → no discount
- (price = 20, customer_type = :regular) → no discount
This ensures all meaningful behaviors are tested, without redundancy.
Possible research questions
There are several puzzles and research questions that students can work on.
- Scalability
What is needed to optimize the approach for large-scale systems to maintain efficiency as model complexity increases?
- Scope
Currently it only works for a subset of Ruby, could we expand this?
- Argue about models
Could we use this somehow to argue and think about the model code?
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.