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.
List of original publications
1 Atle Refsdal, Knut Eilif Husa, and Ketil Stølen. Speciﬁcation and reﬁnement of soft real-time requirements using sequence diagrams. In Proceedings of Formal Modeling and Analysis of Timed Systems (FORMATS): Third International Conference, volume 3829 of LNCS, pages 32–48. Springer, 2005.
2 Atle Refsdal, Ragnhild Kobro Runde, and Ketil Stølen. Underspeciﬁcation, inherent non-determinism and probability in sequence diagrams. In Proceedings of the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), volume 4037 of LNCS, pages 138–155. Springer, 2006.
3 Ragnhild Kobro Runde, Atle Refsdal and Ketil Stølen. Relating Computer Systems to Sequence Diagrams with Underspeciﬁcation, Inherent Nondeterminism and Probabilistic Choice – Part 1: Underspeciﬁcation and Inherent Nondeterminism. Research report no. 346, Department of Informatics, University of Oslo, 2007.
4 Atle Refsdal, Ragnhild Kobro Runde and Ketil Stølen. Relating Computer Systems to Sequence Diagrams with Underspeciﬁcation, Inherent Nondeterminism and Probabilistic Choice – Part 2: Probabilistic Choice. Research report no. 347, Department of Informatics, University of Oslo, 2008.
5 Atle Refsdal and Ketil Stølen. Extending UML Sequence Diagrams to Model Trust-Dependent Behavior with the Aim to Support Risk Analysis. In Proceedings of the 3rd International Workshop on Security and Trust Management (STM,), volume 197 of ENTCS, pages 15–29. Elsevier, 2008. Electronic Notes in Theoretical Computer Science, Vol. 197, Issue 2, 2008, Pages 15-29