Distributed System Design with Message Sequence Charts

The methodical mastery of interaction scenarios is a key factor for capturing and modeling system requirements of distributed, reactive systems. Message Sequence Charts (MSCs) and variants thereof are well-accepted as a graphical description technique for interaction scenarios. MSCs emphasize the inter-component coordination aspect of typically partial system executions; this complements the usually complete behavior description for individual components, as given by state-oriented automaton specifications. The topic of this thesis is the seamless, methodically founded integration of MSCs into the development process for distributed, reactive systems. The comparison of several MSC dialects and automaton models is followed by the definition and analysis of the formal syntax and semantics for the MSC notation used in this thesis. The stream-based system model, underlying the semantics definition, enables the integrated consideration of interaction-oriented and state-oriented system specifications; it also serves as the basis for the introduction of effective refinement notions for MSCs. Next, different MSC interpretations -- in the range from scenario specification to complete behavior descriptions to the specification of unwanted behavior -- are formally defined. In addition, the application of MSCs for the description of safety and liveness properties is analyzed. Finally, two transformation procedures, supporting the transition from interaction scenarios to complete behavior specifications for individual components, are presented. The first one schematically extracts relational assumption/commitment specifications from MSCs. The second one turns MSCs syntactically into corresponding state automata. On the one hand this makes the component properties defined by MSCs accessible to formal analysis; on the other hand this constructively bridges the gap between interaction requirements and component implementations.