Specifying Computer Systems with Probabilistic Sequence Diagrams

Abstract

Probability often plays a major role in the specification of computer systems, for a number of reasons. Probabilistic requirements are, of course, essential for specifying applications such as games of chance or probabilistic algorithms. Soft real-time requirements are probabilistic requirements that are very important when we are interested in the performance characteristics of a system. Probabilistic requirements can be used when a certain amount of undesirable behavior (such as a message getting lost in a communication medium) has to be accepted for technical or economical reasons. Probability in specifications can also be used to model the system environment, or as an abstraction from detailed criteria for making a deterministic choice. This thesis proposes a specification language that allows probabilistic requirements to be expressed at the same level as other requirements. The language is based on UML sequence diagrams. Unlike UML sequence diagrams, however, the language is given a formal (denotational) semantics, and is supported by formal definitions of refinement and system compliance. Thereby, we remove ambiguity of specifications and facilitate formal reasoning about systems before they are built, as well as verification of systems against specifications. The combination of the specification language, the refinement relations, and the compliance relations is called probabilistic STAIRS, or pSTAIRS. On top of pSTAIRS, we propose a language that allows us to model the trust of actors, the influence of this trust on the choices of action made by the actors, and the actual system behavior. When analyzing systems with respect to risk or other concerns, such information is important in cases where the critical system behavior depends on choices made by actors based on trust. UML sequence diagrams focus on communication, which is essential in most computer systems today. They seem to be easy to understand at an intuitive level, and are much used in the software industry. By basing our languages on UML sequence diagrams, we hope to reduce the obstacles to adopting the languages in practical settings.