% ------------------------------------------------------------------ %
%                                                                    %
% Datei: modell2.tex                                                 %
% Autor: Oliver Nietsch                                              %
%                                                                    %
% Universitaet Hamburg                                               %
% Fachbereich Informatik                                             %
% Arbeitsbereich DBIS                                                %
%                                                                    %
% Thema: Diplomarbeit: Die Modellierung und Validierung dynamischen  %
%                      Systemverhaltens am Beispiel von StP/OMT      %
%                      und Tycoon                                    %
%                                                                    %
% Inhalt: LaTeX-Dokument: Diplomarbeit,                              %
%                         Kapitel 4: Statecharts zur Modellierung    %
%                                    dynamischen Systemverhaltens    %
%                                                                    %
% Version vom 18. 4.1997                                             %
% ------------------------------------------------------------------ %

\section{Zustands"uberg"ange}
\label{Sec:ZuUeber}

Ein Zustands"ubergang "uberf"uhrt im einfachsten Fall \cite{huizing88} einen Zustand in einen Nachfolgezustand. Innerhalb dieser Arbeit werden Zustands"uberg"ange auf diesen einfachsten Fall eingeschr"ankt. Die semantischen Konsequenzen aus verzweigten Transitionen, die einen Quellzustand mit mehreren Nachfolgezust"anden oder mehrere Quellzust"ande mit einem Nachfolgezustand verbinden, werden hier nicht untersucht. Ein Zustands"ubergang wie z.B. die Transition {\sl $t_6$} zwischen dem Zustand {\sl Videotxt} und seinem Nachfolgezustand {\sl Display} in der verfeinerten Darstellung des Zustands {\sl Image} in Anhang~\ref{Ann:TVChart2} kann Zust"ande unterschiedlicher Hierarchieebenen verbinden.

Innerhalb der exemplarisch betrachteten Tycoon Umgebung {\sl StatechartEnv} zur Modellierung dynamischen Systemverhaltens in einer statechartad"aquaten Tycoon Repr"asentation entspricht ein Zustands"ubergang dem mit dem Datentyp {\sl State} wechselseitig rekursiven Datentyp {\sl Transition}, dessen Definition im folgenden wiedergegeben ist:

\begin{xple}
     \k{Let Rec} State $<:$\k{Ok} =
       \k{Tuple}
         ...
       \k{end}
     \k{and} States $<:$\k{Ok} = set.T(State)
     \k{and} Transition $<:$\k{Ok} =
       \k{Tuple}
         source :State
         target :State
         trigger :Events
         condition :States
         actions :Actions
       \k{end}
     \k{and} Transitions $<:$\k{Ok} = set.T(Transition)
\end{xple}

Als Attribute besitzt ein Zustands"ubergang vom Typ {\sl Transition} einen Quell- und einen Nachfolgezustand (Attribute {\sl source} und {\sl target}), eine Menge mit dem Zustands"ubergang assoziierter Ereignisse (Attribut {\sl trigger}) und eine Menge von Aktionen (Attribut {\sl actions}). Desweiteren kann ein Zustands"ubergang durch eine Bedingung (Attribut {\sl condition}) in der Form einer Zustandsmenge eingeschr"ankt werden. Diese Bedingung l"a"st einen Zustands"ubergang nur dann stattfinden, wenn die in dieser Bedingung spezifizierten Zust"ande zum Zeitpunkt des m"oglichen Zustands"ubergangs in der aktuellen Systemkonfiguration enthalten sind (vgl. Abschnitt~\ref{SubSec:Konfig}).

Innerhalb der Tycoon Modellierungsumgebung {\sl StatechartEnv} wird ein, mit Aktionen (vgl. Abschnitt~\ref{SubSec:Aktionen}) assoziierter Zustands"ubergang, mit der Funktion {\sl createTransitionWithActions} in einer Tycoon Repr"asentation angelegt:

\newpage

\begin{xple}
     \k{let} createTransitionWithActions(source, target :State
                                                 trigger :Events
                                                 actions :Actions) :Transition =
       \k{if not}(list.empty(:Event trigger))
         \k{andif not}(set.empty(:Action actions)) \k{then}
           \k{let} transition = \k{tuple} source target trigger
             newConditionSet() actions \k{end}
           set.insert(:Transition source.transitions transition)
           transition
       \k{else}
         \k{raise} argumentError \k{end}
       \k{end}
\end{xple}

Der Funktion {\sl createTransitionWithActions} werden als Parameter der Quellzustand ({\sl source}), der Nachfolgezustand ({\sl target}), eine Menge von Ereignissen ({\sl trigger}), welche die ausl"osenden Ereignisse des Zustands"ubergangs darstellen, und eine Menge mit dem Zustands"ubergang assoziierter Aktionen ({\sl actions}) "ubergeben. Als R"uckgabewert dieser Funktion enth"alt der Tycoon Anwendungsentwickler ein Objekt vom Typ {\sl Transition}. Desweiteren wird die generierte Transition in die Zustands"ubergangsmenge des Quellzustands ({\sl source.transitions}) eingef"ugt. Sollte die der Funktion {\sl createTransitionWithActions} "ubergebene Ereignisliste ({\sl trigger}) oder Aktionenmenge ({\sl actions}) keine Elemente enthalten, so wird ein Fehler ausgel"ost ({\sl \k{raise} argumentError \k{end}}), da eine korrekte Spezifikation des Zustands"ubergangs nicht erfolgen kann.

Die Schnittstellen der innerhalb der Modellierungsumgebung {\sl StatechartEnv} implementierten TL Operationen zum Generieren von Zustands"uberg"angen ohne assoziierte Aktionen ({\sl createNormalTransition}) oder mit assoziierten Bedingungen ({\sl createConditionalTransition}) etc. sind in Anhang~\ref{Ann:SchnittStatechartenv} dargestellt.

\subsection{Ereignis}
\label{SubSec:Ereignis}

Ein Ereignis l"ost einen oder mehrere Zustands"uberg"ange innerhalb eines Statecharts aus. Dabei kann in der Bezeichnung der Transition ein zusammengesetzter logischer Ausdruck der Form einer Konjunktion, Disjunktion oder Negation von Ereignissen auftreten. Innerhalb dieser Arbeit werden Ereignisse auf primitive Ereignisse, also nicht zusammengesetzte logische Ausdr"ucke, eingeschr"ankt.

Ereignisse lassen sich unterscheiden in externe und interne Ereignisse. Externe Ereignisse sind solche, die in Anlehnung an das in Abschnitt~\ref{SubSec:Dynam} dargestellte OMT Ereignispfaddiagramm, zwischen OMT Klassen eines Systems ausgetauscht werden und von au"sen auf die das Verhalten dieser OMT Klassen spezifizierenden Statecharts wirken. Interne Ereignisse werden von einer mit einer Transition assoziierten Aktion innerhalb eines Statecharts bei einem entsprechenden Zustands"ubergang generiert. Daraus resultiert, da"s diese generierten internen Ereignisse bei der Berechnung des n"achsten auszuf"uhrenden Zustands"ubergangs ber"ucksichtigt werden m"ussen. Solche durch interne Ereignisse ausgel"osten Transitionen werden als \engl{Micro Steps} bezeichnet \cite{pnueli91}. Die in einem \engl{Micro Step} ausgef"uhrte Transition kann ebenfalls interne Ereignisse generieren, die ihrerseits wiederum anderen Transitionen als Trigger dienen. Erst nach der Ausf"uhrung aller durch ein externes Ereignis generierten \engl{Micro Steps} wird beim Vorliegen eines externen Folgeereignisses die Berechnung des n"achsten auszuf"uhrenden Zustands"ubergangs durchgef"uhrt. Alle aus einem externen Ereignis resultierenden Zustands"uberg"ange (\engl{Micro Steps}) innerhalb eines Statecharts ergeben zusammen einen \engl{Macro Step} \cite{pnueli91}.

Innerhalb der Tycoon Umgebung {\sl StatechartEnv} entspricht ein Ereignis dem Datentyp {\sl Event}, dessen Definition im folgenden wiedergegeben ist:

\begin{xple}
     \k{Let Rec} Event $<:$\k{Ok} =
       \k{Tuple}
         \k{case} primitive \k{with} eventName :String
         ...
       \k{end}
     \k{and} Events $<:$\k{Ok} = list.T(Event)
\end{xple}

Als einziges Attribut besitzt ein primitives Ereignis ({\sl \k{case} primitive}) vom Typ {\sl Event} einen Bezeichner (Attribut {\sl eventName}).

Innerhalb der Tycoon Modellierungsumgebung {\sl StatechartEnv} wird ein primitives Ereignis mit der Funktion {\sl createPrimitiveEvent} in einer Tycoon Repr"asentation angelegt:

\begin{xple}
     \k{let} createPrimitiveEvent(trigger :String) :Event =
       \k{tuple\_case} primitive \k{of} Event \k{with} trigger \k{end}
\end{xple}

Der Funktion {\sl createPrimitiveEvent} wird als Parameter der Ereignisbezeichner ({\sl trigger}) "ubergeben. Als R"uckgabewert dieser Funktion erh"alt der Tycoon Anwendungsentwickler ein Objekt vom Typ {\sl Event}.

Ein Beispiel f"ur statische Bindungen der mit der TL Funktion {\sl createPrimitiveEvent} generierten Ereignisse {\sl vtxt}, {\sl sound\_on} und {\sl sound\_off} (vgl. Verfeinerung des Zustands {\sl Image} in Anhang~\ref{Ann:TVChart2}) an die Tycoon Bezeichner {\sl triggerVtxt}, {\sl triggerSoundOn} und {\sl triggerSoundOff} lautet:

\begin{xple}
     \k{let} triggerVtxt = createPrimitiveEvent("{}vtxt"{})
     \k{let} triggerSoundOn = createPrimitiveEvent("{}sound\_on"{})
     \k{let} triggerSoundOff = createPrimitiveEvent("{}sound\_off"{})
\end{xple}

\subsection{Aktion}
\label{SubSec:Aktionen}

In der Bezeichnung eines Zustands"ubergangs (vgl. Transition {\sl $t_5$} in Anhang~\ref{Ann:TVChart2}) kann eine Menge von Ereignissen spezifiziert werden, die bei der Durchf"uhrung des Zustands"ubergangs generiert werden sollen (hier: Ereignis {\sl sound\_off}). Desweiteren k"onnen Aktionen im Rahmen von Eingangs- oder Ausgangsaktionen mit Zust"anden assoziiert werden (vgl. Ausgangsaktion {\sl sound\_on} im Zustand {\sl Videotxt} in Abbildung~\ref{Fig:ChartVtxt} auf Seite~\pageref{Fig:ChartVtxt}). Diese intern generierten Ereignisse f"uhren umgehend zu Zustands"uberg"angen in der Form der in Abschnitt~\ref{SubSec:Ereignis} erl"auterten \engl{Micro Steps}.

Innerhalb der Tycoon Umgebung {\sl StatechartEnv} entspricht eine Aktion dem Datentyp {\sl Action}, dessen Definition im folgenden wiedergegeben ist:

\begin{xple}
     \k{Let} Action $<:$\k{Ok} =
       \k{Tuple}
         actionLabel :String
         trigger :Event
         \k{var} actionPart :\k{Fun}() :\k{Ok}
      \k{end}
\end{xple}

Als Attribute besitzt eine Aktion vom Typ {\sl Action} einen Bezeichner (Attribut {\sl actionLabel}), ein zu generierendes Ereignis (Attribut {\sl trigger}) und einen Aktionsteil (Attribut {\sl actionPart}), der eine parameterlose TL Funktion beinhalten kann. Detailliert wird dieser Aktionsteil in Abschnitt~\ref{SubSec:ExternDienst} bei der Anbindung externer Dienste an Zustands"uberg"ange eines Statecharts erl"autert.

Innerhalb der Tycoon Modellierungsumgebung {\sl StatechartEnv} wird eine Aktion mit der Funktion {\sl createAction} in einer Tycoon Repr"asentation angelegt:

\begin{xple}
     \k{let} createAction(actionLabel :String  triggeredEvent :Event
                            actionPart :\k{Fun}() :\k{Ok}) :Action =
       \k{tuple} actionLabel triggeredEvent \k{var} actionPart \k{end}
\end{xple}

Der Funktion {\sl createAction} werden als Parameter ein Bezeichner der Aktion ({\sl actionLabel}), das zu generierende Ereignis {\sl triggeredEvent} und der Aktionsteil {\sl actionPart} "ubergeben. Als R"uckgabewert dieser Funktion erh"alt der Tycoon Anwendungsentwickler ein Objekt vom Typ {\sl Action}.

Ein Beispiel f"ur statische Bindungen der mit der TL Funktion {\sl createAction} generierten Aktionen {\sl sound\_on} und {\sl sound\_off} (vgl. Verfeinerung des Zustands {\sl Image} in Anhang~\ref{Ann:TVChart2}) an die Tycoon Bezeichner {\sl actionSoundOn} und {\sl actionSoundOff} lautet:

\begin{xple}
     \k{let} actionSoundOn = createAction("{}sound\_on"{} triggerSoundOn \k{fun}() :\k{Ok} ok)
     \k{let} actionSoundOff = createAction("{}sound\_off"{} triggerSoundOff \k{fun}() :\k{Ok} ok)
\end{xple}

Ein komplettes Beispiel der Anbindung von Aktionen an Zust"ande oder Zustands"uberg"ange ist in Anhang~\ref{Ann:TVschnitt} enthalten.

\section{Semantik von Ausf"uhrungsschritten}
\label{Sec:Ausfuehrung}

Zustands"uberg"ange "uberf"uhren ein System von einem Zustand in einen Nachfolgezustand. Ein Ausf"uhrungsschritt "uberf"uhrt dabei ein System von einer konkreten Konfiguration in eine Folgekonfiguration, die den Systemzustand repr"asentiert. Ausgehend von einer aktuellen Konfiguration kann stets nur eine eingeschr"ankte Menge von Zustands"uberg"angen stattfinden. In Abschnitt~\ref{SubSec:Step} ist die Berechnung solch einer Menge von ausf"uhrbaren Zustands"uberg"angen erl"autert. Die in der Tycoon Umgebung {\sl StatechartEnv} exemplarisch implementierte Statechart Semantik zur Ausf"uhrung von Statecharts auf der Basis einer gegebenen Konfiguration wird in \cite{pnueli91} detailliert vorgestellt.

\subsection{Systemkonfiguration}
\label{SubSec:Konfig}

Eine Systemkonfiguration beschreibt den globalen Zustand eines Statecharts, welcher sich aus einer "uber Abstraktionsebenen hinweg betrachteten maximal konsistenten Teilmenge aller Statechartzust"ande zusammensetzt. Eine Teilmenge von Zust"anden eines Statecharts hei"st konsistent, falls f"ur alle Zustandspaare alternativ gilt:

\begin{itemize}
  \item Die Zust"ande stehen miteinander in einer Verwandtschaftsbeziehung. Zwei Zust"ande sind miteinander verwandt, falls der eine Vorfahr oder Nachkomme des anderen ist, wobei zwischen beiden Zust"anden mehrere Verfeinerungsebenen liegen k"onnen.
  \item Die Zust"ande sind orthogonal zueinander. Zwei Zust"ande sind orthogonal, falls sie nicht in einer Verwandschaftsbeziehung stehen und ihr kleinster gemeinsamer Vorfahr ein UND-Zustand ist. Der kleinste gemeinsame Vorfahr zweier Zust"ande ist der Zustand, bei dem sich die Hierarchiepfade von den Zust"anden zur Wurzel des Statecharts hin treffen \cite{fricke95}.
\end{itemize}

Eine konsistente Teilmenge \engl{X} von Zust"anden eines Statecharts hei"st maximal konsistent, falls f"ur jeden Statechartzustand \engl{s} au"serhalb dieser Teilmenge von Zust"anden gilt, da"s die Vereinigungsmenge \engl{X $\cup$  \{s\}} eine nicht konsistente Menge von Zust"anden ergibt.\\

\begin{figure}[hbt]
\noindent
\begin{minipage}{7cm}
  \begin{center}
    \ 
    \epsfig{figure=konfig3.eps,width=4cm}
  \end{center}
  \caption{\label{Fig:Konf3} Ausgangskonfiguration}
\end{minipage}
\hfill
\begin{minipage}{7cm}
  \begin{center}
    \ 
    \epsfig{figure=konfig4.eps,width=4cm}
  \end{center}
  \caption{\label{Fig:Konf4} Folgekonfiguration}
\end{minipage}
\end{figure}

In Anlehnung an das Konzept der Markierung von Bedingungen in Netzen \cite{reisig82}, kann innerhalb von Statecharts ein in einer aktuellen Systemkonfiguration enthaltener Zustand grafisch ebenfalls als markiert dargestellt werden.

In der Abbildung~\ref{Fig:Konf3} ist eine Ausgangskonfiguration als maximal konsistente Teilmenge von Zust"anden des {\sl Television} Statecharts dargestellt. Sie umfa"st die markierten Zust"ande {\sl Television} und {\sl Power\_Off}. "Ahnlich wie bei Stellen/Transitions-Netzen \cite{jessen87}, bei denen eine Transition nur schalten kann, wenn die davorliegenden Stellen entsprechend markiert sind und die Kapazit"at der dahinterliegenden Stellen durch das Schalten der Transition nicht "ubertroffen wird, kann in einem Statechart ein Zustands"ubergang nur stattfinden, wenn der entsprechende Quellzustand in der aktuellen Systemkonfiguration enthalten ist. Ausgehend von der in der Abbildung~\ref{Fig:Konf3} dargestellten Ausgangskonfiguration {\sl C = \{Television, Power\_On\}} wird beim Eintreten des Ereignisses {\sl power} die in der Abbildung~\ref{Fig:Konf4} gezeigte Folgekonfiguration erreicht, wobei die Konfiguration "uber diese Abstraktionsebene hinaus die Defaultzust"ande der weiter verfeinerten Zust"ande des Zustands {\sl Power\_On} umfa"st (vgl. Abbildung~\ref{Fig:ChartPowerOn} auf Seite~\pageref{Fig:ChartPowerOn}). Die in der Abbildung~\ref{Fig:Konf4} dargestellte Folgekonfiguration {\sl C'} beinhaltet die Zust"ande {\sl Television}, {\sl Power\_On} und {\sl Standby}.

Angelegt wird eine Ausgangskonfiguration innerhalb der Tycoon Umgebung {\sl StatechartEnv} auf der Basis des in Anhang~\ref{Ann:TVschnitt} dargestellten Tycoon {\sl Television} Statecharts mit der Funktion {\sl setConfiguration}:

\begin{xple}
     ...
     \k{let} stateSet = emptySet(:State)
     set.insert(stateSet tv)
     set.insert(stateSet powerOff)

     television.setConfiguration(stateSet)
\end{xple}

\subsection{Schrittkonstruktion}
\label{SubSec:Step}

Wie in Abschnitt~\ref{SubSec:Konfig} dargestellt, kann in einer aktuellen Konfiguration stets nur eine bestimmte Menge von Zustands"uberg"angen stattfinden. Die folgenden Bedingungen schr"anken die Menge der ausf"uhrbaren Transitionen ein \cite{day93}:

\begin{itemize}
  \item Ein Zustands"ubergang kann stattfinden, falls sich die Systemkontrolle in dem Quellzustand des Zustands"ubergangs befindet. Das bedeutet, da"s dieser Quellzustand in der aktuellen Systemkonfiguration enthalten sein mu"s. Liegt das zustands"ubergangsausl"osende Ereignis vor, so kann das System in eine Folgekonfiguration "ubergehen.
  \item Innerhalb eines ODER-Zustands kann nur ein Zustands"ubergang zu einem Zeitpunkt stattfinden.
  \item Innerhalb eines UND-Zustands k"onnen orthogonale Zustands"uberg"ange simultan innerhalb der einzelnen UND-Komponenten stattfinden.
\end{itemize}

Die Menge der ausf"uhrbaren Transitionen ist abh"angig von den externen Ereignissen und den innerhalb eines Ausf"uhrungsschritts generierten internen Ereignissen, da jede Transition, wie in Abschnitt~\ref{Sec:ZuUeber} dargestellt, zustand"ubergangsausl"osende Ereignisse durch Aktionen generieren kann, die ihrerseits wiederum zu einer Folge von Zustands"uberg"angen (\engl{Micro Steps}) f"uhren k"onnen.

Ein Ausf"uhrungsschritt (\engl{Macro Step}) ist eine maximale Folge solcher ausf"uhrbarer \engl{Micro Steps}, an deren Ende sich das System in einem stabilen Zustand befindet, in dem keine internen Ereignisse mehr generiert werden und die n"achste Systemkonfiguration erst wieder durch einen \engl{Macro Step} auf der Basis eines externen Ereignisses erreicht werden kann. Solch eine stabile Konfiguration wird als eine dauerhafte Konfiguration bezeichnet. W"ahrend der Abfolge der \engl{Micro Steps} werden keine externen Ereignisse als Trigger f"ur Zustands"uberg"ange zugelassen, die eine Konfiguration in eine Folgekonfiguration "uberf"uhren k"onnten. Diese Bedingung beruht auf der den Statecharts zugrungeliegenden Synchronit"atshypothese, die besagt, da"s ein System immer erst seine vollst"andige Reaktion auf ein externes Ereignis inklusive aller generierten internen Ereignisse durchf"uhren kann, bevor das n"achste externe Ereignis tats"achlich eintritt \cite{pnueli91}.\footnote{In der Originalformulierung der Statechartsemantik \cite{harel87} bestimmen sowohl die Menge der externen Ereignisse zu Beginn eines Ausf"uhrungsschritts als auch die Menge der in einem \engl{Macro Step} generierten internen Ereignisse die Transitionen, die zu einem Zustands"ubergang f"uhren k"onnen. Das bedeutet, da"s die Ereignisse f"ur die L"ange eines Ausf"uhrungsschrittes vorliegen, nicht aber im n"achst folgenden Schritt ber"ucksichtigt werden. Eine neue Menge externer Ereignisse mu"s vorhanden sein, um den n"achsten \engl{Macro Step} auszul"osen.}

Zur Bestimmung der Zustands"uberg"ange, die beim Vorliegen externer Ereignisse und durch Aktionen generierter interner Ereignisse ausgef"uhrt werden k"onnen, gilt f"ur die Menge aller Transitionen \engl{T}, eine die in Abschnitt~\ref{SubSec:Konfig} dargestellten Bedingungen f"ur g"ultige Systemkonfigurationen erf"ullende aktuelle Systemkonfiguration \engl{C} und eine Menge von externen Ereignissen \engl{I} eines Statecharts die Funktion \engl{En} (\engl{Enabling Function}) \cite{leveson94}:

\begin{quote}
\engl{En(T,C,I) = relevant(C) $\cap$ consistent(T) $\cap$ triggered(I $\cup$ generated(T))}
\end{quote}

Hierbei bezeichnet nach \cite{harel90}

\begin{itemize}
  \item \engl{relevant(C)} die Menge der Transitionen, deren Quellzust"ande sich in der aktuellen Konfiguration \engl{C} befinden;
  \item \engl{consistent(T)} die Menge der Transitionen aus \engl{T}, die paarweise miteinander konsistent sind;\footnote{Eine Transition ist konsistent mit sich selbst. Desweiteren sind zwei Transitionen konsistent miteinander, wenn die Arenen beider Transitionen, also der ODER-Zustand, der sowohl den Quell- als auch den Zielzustand der Transition enth"alt, zueinander orthogonal sind (vgl. Abschnitt~\ref{SubSec:Konfig}).}
  \item \engl{triggered(E)} die Menge der Zustands"uberg"ange, deren Trigger in der Menge der vorliegenden Ereignisse \engl{E} enthalten sind;
  \item \engl{generated(T)} die Menge der durch die Aktionen der Transitionen der Menge \engl{T} generierten internen Ereignisse.
\end{itemize}

Ein konkretes Beispiel zur Berechnung von Ausf"uhrungsschritten anhand der \engl{Enabling Function En} ist in \cite{pnueli91} enthalten. Im Rahmen der Implementierung der in Kapitel~\ref{Sec:statechartenv} vorgestellten Tycoon Modellierungs- und Validierungsumgebung wird innerhalb der Tycoon Umgebung {\sl StatechartEnv} die dargestellte Semantik von Ausf"uhrungsschritten als Grundlage der Funktion {\sl simulate} zur Ausf"uhrung von Statecharts benutzt (vgl. Anhang~\ref{Ann:TVschnitt}).

\clearemptydoublepage
