Back to research topics

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.

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: