Summary

This chapter has presented a way of verifying that Java implementations satisfy the same safety and progress properties as the design models from which they were developed. The approach is to translate the Java program into a detailed FSP model that captures all aspects of the Java synchronization mechanisms – in particular, monitor locks and notification. This implementation model is then analyzed with respect to the same safety and progress properties used in analyzing the design model. We also showed in the bounded buffer example that the design model itself can be used as a safety property when verifying the implementation model.

Implementation models are considerably more detailed than design models and as such generate much larger state spaces during analysis. It is in general only possible to analyze small parts of an implementation. This is why in the book we have advocated a model-based design approach in which properties are investigated with respect to a design model and then this model is used as a basis for program implementation. Clearly, as we have demonstrated in the examples contained in this chapter, errors can be introduced in going from design model to implementation. Interestingly, the two bugs discovered both arise from the use of notify() in place of notifyAll(). Perhaps the most important lesson from this supplement is that strict attention must be paid to the rule that notify() should only be used if at most one thread can benefit from the change of state being signaled and it can be guaranteed that the notification will go to a thread that is waiting for that particular state change in the monitor class itself or in any subclasses.

Finally, as illustrated in the implementation models, sequential composition can be seen to provide a convenient means for structuring complex sequences of actions from simpler fragments of sequential processes.