Chitra Hapsari Ayuningtyas

 

Probabilistic Message Sequence Charts

 

Abstract:

This thesis deals with probabilistic extensions of MSCs and MSGs.
Probabilistic MSCs (pMSCs) are defined using probabilistic lossy channel
systems where a probability of message loss is specified for every
channel such that a message sent using this channel can be lost with the
specified probability. We provide semantics of the model in terms of
partial ordered sets (posets) and show how to compute probabilities of
possible scenarios defined by the posets.

We define probabilistic MSGs (pMSGs) as a means to combine a set of
pMSCs by enabling both probabilistic and nondeterministic system
behavior to be specified using the model. We first provide a
concatenation operator to combine a set of pMSCs then discuss about the
syntax and semantics of pMSG. We present an Asynchronous Leader Election
Protocol as a case study and show how this protocol can be specified
using our models.

We also provide a logic to reason about properties of pMSCs. Our logic
is an extension of Propositional Dynamic Logic (PDL) for message-passing
systems. We extend PDL by adding probabilistic operators and modify its
semantics in order to make it suitable with the partial order semantics
of pMSCs.