Abstract in English

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.

Die methodische Beherrschung von Interaktionsszenarien ist ein Schlüsselfaktor bei der Erfassung und Modellierung von Systemanforderungen für verteilte, reaktive Systeme. Message Sequence Charts (MSCs) und Varianten davon haben sich als grafische Beschreibungstechnik für Interaktionsszenarien etabliert. MSCs betonen den komponentenübergreifenden Koordinationsaspekt eines typischerweise partiellen Systemablaufs; dies ergänzt die komponentenlokale, jedoch meist vollständige Verhaltensbeschreibung, wie sie durch zustandsorientierte Automatenspezifikationen gegeben ist.

Gegenstand der vorliegenden Arbeit ist die durchgängige, methodisch fundierte Integration von MSCs in den Entwicklungsprozeß für verteilte, reaktive Systeme.

Nach einer vergleichenden Betrachtung verschiedener MSC-Dialekte und Automatenmodelle wird die formale Syntax und Semantik der in dieser Arbeit verwendeten MSC-Notation definiert und analysiert. Das der Semantikdefinition zugrundeliegende, strombasierte Systemmodell ermöglicht die integrierte Betrachtung interaktions- und zustandsorientierter Systemspezifikationen und dient als Basis für die Einführung effektiver Verfeinerungsbegriffe für MSCs. Im Anschluß daran werden unterschiedliche MSC-Interpretationen -- von der Szenarienspezifikation über die vollständige Verhaltensbeschreibung, bis hin zur Spezifikation von Fehlverhalten -- formal definiert. Zusätzlich wird die Anwendung von MSCs zur Beschreibung von Sicherheits- und Lebendigkeitseigenschaften untersucht.

Um den Übergang von Interaktionsszenarien zu vollständigen Verhaltensspezifikationen für einzelne Komponenten methodisch zu unterstützen, werden schließlich zwei Transformationsverfahren angegeben. Das erste extrahiert relationale Assumption/Commitment-Spezifikationen auf schematische Weise aus MSCs. Das zweite wandelt MSCs syntaktisch in korrespondierende Zustandsautomaten um. Dadurch werden einerseits die durch ein MSC definierten Komponenteneigenschaften einer formalen Analyse zugänglich, andererseits wird die Lücke zwischen Interaktionsanforderungen und Komponentenimplementierungen konstruktiv überbrückt.