Top computer scientists at the AVACS Transregional Collaborative Research Center have made problems in safety-critical systems that were allegedly "undecidable" solvable. In this interview AVACS Coordinator Werner Damm looks back on twelve exciting years with the project.

QUESTION: Professor Damm, twelve years is the maximum duration for a Transregional Collaborative Research Centre. You exhausted the full period. AVACS clearly deals with a complex subject?

DAMM: You're right about that. AVACS stands for "Automatic Verification and Analysis of Complex Systems", so the term "complex systems" is already in the title. To be specific it's about safety-relevant technical applications, for example the electronics in an aircraft or a car. AVACS is not a Federal Ministry of Education and Research project but a Transregional Collaborative Research Center [funded by the German Research Foundation - DFG]. So our goal wasn't to develop such systems. What we were aiming for was to make the complexity we observe on the market mathematically controllable in order to be able to prove that these systems are safe. That was AVACS' main goal. And we did it: our results are absolutely amazing.

QUESTION: In what way?

DAMM: Computer science uses the terms "decidable" and "undecidable". So there are problems that are undecidable – no matter how much computing capacity or how much brainpower you have, they simply aren't solvable. This often happens with systems that are governed by nonlinear differential equations: even the tiniest alterations can cause major disruptions. So for example when a pilot pulls a little too hard on the joystick this can – unless the electronics prevent it - cause the plane to nosedive. Until now it was impossible to provide a formal proof of the safety of such systems. It was undecidable. But then AVACS came along and showed that it can be done.

FRAGE: How did you do this?

DAMM: I'll use an example to explain. Take autonomous driving. At a crossroads a large number of cars need to be coordinated to avoid accidents. Proving the safety of these systems is an undecidable problem – in principle an unlimited number of cars can be involved. But you can, for instance, cut out irrelevant information – for example the cars' registration numbers. This simplifies the entire system. In addition – and not least because we'd taken the registration numbers out of the equation – we were even able to demonstrate mathematically that there is no need to provide a proof for an unlimited number of cars. It's enough to provide a proof for a specific number. How high that number should be we can derive from the safety requirements, for example the regulations on the minimum distance between the vehicles. In this way a supposedly undecidable problem becomes decidable. That is just one example. At AVACS we have been able to make several such statements that are truly revolutionary.

QUESTION: That sounds like success right down the line…

DAMM: It couldn't have been better. The importance of these results simply can't be overrated. They are useful for all technical systems in which nonlinear differential equations are relevant: chemical production processes, the control systems at nuclear power plants, the stabilisation of energy networks – you could even use these methods to analyse whether our energy supply network would withstand a terrorist attack. The secret of AVACS' success was to get together a team that on the one hand understood something about the applications – for instance in our example above the fact that for a car's steering system its registration number is completely irrelevant –  and on the other hand understood the necessary proof processes. 

QUESTION: And these skills are available here in Oldenburg?

DAMM: We put together a team of scientists from Oldenburg, Saarbrücken and Freiburg who contributed to the project from very diverse fields. Here in Oldenburg we have high competences in System Modeling and in the application domains, in Saarbrücken there is a lot of expertise in the field of real-time analysis methods and probabilistic verification, and our colleagues there are also very good with algorithms and logic. . Freiburg was our centre for circuit verification and the efficient representation of complex sets.    

FRAGE: That all sounds very complex. Where do you begin?

DAMM: We simply followed our intuition. It hardly makes sense that on the one hand we have constantly falling accident rates in the aviation industry while on the other hand we have these undecidability results. So first we took a look at how the experts in the industry deal with this. We have been working with Airbus for over 20 years and have detailed knowledge of their development processes. We realised that computer science theoreticians and industry specialists are worlds apart: the theoreticians want to analyse situations that aren't even possible in practice – for example an unlimited amount of information having to be coded within a finite time interval. But if you take a look at everyday practice you see that the systems are clocked, so you're not dealing with unlimited amounts of information. This is where we scientists come into play: we wrap our intuition into a formal model. That's the fun of scientific work.

QUESTION: So has AVACS solved all the problems of complex systems?

DAMM: I'll put it like this: using AVACS methods we can say how systems should be built to make them controllable. After all, nowadays systems interact with each other. I'll use the catchphrase "Internet of Things": every item has a clear name – whether it's a coffee maker or a spare part for a vehicle – and can be connected to individually on the web. This has major advanteges for industry. Logistics departments, for example, can optimise their production processes because they can keep track of everything. However, the market dynamic is so strong that for purely pragmatic reasons companies start building something and then it grows into a system that is no longer analysable. In logistics that may be okay but when it comes to safety-critical systems like autonomous cars it's simply unacceptable. We as a society are making ourselves dependent on systems that have been grown ad-hoc, and of which we no longer control the risks.

QUESTION: Now you're making me a bit scared...

DAMM: Well AVACS has shown how systems can be built in such a way that they remain controllable. And we are seeing the first positive results here: our colleagues in Saarbrücken are proud to have convinced a well-known manufacturer of semiconductors to build a generation of processors in such a way that it is analysable.

QUESTION: AVACS has now officially come to an end. Is the final report ready?

DAMM: Almost, we're in the final phase.

QUESTION: How thick is it?

DAMM: Exactly 140 pages thick, as stipulated by the German Research Foundation. It's a real challenge, squeezing twelve years of research onto so few pages. We must confine ourselves to the highlights. But fortunately those 140 pages are not all that remains of AVACS. There are many follow-up projects. Here at the University of Oldenburg we plan to put humans at the centre of several follow-up projects. So it's good that we have the medical faculty here and we're working closely with the Department of Psychology and the Department of Health Services Research. We want to try to create human models and for that we are focussing on observing brain activity. 

QUESTION: Designing human models? That sounds a bit like science fiction...

DAMM: It's not as far-fetched as it sounds. Autonomous vehicles will soon be reality. Yet humans will continue to play a key role in certain situations. Imagine you're sitting in a driverless car, leaning back in your seat watching a film. All of a sudden a tire goes flat and the lorry in front loses its cargo. The car can't cope with the situation and says: You take over. What do you need to react appropriately at that moment? What are we humans capable of cognitively in such extreme situations? Here at Oldenburg we have a fantastic opportunity to get involved, together with our medical colleagues, in building human models. That is the subject of the project "Critical Systems Engineering for Socio-Technical Systems", which originated with AVACS. And incidentally we're also planning a new collaborative research center that goes in that direction. We want to use the methods we developed in AVACS for technical systems to understand the interaction between humans and technical systems.

QUESTION: Are there other projects?

DAMM: There are several transfer projects that are building bridges with industry, for example one that deals with software verification in assistance systems. My Oldenburg colleague Martin Fränzle has developed algorithms that now secure the wheel extension mechanism in Airbus planes.   

QUESTION: So your assessment of the project is positive in every respect...

DAMM: Definitely. It's a very exciting field of research. It's relevant, it involves interdisciplinary work, it requires extensive mathematical knowledge – everything fits together perfectly. It was by no means a given that we would be able to build up a team spirit that created a scientific community stretching across three different locations. Around 80 researchers were involved. And we had an extremely pleasant work environment.

Interviewer: Birgit Bruns