Software model checking: extracting verification models from source code

To formally verify a large software application, the standard method is to invest a considerable amount of time and expertise into the manual construction of an abstract model, which is then analysed for its properties by either a mechanized or a human prover. There are two problems with this approach. The first problem is that this verification method can be no more reliable than the humans that perform the manual steps. If the average rate of error for human work is a function of the problem size, this holds not only for the construction of the original application, but also for the construction of the model. The standard verification trajectory therefore tends to become less reliable for larger applications. The second problem is one of timing and relevance. Software applications built by teams of programmers can change rapidly, often daily. Manually constructing an accurate abstraction of any one version of the application, though, can take weeks, which may jeopardize the validity of the results. In this paper a different verification method that avoids these problems is discussed. This method, which may be the precursor of a new class of testing techniques, was originally developed to allow for a thorough testing of parts of the software of a new commercial telephone switch. Here it is argued, though, that the method also has broad applicability to distributed software systems design in general.