Search
Close this search box.

21 February 2022

Meet Christian Schilling, who has come to Denmark to build software that can check other software for errors

Today we have cyber-physical software systems everywhere in our society, from thermostats to intelligent traffic management and water supply systems. It is therefore crucial to develop verification software that can check these programs for errors before they are put into operation.  

Christian Schilling from Germany is interested in formal verification and modeling and has come to Aalborg University to be part of the DEIS group. He is also part of the DIREC project Verifiable and safe AI for Autonomous Systems and explains how research in cyber-physical systems makes a difference for companies and society.

Can you tell a bit about your background and why you ended up in Denmark as a computer scientist?

I did my PhD at a German university (Freiburg) and was a postdoc at an Austrian research institute (IST Austria). Now I am a tenure-track Assistant Professor at Aalborg University. The DEIS group at Aalborg University has an international reputation and is a great fit for my interests. It is productive to work with people who “speak my language.” At the same time I can develop my own independent research directions.

What are you researching and what do you expect to get out of your research?

Broadly speaking, I am interested in the algorithmic analysis of systems. More precisely, I work on cyber-physical systems, which are systems consisting of a mix of digital (cyber) and analog (physical) components. Nowadays these systems are everywhere, from thermostats to aircraft. I want to answer the fundamental question of safety: Can a system end up in an error? My analysis is based on mathematical models, and I also work on the construction of such models from observational data.

We look at models of systems and then we try to find behaviors of that system and it might not be what you want. Or if you don’t find any errors you can get a mathematical proof that your model is correct. Of course you could make mistakes with the wiring when you implement the models in a practical system, we cannot cover that. That’s why there are still more practical aspects of our work.

What are the scientific challenges and perspectives in your project?

One of the grand challenges is to find approaches that scale to industrial systems, which are often large and complex. In full generality this goal cannot be achieved, so researchers focus on identifying a structure in practical systems that still allows us to analyze the system. The challenge is to find that structure and develop techniques that exploit this challenge.

Another recent relevant trend is the rise of artificial intelligence and how it can be safely integrated into systems without causing problems. Think about autonomous systems like vacuum cleaners, lawn mowers, and of course self-driving cars in the near future. 

It is certainly a challenge to analyze and verify systems that involve AI, because the way AI is used these days is really more like a black box where nobody understands what happens. It is very difficult to say that a self-driving car under no circumstance will kill a person. 

To make this kind of analysis you need a model, and of course you could say that an engineer could build this model, but at a certain size it becomes too complex and very difficult to do. So you want an automatic technique to do that. 

Another challenge is to go from academic models to real world systems, because usually you do some simplifications which you have to take into consideration and solve when you implement the models. 

How can your research make a difference for companies and communities?

Engineers design and build systems. Typically, they first develop a model and analyze that model. My research directly addresses this phase and helps engineers learn about the behavior only given a model. This means that they do not need to build a prototype to understand the system. This saves cost in the design phase, as changing a model is cheap but changing a prototype is expensive. On the level of a model you can actually have mathematical correctness guarantees. This is something you cannot achieve in the real world.

The DEIS group has a lot of industry collaboration, but so far I’ve been working with academic modeling. With these verification models you can make sure that intelligent traffic systems work as they should.