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 works by checking so called Linear Time Logic (LTL) properties against transition systems. 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 has worked at the university of Twente and is an expert in the field.
All the work around model checking of symbolic transitions systems is too much for one graduation project. There are several puzzles and research questions that we see.
- LTL formulas1. An LTL formula is not something that our clients 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?
- LTL formulas2. How can we relate LTL formulas to test cases? How can we check that a test case with data and time satisfies a property?
- How can we model check STS-models directly, I.e., without converting them to LTL models?
- Can we apply LTS model checking algorithms to STS models?
- A design and implementation of a human readable LTL domain specific language
- A design and implementation of an LTL checker for test cases
- A design and implementation of (part of) an STS model checker