Making critical systems more safe and secure by model checking
Maurice Laveaux developed several methods to improve the scalability of formal verification in large scale software systems.
Many parts of our life depend on software behaving as expected. In most cases misbehavior is only a nuisance, but in safety critical systems such as airplanes, cars or medical devices it can lead to fatal accidents. In other cases, security flaws can result in private information being leaked to the public. PhD candidate Maurice Laveaux developed several methods to ensure the correctness of larger systems more quickly. He defended his thesis on Tuesday 22 November at the department of Mathematics and Computer Science.
Model checking is a rigorous method to analyze the behavior of software by automatically verifying questions about it. The behavior is ultimately described by all possible configurations (or 'states') that the system can be in and how the system goes from one state to another. Relevant questions could be: can our software always make progress? Or, after an error has been received, will it be dealt with?
Faster verification of software
Answering these questions can require a lot of computational power due to the number of states in the complete system. This is often the result of the interaction between several components of the software. Laveaux researched different ways to accelerate this verification process.
One way to deal with the verification of a large system is by dealing with the individual component instead. First of all, Laveaux improved existing so-called refinement algorithms in the literature that determine the correctness of a component with respect to its interface one component at a time.
Splitting a large monolithic software system
Related to this idea of dealing with components, another technique was developed to split a large monolithic software system into multiple smaller components, in such way that the individual components can be reduced individually and then subsequently combined to obtain the complete behavior.
Another useful strategy for verifying large systems is to try to determine the answer eagerly. For example: to answer the question whether out software can always make progress negatively, it is sufficient to find a single state that cannot make progress. Although conceptually simple, proper techniques had to be developed to apply this correctly.
Finally, since the amount of processors available in common hardware is growing steadily, it makes sense to also develop concurrent algorithms for the verification process. To this end, Laveaux developed data structures that can be accessed concurrently to form the basis of these concurrent algorithms.
Future application in industry
All of these techniques fit within efforts to improve scalability of formal verification in large scale software systems. In the future, these efforts will allow us to ensure correctness of larger systems more quickly, which will help in the adoption of these techniques in industry. In turn, this will improve the reliability of safety critical systems by reducing the reliance on human intuition and testing, to ensure the correctness of software.
Keep following us
Experience life at our university on Instagram. With every week a different person taking over.
On our YouTube channel you find the latest videos and animations about research, education and working at TU/e.
Follow the latest TU/e updates on our Facebook page.
Be part of our community and stay up to date on everything that happens at TU/e by following us on LinkedIn.
Be the first to know the latest TU/e news via our Twitter channel.