STAIRS — Understanding and Developing Specifications Expressed as UML Interaction Diagrams Doctoral Dissertation by

STAIRS is a method for the step-wise, compositional development of interactions in the setting of UML 2.x. UML 2.x interactions, such as sequence diagrams and interaction overview diagrams, are seen as intuitive ways of describing communication between different parts of a system, and between a system and its users. STAIRS addresses the challenges of harmonizing intuition and formal reasoning by providing a precise understanding of the partial nature of interactions, and of how this kind of incomplete specifications may be consistently refined into more complete specifications. For understanding individual interaction diagrams, STAIRS defines a denotational trace semantics for the main constructs of UML 2.x interactions. The semantic model takes into account the partiality of interactions, and the formal semantics of STAIRS is faithful to the informal semantics given in the UML 2.x standard. For developing UML 2.x interactions, STAIRS defines a number of refinement relations corresponding to basic system development steps. STAIRS also defines matching compliance relations, for relating interactions to real computer systems. An important feature of STAIRS is the distinction between underspecification and inheren