STAIRS: Steps To Analyze Interactions with Refinement Semantics

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.

Semantics

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.

Underspecification and inherent non-determinism

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

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

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

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 STAIRS

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.

Further reading

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.

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

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

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.

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