Model checking is emerging as a practical tool for automated debugging of complex reactive systems such as embedded controllers and network protocols. In model checking, specifications about the system are expressed as (temporal) logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. In our research on model checking, we consider systems that are described as networks of timed automata in the sense of Alur and Dill. Our group is one of the two or three leading groups worldwide in the area of applying timed automata model checking to industrial sized problems. In part due to our work, tools such as Uppaal are now routinely used for industrial case studies. We follow an iterative approach where fundamental research on theory and algorithms - challenged by real-life case-studies - is developed and implemented in methods and tools, which are evaluated again through case studies.
Automata or state machines are key models for the design and analysis of computer systems. The problem of learning (reverse-engineering) automata automatically from trace data enjoys a lot of interest from the software engineering and formal methods communities because it provides insight into complex software systems, e.g., using model checking and testing techniques. Formally, automata learning can be seen as a grammatical inference problem in which execution traces are modeled as the words of a language, and the goal is to find a model for this language. Two frameworks can be used to learn such automata: passive and active. Passive learning focuses on learning the automata structure from data (logs). Active learning gathers such data by providing a black-box system with inputs and reading the corresponding output. Our group has build state-of-the-art tools for both passive and active learning of different kinds of automata models of software systems. The Tomte tool uses new automated abstractions to learn Mealy machines with parameters by actively querying a black-box component. The winner of the 2012 Stamina software model learning competition (DFASAT) was co-developed by our researchers. RTI is the first algorithm for passively learning timed automata. In addition, our group has made several important contributions to the theory and understanding of automata learning and is actively involved in automata learning programming competitions (Pautomac 2012 and RERS 2013).
Systematic testing is important for software quality, but it is also errorprone, expensive, and time-consuming. Model-based testing (MBT) is a new technology that can improve the effectiveness and efficiency of the testing process. With MBT a system under test (SUT) is tested against a formal description, or model, of the SUT's behaviour. Based on different modelling paradigms two approaches to MBT are pursued: the state-based and function-based approach. For the state-based approach there is a rich and well-understood theory for testing of reactive systems. This so-called ioco-test theory for labelled transition systems was developed by SWS members together with the University of Twente, and forms now the underlying theory for several MBT tools such as TorX, TGV, STG, TestGen, Uppaal-Tron, and Agedis. For the function-based approach algorithms to generate tests from formal models have been developed and implemented in the test tool Gast. Gast is based entirely on the state-of-art generic programming techniques that we have developed and incorporated in the functional language Clean. Gast has been successfully used to test libraries of higher order functions.
The holy grail we are looking for is the ability to generate a complete working system fully automatically from a model, with the aim of reducing software development time and increasing system reliability. This is clearly very hard to accomplish in general, but for specific problem areas it should be possible. Ideally one wishes to specify a system at a level of abstraction that is easily understood by domain specialists. For this purpose it is probably best to use a domain specific language. To cope with the intricacies of an actual system, a lot of detailed technical information needs to be supplied. The underlying modeling language must, therefore, possess powerful abstraction mechanisms enabling to abstract from low level details. For this reason we believe it is better to embed the modeling language in an advanced general purpose programming language. This also makes it commonly much easier to extend the modeling language with new constructs.
For over two decades, Nijmegen has maintained a leading role in the development of efficient functional programming languages, which has resulted in the freely available, state-of-art, pure, lazy functional programming language .