When you are driving a car, you expect the software hidden under the dashboard to function properly. If a bug in the software suddenly causes the brakes to malfunction, you are in big trouble. Alfons Laarman studies how we can efficiently guarantee that software is free from errors, an issue that requires specific attention when lives depend on it.
Preventing errors in critical systems
Nowadays, software can be found in just about any electronic device. It has extended its reach beyond computers to things like cars, mobile phones and even vacuum cleaners. Software is all around us, which means that it is even more important to make sure that it does not contain any errors, or “bugs”. While a bug might not be that much of a problem when it occurs in an app on your phone, this changes quickly if it occurs in a more important system – such as the braking system in your car.
Software is becoming increasingly complex, which increases the risk of errors. ‘If many people are involved in developing a piece of software, as is almost always the case, it is practically guaranteed that errors will pop up somewhere’, says Laarman. He recalls an incident at the European Space Agency. Developers failed to adjust their software to a new, more powerful engine they installed. The software needed to track how much lift the engine was producing. However, it only had a limited amount of storage space. The new engine produced so much lift, that the software reached its storage ceiling and began counting from zero again. ‘This made the software think the rocket was falling back to Earth, triggering a self-destruct sequence in order to prevent a potentially deadly rendezvous with the Earth’s surface.’
Laarman studies how we can systematically check software and find all errors that may cause an app on your phone to crash, the brakes of your car to malfunction, or a multimillion-euro rocket to explode and plummet back to Earth. This is done through a process called “model checking”. This involves a specific type of software - a model checker - that scans every state a piece of software might be in. For all these states the model checker verifies if the software performs the way it is supposed to. This is exceedingly difficult as more and more complex software can be in an increasing number of different states. That is why Laarman tries to come up with ways to make model checkers work as efficiently as possible.
The techniques used by Laarman to increase the efficiency of his model checkers may have some unexpected applications in seemingly unrelated research fields. The techniques may benefit large research projects such as XENON1T in Italy, where scientist are trying to find signs for the existence of dark matter. Projects performed at CERN in Switzerland, where scientist use a giant particle collider to study the elemental particles that make up regular matter, could also benefit. ‘We use techniques to limit the number of states that we have to go through individually with our model checking software’, says Laarman. ‘These large research projects could potentially use the same techniques to more efficiently store the incredible amount of data they produce, which already takes hundreds of petabytes in storage capacity.’
In the end, both individual users and companies just want one thing: for their software to be reliable. This is why Laarman’s ultimate goal is to create a framework that supports the development and implementation of any kind of software from A to Z. There have been many instances in the past where such a framework could have been extremely useful. Around the year 2010, Toyota had to recall around 10 million vehicles when software issues – that affected inter alia the braking system – caused multiple accidents and even victims. ‘This is what we are trying to prevent’, says Laarman. ‘What we want is some kind of certificate that shows consumers, companies and governments alike: this software will do exactly what it is supposed to do.’
Alfons Laarman (Zevenaar, 1983) is an assistant professor (tenure track) at the Leiden Institute of Advanced Computer Science. His PhD research at the University of Twente revolved around the parallelisation of model checking. Notwithstanding his excellent knowledge of software, even Laarman can become annoyed when a computer programme does not do what he wants it to do – just like less digitally educated people.