Multiple Synchrony in MSC

We propose an extension to Message Sequence Charts (MSC); MSC diagrams comprise processes (called instances) and messages. Messages in MSC are either asynchronous or method calls. Our extension adds multiple synchronous messages. We present a transformation algorithm that takes as input a diagram in the extended MSC and generates an equivalent one in the standard MSC. The synchronous messages are transformed to the standard notation via the introduction of several control messages. We also define a semantics for MSC (both the standard and our extension) using the process algebra CSP. Both instances and messages in MSC are characterised as CSP processes. This semantics allows us to formally establish the equivalence between an extended MSC diagram and its corresponding standard diagram (generated by the transformation algorithm). Although our strategy is application independent, the motivation came from an attempt to generate test scripts from MSC diagrams describing the behaviour of mobile phone devices