Timed testing with symbolic transition systems

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 themselves. It's relatively easy to determine if an output of the system under test is 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 on the timed automata theory, it seems we can use this to compute or pre-process many of the time constraints at 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. 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.