Chapter 13: Program Verification

Overview

Up to this point, we have taken a modeling approach to the design of concurrent programs. Models are constructed, so that we can focus on actions, interaction and concurrency before proceeding to implementation and adding the details concerned with data representation, resource usage and user interface. We use the model as a basis for program construction by identifying a mapping from model processes to Java threads and monitor objects. However, we do not demonstrate other than by testing and observation that the behavior of the implementation corresponds to the behavior predicted by the model. Essentially, we rely on a systematic translation of the model into Java to ensure that the program satisfies the same safety and progress properties as the model.

In this chapter, we address the problem of verifying implementations, using FSP and its supporting LTSA tool. In doing verification, we translate Java programs into a set of FSP processes and show that the resulting FSP implementation model satisfies the same safety and progress properties that the design model satisfied. In this way, we can show that the program is a satisfactory implementation of its design model.

Chapter 4 of the book took exactly this approach of translating a Java program into an FSP model to investigate the problem of interference. To perform verification, we need to model the Java program at the level of variables, monitor locks and condition synchronization. In Chapter 4, we showed how to model variables and monitor locks. This chapter develops a model for condition synchronization so that we can verify Java programs that use wait(), notify() and notifyAll(). This implementation model is used in verifying the bounded buffer and Readers – Writers Java programs from Chapters 5 and 7. To allow us to structure the more complex sequences of actions that arise in verification of implementations, we first introduce sequential composition of FSP processes.