Model Based System Development/Move or Clean UP/Formal Methods

Formal Methods

Discipline

Most of our research fits into the discipline of formal methods: the applied mathematics of computer system engineering. Whereas traditional engineering disciplines rely heavily on continous mathematics (analysis, numerical computation) the design of dependable computer based systems requires a more discrete style of mathematical reasoning. These systems are typically modelled as discrete event dynamical systems (state machines, automata) and their specification and analysis requires the use of mathematical logic and advanced search algorithms to enable model checking and theorem proving.

The importance of research on formal methods stems from the fact that in safety critical applications a software error can have disastrous consequences. Design and programming errors are also the main source of cost overruns and security problems in software.

Apart from formal methods, our group also has expertise in the disciplines design of embedded systems, and distributed algorithms and protocols.

Research questions

The key problem with which the discipline of formal methods has to cope is scalability. We know how to analyse small models, but for larger models the state space that has to be explored tends to grow exponentially. To check very large systems, abstraction is therefore a key paradigm: the purpose of an abstract model is to retain those features of a system that are necessary to verify the desired property, and to omit all necessary detail. For verification of hardware and manually constructed models of embedded systems, distributed algorithms and protocols many generic abstractions (e.g. symmetries, data-path) abstractions have been proved useful. Software, however, is generally less structured and there the challenge is to automatically construct abstractions for a given system, using techniques such as predicate abstractions and counterexample guided abstraction. These techniques have recently been used to analyse programs with over 100,000 lines of C code. Still, scalability remains a key issue and in order to enable routine use of formal methods in industry much further research is needed.

An additional major challenge is to make it possible to analyze richer models in which apart from qualitative discrete events also quantitative information is included related to for instance real-time, probabilities, and continuous behaviour.

Application areas

Our group applies formal verification technology in a number of application areas. The most important of these is the design of dependable, real-time embedded systems. We also have a strong interest in modelling and analysis of distributed algorithms and protocols. In this area, new technologies such as ambient intelligence, sensor networks, and security protocols provide a us with a rich source of challenging verification problems. In our research on scheduling and resource allocation, we target applications in the areas of embedded systems, value chain management, and transportation/logistics.