Why timed sequence diagrams require three-event semantics

Abstract

Abstract. STAIRS is an approach to the compositional development of sequence diagrams supporting the specification of mandatory as well as potential behavior. In order to express the necessary distinction between black-box and glass-box refinement, an extension of the semantic frame-work with three event messages is introduced. A concrete syntax is also proposed. The proposed extension is especially useful when describing time constraints. The resulting approach, referred to as Timed STAIRS, is formally underpinned by denotational trace semantics. A trace is a sequence of three kinds of events: events for transmission, reception and consumption. We argue that such traces give the necessary expressive-ness to capture the standard UML interpretation of sequence diagrams as well as the black-box interpretation found in classical formal methods. 1 Introduction to STAIRS Sequence diagrams have been used informally for several decades. The first stan-dardization of sequence diagrams came in 1992 [ITU93] – often referred to as