Using Temporal Fixpoints to Compositionally Reason about Liveness

The compositional specification and verification of the behavior of concurrent processes is a challenging research area. The assumption/commitment approach has emerged as oneway to systematically achieve the desiredmodularity. However, it is generally limited to reasoning about safety propertieswhich apply throughout the execution of a system. Liveness properties involving intermittent behavior are harder to address. We investigate the use of assumptions and commitments in Interval Temporal Logic and show how to augment them with some more information for handling liveness. The proposed techniques are a continuation of our previous research on formalizing assumptions and commitments through the use of fixpoints of certain simple temporal operators. Associated with this is a generalized notion of Owicki and Gries’ proof outlines. We illustrate the approach with examples including a mutual exclusion system with time stamps.