In the AVACS Collaborative Research Centre, top Computing Science researchers have made supposedly "undecidable" problems in safety-critical systems manageable. In this interview, spokesperson Werner Damm looks back on an exciting twelve years.
QUESTION: Mr Damm, twelve years is the maximum duration for a Collaborative Research Centre, and you have made full use of it. Obviously AVACS is a complex topic?
DAMM: You could say that. AVACS stands for "Automatic Verification and Analysis of Complex Systems" - so the term "complex systems" is already in the title. Specifically, it is about technical applications that are relevant to safety, for example the electronics in an aeroplane or car. Now, AVACS is not a project of the Federal Ministry of Education and Research, but a Collaborative Research Centre. We therefore had no intention of developing such systems. We were much more interested in making the complexity that we observe on the market mathematically manageable in order to be able to prove that the systems are safe. That was the central concern of AVACS. And we have succeeded: our results are simply amazing.
QUESTION: In what way?
DAMM: Computing Science recognises the terms "decidable" and "undecidable". In other words, there are problems that are undecidable - you could bring together as much computing power and as many clever minds as you like, but they simply cannot be solved. This often occurs with systems that satisfy non-linear differential equations: Even the smallest changes can cause major disturbances. For example, if a pilot pulls a little too hard on the joystick, this can - if the electronics don't catch it - lead to an extreme steep dive. Until now, it has not been possible to formally prove that such systems are safe. It was undecidable. Then AVACS came along - and we showed that it is possible after all.
QUESTION: How did you manage that?
DAMM: Let me explain with an example: Let's take autonomous driving. A large number of cars have to be coordinated at a junction to prevent accidents. It is not possible to prove the safety of these systems - the basic idea is that there are an unlimited number of cars. But you can, for example, go there and hide the unimportant information - such as the licence plates of the cars. This simplifies the whole system. In addition, we were even able to prove mathematically - not least because of the suppression of the licence plates - that it is not necessary to provide proof for an unlimited number of cars - it is sufficient if I provide it for a certain number. How many cars there have to be can be derived from the safety requirements, for example there are specifications as to how much minimum distance there has to be between the vehicles. In this way, a supposedly undecidable problem becomes decidable. This is just one example. In AVACS, we have been able to make several such statements that are truly groundbreaking.
QUESTION: That sounds like a success across the board...
DAMM: It couldn't be better. We can't rate these results highly enough. They can be used for all technical systems in which non-linear differential equations are relevant: Chemical production processes, the controls of nuclear power plants, the stabilisation of energy grids - you could even use these methods to analyse whether our energy supply can withstand a terrorist attack. The secret of AVACS was that we brought together people who, on the one hand, understand something about the applications - as in our example, that the control system of a car doesn't really care what licence plate it has - and, on the other hand, have mastered modelling, i.e. the necessary proof procedures.
QUESTION: And these skills are all available here in Oldenburg?
DAMM: We have formed a team with scientists from Oldenburg, Saarbrücken and Freiburg, who have contributed from very different backgrounds. Here in Oldenburg we have the expertise in modelling and the application know-how, in Saarbrücken there is a great deal of knowledge about real-time analysis techniques and probability theory, and our colleagues are also very familiar with algorithms and logical foundations. Freiburg was our centre for circuit verification and efficient representation of complex sets.
QUESTION: That all sounds very complex. Where do you start?
DAMM: We simply listened to our intuition: it can hardly be that on the one hand we have constantly falling accident rates in the aviation industry, but on the other hand there are these undecidability results. So we first looked at how the experts in the industry do it. We have been working with Airbus for over 20 years and know their development processes in detail. We discovered that Computing Science theorists and industry are worlds apart: the theorist wants to analyse situations that are not at all possible in practice - for example, that an immense amount of information has to be coded in a finite time interval. However, a look at practice shows that the systems are clocked, so there is not an unlimited amount happening. This is the point at which we scientists become active: We pack our intuition into a formal model. That's the fun of scientific work.
QUESTION: Has AVACS solved all the problems of complex systems?
DAMM: Let me put it this way: we can use AVACS to say how systems should be built so that they are still manageable. The fact is that the systems are now interacting with each other, I'll just use the buzzword "Internet of things": every part has a unique name - whether it's a coffee machine or a spare part for a vehicle - they can all be addressed individually in the network. This brings great advantages for industry, for example logistics can optimise their production processes because everything can be monitored. However, the market dynamics are so strong that companies start to build something purely pragmatically and then a system grows that can no longer be analysed. This may still be possible in logistics, but it is simply unacceptable for safety-critical systems such as autonomous driving. As a society, we are making ourselves dependent on ad-hoc systems whose risks we can no longer control.
QUESTION: Now you're kind of scaring me...
DAMM: Well, AVACS has shown how systems should be built so that they remain manageable. And there have been initial successes: our colleagues in Saarbrücken are proud to have convinced a well-known semiconductor manufacturer to build a processor generation in such a way that it can be analysed.
QUESTION: AVACS is now officially finished. Is the final report available yet?
DAMM: Almost, we are in the final stages.
QUESTION: How thick can I imagine it to be?
DAMM: Exactly 140 pages, that is a requirement of the German Research Foundation. It's quite a challenge to cover twelve years of research in so few pages. We will have to limit ourselves to the highlights. But fortunately, these 140 pages are not the only thing that remains of AVACS. There are many projects that follow. Here at the University of Oldenburg, we want to put people at the centre of several follow-up projects. It's a good thing that we have the School of Medicine on site, we work closely with the Department of Psychology and the Department of Health Services Research. We want to try to model people, and we are focusing in particular on observing brain activity.
QUESTION: Modelling people? That sounds a bit like science fiction...
DAMM: In fact, it's not that far-fetched. Autonomous driving will soon be a reality. However, humans will still play a decisive role in certain situations. Imagine you are sitting in an autonomous car, leaning back and watching a film. Suddenly a tyre bursts and the truck in front of you loses its load. The car is overwhelmed and says: Take over. What do you need at this point to be able to react appropriately? What can we as humans cognitively do in such an extreme situation? Here in Oldenburg, we have a fantastic opportunity to delve a little deeper into human modelling together with our medical colleagues. This is the subject of the "Critical Systems Engineering for Socio-Technical Systems" project, which has emerged from AVACS. Incidentally, we are also planning a new collaborative research centre in this direction. We want to use what we have developed in AVACS for technical systems to understand the interaction between humans and technical systems.
QUESTION: Are there any other projects?
DAMM: There are several transfer projects that bridge the gap to industry. These involve, for example, the verification of software in assistance systems. My Oldenburg colleague Martin Fränzle has developed algorithms that now ensure that the wheels of Airbus aeroplanes are extended.
QUESTION: So you can draw a thoroughly positive conclusion...
DAMM: Definitely. It's a field of research that is totally exciting. It's relevant, it involves interdisciplinary work, you have to be able to do a lot of maths, everything just fits together really well. It was anything but a matter of course that we were able to build up such a team spirit, that a community of scientists was created across three locations. Around 80 researchers were involved. And we had an extremely pleasant working environment.
Interview: Birgit Bruns