Making critical systems more safe and secure by model checking

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.

Title of PhD thesis: Accelerated Verification of Concurrent Systems. Supervisors: Tim Willemse and Jan Friso Groote.