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.
At Axini we have ample knowledge and experience in making LTS based (or so-called explicit state), model-checkers. For example, Dr. Ir. Theo Ruys worked at the university of Twente and is an expert in the field.
Possible research questions
There are several puzzles and research questions that students can work on.
Recent work at Axini on this topic:
- 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.