Our group works on the design of algorithms that allow computers to learn complex state diagrams by providing inputs and observing outputs. This is an exciting area in which we collaborate with the Digital Security group to learn models of security protocols and also with several companies (e.g. ASML, Philips Healtcare, Canon Production Printing, Thermo Fisher and Axini). We refer to the review article by Frits Vaandrager in Communications of the ACM for a general introduction. In model-based testing, a model is the starting point for testing. This model expresses precisely and completely what a system under test should do, and should not do, and, consequently, it is a good basis for systematically generating test cases. Model learning and model-based testing are complementary techniques. In particular, model-based testing can be used to find counterexamples for candidate models produced by model learning techniques. There are several opportunities for theoretical, tool/programming oriented, and application oriented projects related to model learning and model-based testing:
Did you like the Algorithms & Data Structures course and would you like to design algorithms? Or did you like the Languages and Automata course and are you interested in theory? Well, we can define dozens of projects on automata learning that involve algorithm design and/or theory. We recently proposed a new learning algorithm for finite state machines, L# and a prototype implementation in Rust outperforms all existing active learning algorithms. But many questions remain related to the design, implementation and analysis of learning algorithms, ranging from super practical to super theoretical:
(contact Frits Vaandrager or Jurriaan Rot).
Did you like the Computer Networks course and do you find it interesting to understand the details of protocols? There are many possibilities for projects in which the goal is to learn models of protocol components. We are particularly interested in learning models of security related protocols (like TCP, SSH, TLS, EMV, etc). Model learning may help us find specific sequences of input events that exhibit security vulnerabilities. (contact Frits Vaandrager or Erik Poll).
Model learning and model-based testing are popular research topics and during recent years numerous researchers have proposed new learning and testing algorithms for slightly different modelling frameworks, which then are evaluated on a few case studies. However in order to get real scientific progress, it is important to have a big, shared collection of benchmarks that can be used for the evaluation of all these algorithms, supported by tools that support translations between different modelling frameworks. In 2019, we have set up a repository with a publicly available set of benchmarks of state machines that model real protocols and embedded systems to allow researchers to compare the performance of learning and testing algorithms. There is still much work to do in extending this repository with new benchmarks and software, and properly comparing the performance of existing learning and testing algorithms. This is an area where, as a student, you may have real impact and do work that is much appreciated by scientists around the globe. (contact Frits Vaandrager).
For model-based testing, we are working on the TorXakis tool. Also here there are several possibilities for tool oriented projects. Examples are the connection of TorXakis to other tools, such as constraint solvers for test-data generation, to model-checkers for validation of test models, and to industrial and popular testing frameworks (SoapUI, Robot Framework, Behave, ...) for combining model-based testing with existing testing practices. Other possibilities include improving the performance of TorXakis, extension of the TorXakis modelling language, visualization of TorXakis models and test results, and the implementation of new test generation algorithms. (contact Jan Tretmans).
Theorists have developed a powerful set of algorithms for conformance testing of deterministic Finite State Machine models, see e.g. Lee & Yannakakis. Now a problem is that in practice systems often are nondeterministic and do not exhibit the strict alternation of inputs and outputs from the FSM model: sometimes an input is not followed by any output at all, sometimes an input is followed by a series of outputs. Jan Tretmans has developed a popular theory of testing for this general class of systems, but there are still very few algoritms for efficient conformance testing in this general setting. Recently, we have published papers on combining Tretmans' theory with the theory of Finite State Machines, see here and here, but this theory requires some next steps to make it applicable and to implement in the model-based testing tool TorXakis. The goal of this project would be to extend, adapt, and apply this theory. (contact Frits Vaandrager or Jan Tretmans).
Concolic testing is a combination of symbolic and concrete testing applied for white-box testing, which, among others, is successfully used by Microsoft. Model-based testing (MBT) is a promising approach for black-box testing. The goal is to combine these two approaches by applying the concepts of concolic tesing to (ioco-based) MBT, in order to improve test selection for MBT (contact Jan Tretmans).
Current systems are huge. Scaling model-based testing to such large systems is a challenge, in particular the selection of appropriate test cases for testing. One approach is to use usage (operational) profiles as the basis for testing, i.e., using users' scenarios as the basis for test selection. The goal is to combine user profile-based testing with ioco model-based testing (contact Jan Tretmans).
Axini is a spin-off of the University of Twente, based on research by Jan Tretmans and his students on model-based testing. The company specializes in test automation and aims at the application of formal methods in practice. There are several MSc thesis projects available at Axini. We are collaborating with several other companies that are interested in the potential of new learning and testing techniques, for instance, ASML, Philips Healthcare, Tom Tom, Vanderlande, InTraffic, SpronQ or the users from the TicToc project on testing (contact Mathijs Schuts, Jan Tretmans or Frits Vaandrager).