Composition of assumption-commitment specifications in a UNITY style

AbstractThe problem of composing assumption-commitment specifications arises in the hierarchical development of reactive or concurrent systems. Abadi and Lamport's composition principle has been proposed as a logic-independent solution to that problem. In this paper, we apply it to derive a parallel rule for UNITY-like assumption-commitment specifications. For that purpose, we first interpret UNITY formulas in Abadi and Lamport's compositional model. Then, the premises of the parallel rule are reduced to proof obligations that can be carried with rules inherited from the UNITY logic. The approach is illustrated by an example