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 inherent nondeterminism. Underspecification means that there are several possible behaviours serving the same overall purpose, and that it is sufficient for a computer system to perform only one of these. On the other hand, inherent nondeterminism is used to capture alternative behaviours that must all be possible for an implementation. A typical example is the tossing of a coin, where both heads and tails should be possible outcomes. In some cases, using inherent nondeterminism may also be essential for ensuring the necessary security properties of a system.
Haugen,Ø., Husa,K.E., Runde, R.K. and Stølen, K., STAIRS towards Formal Design with Sequence Diagrams, Software and Systems Modeling, 4(4):355-357,2005.
Haugen,Ø., Husa,K.E., Runde, R.K. and Stølen, K., Why Timed Sequence Diagrams Require Three-Event Semantics Published as Technical Report 309,Department of Informatics,University of Oslo,2006.
Runde, Ragnhild Kobro, How to Transform UML neg into a Useful Construct Published in Norsk Informatikkonferanse NIK’2005,pages 55–66. Tapir, 2005.
Runde, Ragnhild Kobro, Refining UML Interactions with Underspecification and Nondeterminism Published as Technical Report 325, Department of Informatics, University of Oslo, 2007.
Runde, Ragnhild Kobro, The Pragmatics of STAIRS Published in Proc.Formal Methods for Components and Objects (FMCO2005), volume 4111 of LNCS,pages 88–114. Springer, 2006.
Refsdal,A., Runde, R. K., and Stølen, K. Underspecification, Inherent Nondeterminism and Probability in Sequence Diagrams. Published in Formal Methods for Open Object-Based Distributed Systems, volume 4037 of LNCS,pages 138-155. Springer, 2006.
Runde, R. K. , Refsdal, A. and Stølen, K. Relating Computer Systems to Sequence Diagrams with Underspecification, Inherent Nondeterminism and Probabilistic Choice Part1: Underspecification and Inherent Nondeterminism Published as Technical Report 346,Department of Informatics, University of Oslo, 2007.
Runde, Ragnhild Kobro, STAIRS Case Study: The Buddy Sync System Published as Technical Report 345, Department of Informatics, University of Oslo, 2007.