Automata-Based Methods

Modelling is an essential part of many scientific and engineering disciplines. In this theme we study automata, (mathematical) models that describe software systems in terms of states and transitions between states. Automata-based models provide powerful abstractions that for instance allow us to verify systems whose behavior is uncertain, synthesize controller software that is correct by construction, and to develop learning-based testing algorithms that find deep software bugs. The research in this theme belongs to the general area of formal methods.

Verification of Probabilistic Systems

This focus area considers the verification of systems whose behavior is uncertain, e.g., due to the effects of sensors in the system. Examples for verification questions we ask are what is the probability that the system reaches an error state? and what is the expected time until we deplete our battery?. We assume that models are given in a high-level representation of a Markov decision process and study various extensions of Markov decision processes. Most techniques we develop are implemented in the probabilistic model checker Storm.

Synthesis

Supervisory controller synthesis is a main element of synthesis-based engineering. It involves the automatic generation of (provably correct) supervisory controller models. Implementation of the controller is achieved through (implementation language) code generation, improving speed and reducing the number of errors introduced at this stage. Combined, they allow engineers to focus on what the controller should do, rather than how it should do it, and how this is to be implemented. In the Explainable synthesis of supervisory controllers (ExSyn) project, in collaboration with ASML, we explore how to develop supervisory controllers more efficiently using synthesis-based engineering.

Learning and Testing

Model learning aims to construct aims to construct state diagram models of black-box software and hardware systems by providing inputs and observing outputs. Model-based testing is a testing method that uses a model (or specification) of the black-box behavior of a system to generate test cases to establish whether a system conforms to its specification. Model learning and model-based testing are dual activities: (1) we typically want to use model-based testing in order to increase our confidence in the correctness of a learned model and to find counterexamples, and (2) often a learned model may serve as a specification, for instance to check conformance of a refactored implementation.

Systematic testing is important for software quality, but it is also error-prone, expensive, and time-consuming. Model-based testing can improve the effectiveness and efficiency of the testing process. Model learning is emerging as a highly effective bug-finding technique, with applications in areas such as banking cards, network protocols and legacy software.

Within our group, we tackle the following research challenges:

• The design of algorithms for model learning constitutes a fundamental research problem. Recently, our group has designed the L# learning algorithm, which is of the most efficient algorithms to date. Our aim is to make learning algorithms even more powerful, that is, able to learn models with more states and input events with fewer data. Also, we aim to extend this algorithm to richer settings, allowing us to learn models of real-time systems, and systems with data parameters.
• We explore tight integration of algorithms for model learning and testing, through the conceptual framework of black-box checking and through the use of shared data structures.
• We advance foundational research in model learning in two directions: with approximation and with abstraction. Understanding approximation is key to measure the quality of learned automata, which is crucial to determine to what extent correctness properties that hold on the learned automaton actually hold in reality. Abstraction is essential to construct meaningful automata for large‐scale and realistic systems.
• High-tech systems come in many variants, customized for various users. These systems evolve over time to adapt to changing requirements and contexts. As a result, the number of possible different variants grows exponentially, making testing of systems with high variability and evolution a major challenge. Our aim is that not all versions and variants have to be completely re-tested, while still providing high, argued test coverage and confidence in the quality of the whole system. We follow a model-based approach using component-based and feature-driven testing.
• A mature research is characterized by the presence of a rich set of shared benchmarks that can be used to compare different approaches. We therefore maintain the automata wiki: a publicly available set of benchmarks of state machines that model real protocols and embedded systems. These benchmarks allow researchers to compare the performance of learning and testing algorithms.

Co-algebra

The categorical notion of co-algebra forms an ideal abstraction technique, as it describes systems in terms of observations and provides a general notion of "state-based system", generalising widely occurring structures such as automata, transition systems and probabilistic systems. Of particular interest is the interaction with algebraic structure: this interaction occurs for instance in the semantics of programming language At SWS we work on the interaction algebraic and coalgebraic techniques, and their application to concrete analysis tasks of systems, such as automata learning.

The interaction between algebra and coalgebra is also apparent in concurrency theory. Thus, for instance, we further develop algebraic models such as Kleene algebra and its extensions, together with coalgebraic decision procedures. We study notions of equivalence between (concurrent) systems through notions of behavioural equivalence and their intricate relationships with modal logics.

Please use the menu on the left for more information.