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.
The formal theory of model based testing makes use of Symbolic Transition Systems (STS), a form of labeled transition systems (LTS). For LTS models, academia has developed model checking algorithms that can check whether models meet certain properties. This technique can be used to validate the design of the system before it is built.
Model checking uses so called Linear Time Logic (LTL) to express properties to check against the transition system. An LTL property is a logical formula that can express a reachability or safety property.
The models of Axini make use of symbolic transition systems (STS), which include data in the form of variables, assignments and conditions. This addition increases the expressiveness and testing power of our models but makes the LTS model checking algorithms from academia difficult to apply.
Another challenge is ensuring that the model checker can be seamlessly integrated into our tool. To achieve this, it must operate without relying on third-party components that are incompatible with our existing systems.
At Axini we have ample knowledge and experience in making LTS based (or so-called explicit state), model-checkers. For example, Dr. Ir. Machiel van der Bijl did his PhD in the formal methods group of the University of Twente. We have contact with several research groups at universities to help and guide where needed.
Possible research questions
There are several puzzles and research questions that students can work on.
- Human readable LTL formulas
An LTL formula is not something that our customers can and will use without problems. It is a potentially complex formula with complex symbols that are hard to relate to the domain of the client. How can we express LTL formulas in a human readable way for which you do not need a PhD to understand them?
- Model checking STS models
How can we model-check STS-models directly without converting them to LTS models?
Recent work
Recent work at Axini on this topic:
- David Hildering (2025) is currently investigating how to use model checking related techniques like symbolic execution, path analysis etc. to efficiently compute test cases.
- Lucas Steehouwer (2022) has developed a proof-of-concept solution that is capable of verifying deadlock-freedom of Axini models. For this, Axini models are translated to Promela, the input language of the SPIN model checker.