Summary

A safety property asserts that nothing bad happens during the execution of a program and a liveness property asserts that something good eventually happens. In this chapter, we described how FSP models can be checked for both safety and liveness properties.

A safety property is defined by a deterministic process property P. This asserts that any trace including actions in the alphabet of P is accepted by P. When the property P is composed with a system S, traces of actions that are in the alphabet of S and the alphabet of P must also be valid traces of P, otherwise the ERROR state is reachable. Consequently, if safety analysis does not detect an ERROR state, we know that the property holds for the system.

We defined a subset of liveness properties which we termed progress properties. A progress property is defined by a progress set of action labels. It asserts that in any infinite execution of a system, one of the actions in the progress set must happen infinitely often. In asserting progress, it is necessary to make some scheduling assumptions as to which transitions are chosen for execution. We assume fair choice for a set of transitions such that if the set is executed infinitely often, then every transition in the set will be executed infinitely often. To investigate the liveness problems that occurred in our example programs, we introduced a way of specifying action priority that let us superimpose a specific scheduling policy on fair choice. This enabled us to model adverse situations in which processes compete for scarce resources.

The example programs developed in this chapter had a fixed set of threads competing for a resource. In Chapter 9, we examine systems in which the size of the set varies as threads are dynamically created and terminated.