In dieser Arbeit werden Message Sequence Charts (MSCs) unter dem Aspekt des quantitativen Zeitverhaltens betrachtet. Dazu wird eine auf Uhrenautomaten basierende Semantik von Timed High-Level MSCs (HMSCs) vorgestellt.
Hierzu werden MSCs mit Koregionen und genereller Ordnung untersucht, wobei die Kanäle keine FIFO-Semantik haben müssen. Anschließend wird die Konkatenation von MSCs so erweitert, daß verschiedene sinnvolle und die Intuition formalisierende Semantiken (synchrone, asynchrone Konkatenation, Erweiterung von Koregionen über MSC-Grenzen hinaus) ausgedrückt werden können. Für dir Spezifikation des Zeitverhaltens werden Einschränkungen an das Auseinanderliegen verschiedener Ereignisse, Dauer von lokalen Aktionen und Timer im Sinne des MSC-Standards unterstützt.
Kern der Arbeit ist eine robuste Übersetzung von HMSCs in diskrete Automaten. Dabei wird, aufbauend auf Vorarbeiten zur Regularität der diskreten HMSC-Semantik, ein Kriterium entwickelt, welches für die Übersetzbarkeit hinreichend ist. Die Übersetzung ist robust in dem Sinne, daß sowohl eine Erweiterung der Semantik von HMSCs um das quantitative zeitliche Verhalten als auch die Benutzung von Life Sequence Charts (LSCs) (MSCs, bei denen nicht jedes Ereignis stattfinden muß) statt MSCs nur geringe und leicht nachvollziehbare technische Änderungen und Erweiterungen der Übersetzung erfordern. Bezüglich des Zeitverhaltens werden verschiedene intuitive Semantiken formalisiert.
Sowohl die diskreten Automaten als auch die Uhrenautomaten lassen sich dabei für weitere Untersuchungen benutzen, etwa über Veränderungen der Semantik von (Timed) HMSCs bei Änderung des unterliegenden tatsächlichen Kommunikationsmediums (z. B. Kanalbeschränkungen) oder zur Verifikation eines Systems gegenüber geeigneten Logiken.
@mastersthesis(Lucas-Diplom,
author={Philipp Lucas},
title={Analyse von Message Sequence Charts (German)},
school={RWTH~Aachen},
type={Diplomarbeit},
month={February},
year=2002
)
Valid XHTML 1.0 Strict, valid CSS.
Autor: Philipp Lucas.