Chapter 7
Selected Applications
The future is here. It's just not widely distributed yet.
—William Gibson
We have now seen a range of theories, techniques and tools based on our temporal logic, and have indicated some of the potential application areas for, and extensions of, these. Clearly we cannot hope to describe all the possible ways in which these can be applied in detail; indeed, we would not wish to do that here. Instead, this chapter consists of a little more detail concerning a selection of application areas utilizing temporal approaches. This is quite a subjective selection, reflecting areas that the author finds particularly interesting or has been closely involved with. Of course, there are many useful application areas that have not found their way into this chapter.
7.1 Model Checking Programs
In our examination of model checking we assumed that a finite state model of the program execution was available. In our practical examples, the Promela programming language provided these models. However, most programs are not written either as finite state models or as Promela programs. In spite of this the basic idea behind model checking, specifically the on-the-fly automata-theoretic approach, can be extended to the direct verification of widespread programming languages such as C and Java.
Let us recall the on-the-fly model-checking approach employed by Spin as described in Section 5.3.3. Here, the temporal property to be checked is negated and this is encoded as a Büchi ...
