Model checking of symbolic transition systems

Read more about this research topic.

Back to research topics

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.

Possible deliverables: