Applying Formal Methods in Software Development

Leonard Lensink

Promotor: prof.dr. M.C.J.D. van Eekelen (RU and OU)
Copromotor: dr. S. Smetsers (RU)
Radboud Universiteit Nijmegen
Date: 6 November, 2013, 16:30

Summary

Our society is still increasingly dependent on computer systems. As a result, mistakes in these computer systems can have dire consequences: large monetary damage can occur, or human lives can be endangered. In these cases, the traditional error prevention methods are often insufficient. However, employing formal methods can help to achieve the desired safety level.

Formal methods in software engineering are mathematical techniques that are used in the design, implementation and testing of computer systems. The application of mathematical methods in the development and verification of software is very labor intensive, and thus expensive. Therefore, it is not feasible to check all the wanted properties of a complete computer program in detail. It is more cost effective to first determine what the crucial components of the software are. These parts can then be isolated and studied in detail by creating mathematical models of these sections and verifying them.

In order to reason about mathematical models, several different techniques have been developed.
In this thesis we will focus mainly on model checking and theorem proving. The first method takes a finite transition system and systematically checks whether all the desired properties hold for every state of the system. Because the number of states increases exponentially with the size of the model, this method will often have to limit itself to small variants of the system that is under investigation. An advantage of model checking is that, when it finds a problem, it can indicate how it got into an error state. This information can be used to improve the model.

The second method uses general mathematical techniques to reason about the models. This makes it possible to reason about systems of which the number states is unlimited. For this a price must be paid: the reasoning cannot occur fully automatically. By combining the strong points of model checking; automation and finding counter examples, with the more general mathematical power of theorem proving, it takes less effort to guarantee the reliability of the investigated systems.
The thread that runs through the different parts of this thesis is the software surgery methodology. This is a methodology in which critical software components are investigated, improved and verified, using the earlier mentioned formal methods. Subsequently, the verified models can be used to derive (fragments of) computer programs, that satisfy high reliability demands. These fragments can then replace the original components.

The specific contributions of this thesis are the following:

A model has been constructed in the theorem prover PVS of a smartcard personalization machine. This machine was extensively investigated using model checking techniques in the past. The earlier attempts had led to the verification of the machine’s scheduling algorithm for a limited amount of cards and personalization stations. By using PVS, the scheduling mechanism has been found to be correct for an unlimited amount of cards and an indeterminate number personalization stations.

This thesis also provides a model and an algorithm for the reentrant readers-writers protocol, that is used in, among others, the Qt toolkit. This solution is accompanied by a proof that it does not have any deadlock and starvation issues for an indeterminate amount of processes. Furthermore, in order to combine the use of the model checker Spin and the theorem prover PVS more easily a framework is presented. This framework offers a translation from the modeling language Promela, which is used by Spin, to the specification language of PVS. It also gives support in the proving process by supplying a number of generally applicable lemmas.
Finally, this thesis describes a translation that can be used to generate Java code from verified PVS models. The Java code is augmented with annotations. These can be used to verify that the generated Java code is a correct translation. The articles that describe these results contribute as a whole to combing different formal methods in order to increase the reliability of computer systems.