Communicating transaction processes

Message sequence charts (MSC) have been traditionally used to depict execution scenarios in the early stages of design cycle. MSCs portray inter-process (inter-object) interactions. Synthesizing intra-process (intra-object) executable specifications from an MSC-based description is a nontrivial task. Here we present a model called communicating transaction processes (CTP) based on MSCs from which an executable specification can be extracted in a straight forward manner. Our model describes a network of communicating processes as a collection of high-level labeled transition systems, where processes interact via common action labels. Each action is a nonatomic interaction which is described by a guarded choice of MSCs. Thus our model achieves a separation of concerns: the high-level transition systems depicting intra-process control flow, while the actions in the transition system capture inter-process interaction via MSCs. We show how to extract an ordinary Petri net from a CTP model thereby leading to a standard operational semantics. We also discuss the connection of our formalism to live sequence charts, an extension of MSCs which also has an executable semantics.