Application of the composition principle to unity-like specifications

Abstract

The problem of composing mutually dependent rely-guarantee specifications arises in the hierarchical development of reactive or concurrent systems. The composition principle has been proposed as a logic-independent solution to this problem. In this paper, we apply it to Unity-like rely-guarantee specifications. For that purpose, we interpret Unity formulas in Abadi and Lamport’s compositional model. Then, the premises of the composition rule are reduced to proof obligations that can be carried out in the existing Unity proof system. The approach is illustrated by an example, the composition of mutually dependent specifications of concurrent buffers.