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). We pragmatically added time as a concept to our models. While it works surprisingly well in many cases, we like to improve on it to cover all possible use cases of time in an efficient way. For Timed Automata there exists a timed testing theory. We would like to extend this to symbolic transition systems.
Timed Automata are a kind of transition system with clocks as a primary concept.
An interesting aspect of timed testing is the timestamps itself. It's relatively easy to determine if an output of the system under test in on time. But can we also guarantee that inputs occur fast enough?
Another interesting aspect is that time variables are monotonic and from the domain of real values. Based in the timed automata theory it seems that we can make use of this to compute or pre-process many of the time constraints compile time.
The models of Axini make use of symbolic transition systems (STS), which include data in the form of variables, assignments and conditions. We also have a limited form of time and timed testing, but Timed Automata are more powerful.
At Axini we have ample knowledge and experience in test automation and timed testing. 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.
- Extend the STS based test theory with time
Study the theory of timed testing and include the relevant concepts in the so called IOCO theory of Jan Tretmans.
- Implement a timed testing algorithm
Create an algorithm that implements timed testing for the Symbolic Transition Systems that Axini uses.