Revisiting Safe Realizability of Message Sequence Charts Specifications

Safe realizability of Message Sequence Charts (MSCs) specifications is a measure of whether or not there exists a distributed implementation of the specification such that it is deadlock free and shows exactly the behaviours specified in the specification. There are also some works that given a specification, can answer whether it is safely realizable or not. However, while these works are restricted by certain assumptions such as synchronous message passing in the system, they also cannot answer why given two specifications, one is safely realizable and the other is not. In this paper, we present a property of MSC specifications that explains implementation problems for them. Using this result, we show how we can effectively correct a specification to avoid implementation problems such as deadlocks and implied scenarios.