STAIRS is an approach to stepwise and compositional development of software and system specifications using UML interaction diagrams. UML interactions are commonly expressed using sequence diagrams, communication diagrams or interaction overview diagrams and describe communication between entities (such as actors and components) by the exchange of messages between them.

Semantically a UML interaction is defined in terms of traces. A trace represents a possible execution history and comprises a partially ordered set of event occurrences, where an event is either the sending or the reception of a message by an entity. Whereas the trace semantics is only informally defined by the UML standard, STAIRS comes with a mathematically well-founded denotational semantics that complies as closely as possible with the standard. The semantics is compositional in the sense that the semantics of a composed interaction diagram can be completely determined by the semantics of its sub-diagrams and the composition operator. Some of the most common composition operators are **seq** (for sequential composition), **alt** (for specifying alternatives), **par** (for parallel composition), **loop** (for several executions of the operand), and **neg** (for specifying prohibited interactions).
To semantically distinguish between allowed and prohibited traces, the semantics is given by a pair of trace sets, one set of positive traces (describing allowed interactions) and one set of negative traces (describing prohibited interactions). Traces that are neither positive nor negative are referred to as inconclusive and are irrelevant for the interaction in question.

An important aspect of STAIRS is the expressiveness to distinguish between underspecification and inherent non-determinism. Underspecification is a feature of abstraction and means specifying several behaviors, each representing a potential alternative serving the same purpose; the fulfillment of only some of them (at least one) is acceptable for an implementation to be correct. Inherent non-determinism, on the other hand, captures execution alternatives that the implementation is required to possess. A simple example of the latter is the non-determinism between heads and tails in the specification of the game of tossing a coin.
In order to syntactically distinguish between underspecification and inherent non-determinism, STAIRS introduces the **xalt** operator. Whereas **alt** is used for capturing underspecification, the **xalt** operator (explicit alternatives) is used for capturing inherent non-determinism. The STAIRS semantics is generalized to capture this: Instead of one pair of trace sets, the semantics is given by a set of such pairs. Each pair is referred to as an interaction obligation and describes execution alternatives that the implementation must provide. The set of positive traces of each interaction obligation captures underspecification.

Refinement means to add details to an abstract specification, thereby making it more concrete and closer to implementation. Commonly, refinement involves reducing underspecification by reducing the set of positive traces in one or more interaction obligations. The notion of refinement is formally defined as a relation between two interaction diagrams, precisely capturing what it means that one diagram is a refinement of another. The STAIRS refinement relation supports stepwise, incremental development of specifications in the sense that an initial, abstract specification can be refined in any number of steps; if each step is a valid refinement, the final, most concrete specification is a valid refinement of the initial one. Refinement in STAIRS is moreover compositional in the sense that a specification can be refined by refining separate parts (sub-diagrams) independently.

Operational analysis of UML interactions is supported by means of an operational semantics for sequence diagrams. The operational semantics is a characterization of the executions of sequence diagrams and, based on this semantics, two methods for analysis of interaction specifications have been developed: Refinement verification and refinement testing. Both of these methods are supported by an analysis tool named Escalator. The operational semantics complies with the UML standard to the same extent as the STAIRS denotational semantics, and the former is proven to be sound and complete with respect to the latter.

Probabilistic STAIRS is an approach, based on STAIRS, to specify probabilistic requirements using UML interactions. Probability often plays an important role in the specification of computer systems, for example for specifying applications such as games of chance or probabilistic algorithms. Probabilistic requirements can also be used when a certain amount of undesirable behavior has to be accepted, or for specifying soft real-time constraints. Probability furthermore relates to trust, in particular in the setting of trust management, since trust is commonly defined in terms of subjective probability. Probabilistic STAIRS extends the UML sequence diagram syntax with language constructs for specifying probabilistic alternatives. The STAIRS denotational semantics is generalized to capture the interpretation of probabilities, and the notion of refinement of Probabilistic STAIRS specifications is formalized based on the semantics. The notion of compliance of systems with Probabilistic STAIRS specifications is moreover formally defined, allowing the verification of systems against specifications. Subjective STAIRS is based on Probabilistic STAIRS and allows the specification of the degree to which an actor trusts an entity with respect to a given transaction, and how this trust determines the actor's choice of action. The level of trust is specified by a subjective probability on the transaction that in turn is specified by a UML interaction.

Deontic concepts are pertaining to duty and are often expressed in terms of obligations, permissions and prohibitions. Deontic notions can be used for policy specifications, where a policy is a set of rules that describe conditional constrains on systems, often to control the management or security of systems. Deontic STAIRS is an approach to policy specification using UML sequence diagrams that extends STAIRS by introducing language constructs drawn from deontic logic. In Deontic STAIRS a policy rule consists of a trigger and a body, both specified by sequence diagrams. The trigger is a specification of the conditions under which the rule applies, and the body specifies the deontic constraints imposed by the rule. The body is of one of the modalities of obligation, prohibition and permission. Deontic STAIRS is underpinned by a denotational semantics based on the STAIRS semantics. Stepwise, compositional refinement of policy specifications is supported by a formal definition of the policy refinement relation. Deontic STAIRS furthermore formalizes the notion of policy adherence, both with respect to systems and with respect to STAIRS system specifications. Policy adherence formally defines what it means that a system (implementation) or system specification adheres to the policy rules of a policy specification.

As suggestions for further reading selected papers, technical reports and PhD theses are listed below for various results and topics related to STAIRS. Each title is linked to a PDF file for download. The following selected papers give an introduction to STAIRS, its formalization, the refinement relations, as well as the pragmatics of STAIRS. The doctoral thesis comprises much of the development of STAIRS and gives a comprehensive presentation of the underlying formalization.

- Ø. Haugen, K. E. Husa, R. K. Runde and K. Stølen. STAIRS towards formal design with sequence diagrams. Journal of Software and Systems Modeling, 22(4):349-458, 2005. (pdf - ©2005 Springer)
- R. K. Runde, Ø. Haugen and K. Stølen. Refining UML interactions with underspecification and nondeterminism. Nordic Journal of Computing, 12(2):157-188, 2005. (pdf - ©2005 Publishing Association Nordic Journal of Computing)
- R. K. Runde, Ø. Haugen and K. Stølen. The pragmatics of STAIRS. In Proc. Formal Methods for Components and Objects (FMCO'05), volume 4111 of LNCS, pp. 88-114. Springer, 2006. (pdf - ©2006 Springer)
- R. K. Runde, A. Refsdal and K. Stølen. Relating computer systems to sequence diagrams: The impact of underspecification and inherent nondeterminism. Journal of Formal Aspects of Computing, 25(2):159-187, 2013. (pdf - ©2013 Springer)
- R. K. Runde. STAIRS – Understanding and Developing Specifications Expressed as UML Interaction Diagrams. PhD thesis, Faculty of Mathematics and Natural Sciences, University of Oslo, 2007. (pdf)

The following paper and doctoral thesis present the approach to operational analysis of sequence diagram specifications.

- M. S. Lund and K. Stølen. A fully general operational semantics for UML 2.0 sequence diagrams with potential and mandatory choice. In Proc. 14th International Symposium on Formal Methods (FM'06), volume 4085 of LNCS, pp. 380-395. Springer, 2006. (pdf - ©2006 Springer)
- M. S. Lund. Operational analysis of sequence diagram specification. PhD thesis, Faculty of Mathematics and Natural Sciences, University of Oslo, 2008. (pdf)

The following papers, technical report and doctoral thesis present Probabilistic STAIRS and Subjective STAIRS.

- A. Refsdal, R. K. Runde and K. Stølen. Underspecification, inherent non-determinism and probability in sequence diagrams. In Proc. 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'06), volume 4037 of LNCS, pp. 138-155. Springer, 2006. (pdf - ©2006 Springer)
- A. Refsdal and K. Stølen. Extending UML sequence diagrams to model trust-dependent behavior with the aim to support risk analysis. Science of Computer Programming, 74(1-2):34-42, 2008. (pdf - ©2008 Elsevier)
- A. Refsdal, R. K. Runde and K. Stølen. Stepwise refinement of sequence diagrams with soft real-time requirements. Journal of computer and System Sciences, 81(7):1221-1251, 2015. (pdf - ©2015 Elsevier)
- A. Refsdal. Specifying Computer Systems with Probabilistic Sequence Diagrams. PhD thesis, Faculty of Mathematics and Natural Sciences, University of Oslo, 2008. (pdf)

The following papers and doctoral thesis present Deontic STAIRS. The second paper moreover explains how preservation of trace-set properties, such as policy adherence is supported by STAIRS.

- B. Solhaug and K. Stølen. Compositional refinement of policies in UML – Exemplified for access control. In Proc. 13th European Symposium on Research in Computer Security (ESORICS'08), volume 5283 of LNCS, pp. 300-316. Springer, 2008. (pdf - ©2008 Springer)
- F. Seehusen, B. Solhaug and K. Stølen. Adherence preserving refinement of trace-set properties in STAIRS: Exemplified for information flow properties and policies. Software and Systems Modeling, 8(1):45-65, 2009. (pdf - ©2009 Springer)
- B. Solhaug and K. Stølen. Preservation of policy adherence under refinement. International Journal of Software and Informatics, 5(1-2):139-157, 2011. (pdf - ©2011 ISACS)
- B. Solhaug. Policy Specification Using Sequence Diagrams - Applied to Trust Management. PhD thesis, Faculty of Social Sciences, University of Bergen, 2009. (pdf)

Created: September 9, 2015. Last updated: September 9, 2015.