Rely-Guarantee Interpretation of Sequence Diagrams

The term “rely/guarantee” was coined by Cliff Jones in his influential PhD-thesis from 1981. Compositional specification of concurrent systems requires a rely/guarantee approach. This paper suggests a rely-guarantee interpretation of sequence diagrams. In the general case, sequence diagrams are represented by sets of trace sets. Each trace set corresponds to a scenario that must be reflected by the specified component. The semantics is compositional and supported by a notion of refinement. The parallel operator is shown to be monotonic with respect to refinement.