Applications that never crash again
Doing your taxes, Netflixing or driving a car: more and more daily activities are supported by computer applications. It is challenging and expensive to test software thoroughly, leading to errors in most applications. PhD candidate Benjamin Lion made a mathematical framework to deal with this problem. With the framework, Lion can rule out mathematically that the interaction of software with the physical world will result in certain unforeseen errors. He will receive his doctorate the first of June.
You want to watch one of your favorite tv-shows, but without any obvious reason the application refuses to launch. Or you are playing a game on your smartphone and it suddenly crashes. Sounds familiar? Most software out there contains errors from time to time, evendough it luckily works fine most of the time.
Unforeseen errors can especially occur if software is continuously interacting with the world we live in, for example in the operating systems of self-driving cars. That is because it is hard to test software in a realistic discrete representation of the world we live in. ‘Finding a uniform way of composing physics and cyber is a challenge,’ according to PhD candidate Benjamin Lion. He designed a mathematical framework to bridge this gap, making it possible to test software more thoroughly.
Error free software
Lion’s framework can be used to mathematically prove that software does not contain errors if used in a certain physical environment. He tested the framework successfully for a hypothetical situation: ‘I used it for a parking lot with self-driving cars that I wanted to rearrange. The cars have properties, for example that they cannot be in one place at the same time. And they have batteries that should not run empty’. Given a description (your software) of the cars and the parking lot (the environment), the framework will check, based on the laws of physics, if the code contains any errors. ‘If the cars can bump into each other for example.'
Improving the testing of software with mathematical methods helps to solve this problem.
A classical way to test software for rearranging self-driving cars on a parking lot, would be to come up with possible scenarios that could result in errors. All these scenarios could be tested in a simulation, for example. But it is impossible for a programmer to think of all scenarios thatpossibly result in errors in the software. Improving the testing of software with mathematical methods helps to solve this problem.
Challenges of multiple cars
What makes Lion’s framework especially interesting is that it can be used to check if multiple cars - or multiple pieces of software - can interact without errors. ‘Every car is in another position, facing different ways. Therefore they sense different things and change actions at different moments.’ An important challenge he had to tackle was representing ‘time’. Lion: ‘In real life, time is continuous. Something can change at any moment. But a computer works in discrete steps.’ Meaning something can happen on the count of one, or two, etcetera, but not at any moment in between.
This different representation of time in the cyber environment, could lead to unforeseen errors once the software has to interact with the physical world. Cars could bump into each other if they change their actions on slightly different moments. This is what makes research in which the cyber and physical world are connected in new ways so important, according to Lion: ‘Providing new ways to understand how the theory of computability (what a machine can do) relates to theoretical physics (what nature can do), is a branch of research that can improve our understanding of how machines interact with the physical world. Consequently, we can design better cyber-physical systems.’
Text: Merel Wiersma