% ------------------------------------------------------------------ %
%                                                                    %
% Datei: valid2.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 5: Validierung dynamischen         %
%                                    Systemverhaltens, Teil 2/3      %
%                                                                    %
% Version vom 17. 4.1997                                             %
% ------------------------------------------------------------------ %

\subsection{Anbindung externer Dienste}
\label{SubSec:ExternDienst}

Bei reaktiven Systemen handelt es sich stets um offene Systeme, welche in einer bidirektionalen Interaktionsbeziehung zu ihrer Systemumgebung oder einem anderen externen System stehen \cite{page91}. Daher wird es im Rahmen der Validierung des dynamischen Systemverhaltens erforderlich, die Verflechtung des Systems mit seiner Systemumgebung zu ber"ucksichtigen. So kann z.B. f"ur Ereignisse, die in der Systemumgebung auftreten und zu einer Reaktion innerhalb des zu entwerfenden Systems f"uhren, das daraus resultierende Systemverhalten nachvollzogen werden. Umgekehrt ist es m"oglich, da"s innerhalb des zu validierenden Systems Ereignisse durch Aktionen generiert werden, die zu Reaktionen innerhalb der Systemumgebung oder einem anderen externen System f"uhren.

Ein Beispiel f"ur die Verflechtung eines zu validierenden Systems mit seiner Systemumgebung stellt die Anbindung der grafischen Benutzeroberfl"ache {\sf StarView} an einen Validierungsprototypen (hier: Tycoon Prototyp {\sl TV}) innerhalb der Modellierungs- und Validierungsumgebung {\sl StatechartEnv} dar. Der externe Dienst {\sf StarView} dient hierbei zur Ausl"osung von Ereignissen innerhalb des Tycoon Validierungsprototypen und zur Aufnahme innerhalb des Prototypen generierter Aktionen an externe Systeme.

Bei {\sf StarView} handelt es sich um eine portable C++ Klassenbibliothek zur Entwicklung und Gestaltung grafischer Benutzeroberfl"achen \cite{hachmann96}. Mit Hilfe eines Tycoon {\sf StarView} \engl{Gateways} \cite{geis95} ist es m"oglich, {\sf StarView} GUI Elemente "uber TL Funktionen anzusprechen und in Tycoon Applikationen einzubinden.\\

\begin{figure}[hbt]
  \begin{center}
    \ 
    \epsfig{figure=proto1.eps,width=13cm}
  \end{center}
  \caption{\label{Fig:Prototyp1} Anbindung externer Dienste}
\end{figure}

In der Abbildung~\ref{Fig:Prototyp1} sind die Interaktionsbeziehungen zwischen einem zu validierenden System (hier: der generierte Tycoon Prototyp {\sl TV}; vgl. Abschnitt~\ref{SubSec:Prototyp}) und seiner Sy\-stem\-um\-ge\-bung "uber die ereignisausl"osende Schnittstelle einer Fernbedienung und die ereignisaufnehmende Oberfl"ache des Bildschirms in einer Abstraktion der entsprechenden {\sf StarView} GUI Elemente dargestellt. 

Das in der Abbildung~\ref{Fig:Prototyp1} abstrahiert dargestellte Ausl"osen eines globalen Ereignisses erfolgt interaktiv durch den Anwender mit einem Mausklick auf eine Taste der Fernbedienung, z.B. die Programmtaste 3. Dieses globale Ereignis l"ost innerhalb des Tycoon Validierungsprototypen {\sl TV} einen, wie in Abschnitt~\ref{Sec:Ausfuehrung} erl"autert, \engl{Macro Step} aus, welcher durch die Generierung interner Ereignisse mehrere \engl{Micro Steps} beinhalten kann und den Prototypen von einer Ausgangskonfiguration in eine stabile Folgekonfiguration "uberf"uhrt. In diesem Beispiel l"ost das Dr"ucken der Programmtaste 3 innerhalb des Tycoon Prototypen {\sl TV} durch Aktionen generierte Ereignisse an den externen {\sf StarView} Dienst aus, welche die {\sf StarView} Funktionen zum Anzeigen der Programmnummer und des entsprechenden Bildes aufrufen.

Realisiert wird die Verkn"upfung des Tycoon Validierungsprototypen mit dem externen, ereignisausl"osenden Dienst {\sf StarView} mit Hilfe der TL Funktion {\sl createRemoteControl}, welche die in Abbildung~\ref{Fig:Prototyp1} dargestellte Fernbedienung in einem eigenen Bildschirmfenster erzeugt:

\begin{xple}
     \k{let} createRemoteControl() :\k{Ok} =
       \k{begin}
         \k{let} cntrlWin = workWindow.new2(...)

         \k{let} progrButton3 = pushButton.new1(cntrlWin)
         ...
         \k{let} clickHandler() :\k{Ok} =
           \k{begin}
             ...
             tv.simulate(progrButton)
           \k{end}
         button.changeClickHdl(progrButton3 link.new(clickHandler))
         ...
         window.show(cntrlWin)
         window.show(progrButton3)
         ...
         application.execute()
       \k{end}
\end{xple}

In diesem Auszug der Funktion {\sl createRemoteControl} wird die Anbindung des Tycoon Validierungsprototypen {\sl TV} "uber die Ereignisbehandlung ({\sl clickHandler}) der Programmtaste 3 ({\sl progrButton3}) realisiert. Angebunden wird der Tycoon Prototyp an die Funktion {\sl clickHandler} mit der Funktion {\sl tv.simulate} (vgl. Anhang~\ref{Ann:ModulStatechart}), die einen \engl{Macro Step} innerhalb des an den Tycoon Bezeichner {\sl tv} gebundenen {\sl TV} Statecharts durch die "Ubergabe eines globalen Ereignisses ({\sl progrButton}) ausl"ost.

Durch den Aufruf der {\sf StarView} Ereigniskontrolle (Funktion {\sl application.execute}) innerhalb der TL Funktion {\sl createRemoteControl} werden die per Mausklick ausgel"osten Ereignisse in einem von der Ausf"uhrung des Validierungsprototypen unabh"angigen Proze"s "uberwacht. Bei einem Mausklick auf die Programmtaste 3 wird die Funktion {\sl tv.simulate(progrButton)} zur "Ubergabe des Ereignisses {\sl progrButton} an den Validierungsprototypen {\sl TV} aufgerufen (vgl. Anhang~\ref{Ann:TV}). Die Kontrolle der {\sf StarView} Ereignisse existiert als nebenl"aufiger Proze"s zur Kontrolle des Validierungsprototypen. Auf die gleiche Art k"onnten mehrere externe Dienste parallel zur Ausl"osung externer Ereignisse an einen Tycoon Prototypen angebunden werden.

Umgekehrt k"onnen beliebige TL Funktionsaufrufe an Zust"ande in der Form von Eingangs- oder Ausgangsaktionen oder an Zustands"uberg"ange in der Form von Aktionen innerhalb einer Tycoon Statechart Repr"asentation angebunden werden. Zu diesem Zweck werden an Zust"ande oder Zustands"uberg"ange im Rahmen der Modellierung des dynamischen Systemverhaltens statisch TL Funktionen als {\sl actionPart} gebunden (vgl. Abschnitt~\ref{SubSec:Aktionen}):

\begin{xple}
     ...
     \k{let} triggerDisplayProgrNr = tv.createPrimitiveEvent("{}display\_progrNr"{})
     \k{let} triggerHideProgrNr = tv.createPrimitiveEvent("{}hide\_progrNr"{})
     ...
     \k{let} actionDisplayProgrNr = tv.createAction("{}display\_progrNr"{}
       triggerDisplayProgrNr  \k{fun}() :\k{Ok} window.show(showProgrNr))
     ...
     \k{let} t14 = tv.createTransitionWithActions(hideProgrNr displayProgrNr
       triggerHideProgrNr actionDisplayProgrNr)
\end{xple}

Innerhalb des Tycoon Validierungsprototypen {\sl TV} wird als Aktionsteil die TL Funktion zum Anzeigen der Programmnummer {\sl window.show(showProgrNr)} innerhalb des daf"ur vorgesehenen {\sf StarView} Fensters an die Aktion {\sl actionDisplayProgrNr} gebunden, welche mit der Transition {\sl $t_{14}$} (entspricht dem Tycoon Bezeichner t14) zwischen den Zust"anden {\sl hideProgrNr} und {\sl displayProgrNr} assoziiert ist.

Ausgel"ost wird die Transition {\sl t14} innerhalb des Tycoon Validierungsprototypen {\sl TV} durch das Ereignis {\sl triggerHideProgrNr}, wodurch die Aktion {\sl actionDisplayProgrNr} aufgerufen wird, die das interne Ereignis {\sl triggerDisplayProgrNr} generiert und die externe Funktion {\sl window.show(showProgrNr)} aufruft. Die Transition {\sl $t_{14}$} f"uhrt somit zu einem Zustands"ubergang innerhalb des {\sl TV} Prototypen, zu einer Generierung eines internen Ereignisses (zum Ausl"osen eines \engl{Micro Steps}) und zum Aufruf einer Tycoon Funktion eines an den Prototyp angebundenen, externen Dienstes.

\section{Vorgehensweisen zur modellbasierten Verhaltensvalidierung}
\label{Sec:Vorgehen}

Grundlage der in diesem Abschnitt betrachteten modellbasierten Verhaltensvalidierung ist ein in einer Tycoon Repr"asentation vorliegendes dynamisches Modell (vgl. {\sl Television} Tycoon Statechart in Anhang~\ref{Ann:TVschnitt}). In diesem Fall ist der Tycoon Statechart explizit programmiert. Wie in Abschnitt~\ref{SubSec:Prototyp} vorgestellt, kann aber auch ein aus einem StP/OMT dynamischen Modell generierter Tycoon Validierungsprototyp Grundlage der modellbasierten Verhaltensvalidierung sein.

\subsection{Statische Validierung}
\label{SubSec:StatVal}

Im Rahmen der statischen Validierung wird untersucht, ob vom Anwender vorgegebene Systemkonfigurationen (vgl. Abschnitt~\ref{SubSec:Konfig}) vom spezifizierten System eingenommen werden k"onnen. Dabei gibt der Anwender aus seiner Sicht relevante Konfigurationen vor, die das zu erstellende System in der Realit"at einnehmen k"onnen soll.

Stellt sich eine Systemkonfiguration als nicht einnehmbar heraus, mu"s der Anwender pr"ufen, ob die von ihm vorgegebene Konfiguration in der Realit"at tats"achlich eintreten kann. Ist dieses der Fall, so mu"s die Verhaltensspezifikation des Systems im Rahmen des in Abschnitt~\ref{Sec:Einordnung} vorgestellten Validierungszyklus korrigiert werden. Die statische Validierung stellt eine Grundlage der in Abschnitt~\ref{SubSec:DynVal} vorgestellten dynamischen Validierung von Proze"sspezifikationen dar.

Beispielsweise ist eine relevante Systemkonfiguration des in Anhang~\ref{Ann:TVschnitt} spezifizierten Fernsehger"ats durch die Zust"ande {\sl Television} und {\sl Power\_Off} gegeben (vgl. Abbildung~\ref{Fig:Konf3} auf Seite~\pageref{Fig:Konf3}). Das Anlegen einer Ausgangskonfiguration zur Verhaltensvalidierung, welche die Zust"ande {\sl Television}, {\sl Power\_Off} und {\sl Power\_On} umfa"st, f"uhrt zu einem Fehler, da diese drei Zust"ande nicht in einer maximal konsistenten Beziehung zueinander stehen (vgl. Abschnitt~\ref{SubSec:Konfig}).

Die statische Validierung wird innerhalb der in Abschnitt~\ref{Sec:statechartenv} dargestellten Modellierungs- und Validierungsumgebung bei der Anlage einer Ausgangskonfiguration durch den Anwender und beim "Ubergang von einer Konfiguration in eine Folgekonfiguration im Rahmen der in Abschnitt~\ref{SubSec:DynVal} vorgestellten dynamischen Validierung durchgef"uhrt.

\subsection{Dynamische Validierung}
\label{SubSec:DynVal}

Bei der dynamischen Validierung ist die Zielsetzung, festzustellen, ob das spezifizierte Systemverhalten den Erwartungen der Anwender entspricht. Anhand von Szenarios typischer Interaktionssequenzen (vgl. Abschnitt~\ref{SubSec:Dynam}) k"onnen Proze"sspezifikationen auf ihre operationale Validit"at untersucht werden. Vorgenommen wird die dynamische Validierung entweder auf der Grundlage von spezifizierten Ereignispfaddiagrammen oder, wie in Abschnitt~\ref{SubSec:ExternDienst} dargestellt, durch das interaktive Ausl"osen von Ereignissen durch den Anwender selbst.

Ein Beispiel eines Validierungsablaufs der in Anhang~\ref{Ann:TVschnitt} spezifizierten Fernsehersteuerung ist in Tabelle~\ref{Tab:DynVal1} dargestellt.\\

\begin{table}[hbt]
\begin{center}
\begin{tabular}{|l|l|l|}
\hline
{\bf Konfiguration} & {\bf Ereignis} & {\bf Folgekonfiguration}\\
\hline\hline
{\sl Television}, {\sl Power\_Off} & {\sl power} & {\sl Television}, {\sl Power\_On}, {\sl Standby}\\
\hline
{\sl Television}, {\sl Power\_On}, {\sl Standby} & {\sl sound\_on} & {\sl Television}, {\sl Power\_On}, {\sl Standby}\\
\hline
{\sl Television}, {\sl Power\_On}, {\sl Standby} & {\sl power} & {\sl Television}, {\sl Power\_Off}\\
\hline
\end{tabular}
\end{center}
\caption{Dynamischer Validierungslauf}
\label{Tab:DynVal1}
\end{table}

Im Rahmen der in Abschnitt~\ref{Sec:statechartenv} dargestellten Tycoon Modellierungs- und Validierungsumgebung wird eine Ausgangskonfiguration, auf deren Grundlage die Validierung des spezifizierten Systemverhaltens vorgenommen werden soll, wie folgt angelegt:

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

     television.setConfiguration(stateSet)
\end{xple}

Innerhalb des in Anhang~\ref{Ann:TVschnitt} spezifizierten Tycoon Statecharts {\sl Television} werden hierbei die Zust"ande {\sl Television} (an den Tycoon Bezeichner {\sl tv} gebunden) und {\sl Power\_Off} (an den Tycoon Bezeichner {\sl powerOff} gebunden) als Zust"ande einer Konfiguration ausgezeichnet (vgl. Abbildung~\ref{Fig:Konf3}).

Daraufhin werden die externen Ereignisse, f"ur die die Proze"sspezifikation des zu entwerfenden Systems validiert werden soll, in eine Liste eingef"ugt, welche anschlie"send im Rahmen der Validierung abgearbeitet wird:

\begin{xple}
     \k{let} eventList = list.new(:television.Event)
     \k{let} eventList1 = list.cons(power eventList)
     \k{let} eventList2 = list.cons(soundOn eventList1)
     \k{let} eventList3 = list.cons(power eventList2)
\end{xple}

Die TL Ereignisliste {\sl eventList3} umfa"st in diesem Fall die externen Ereignisse {\sl power} (gebunden an den Tycoon Bezeichner {\sl power}) und {\sl sound\_on} (an den Tycoon Bezeichner {\sl soundOn} gebunden).

Ausgehend von der oben spezifizierten Ausgangskonfiguration innerhalb des {\sl Television} Tycoon Statecharts und der Ereignisliste {\sl eventList3} wird die Tycoon Spezifikation des dynamischen Systemverhaltens (an den Tycoon Bezeichner {\sl television} gebunden) ausgef"uhrt:

\begin{xple}
     television.simulate(eventList3)
\end{xple}

Das Tycoon System gibt f"ur jedes externe Ereignis die innerhalb der Proze"sspezifikation vorgenommen Zustands"uberg"ange (vgl. \engl{Micro Steps} und \engl{Macro Steps}) aus. Nach jeweils einem \engl{Macro Step} wird die stabile Folgekonfiguration angezeigt, so da"s der Anwender diese gegen seine Erwartung untersuchen kann, um gegebenenfalls "Anderungen in der Proze"sspezifikation des zu erstellenden Systems vorzunehmen.

Ersichtlich wird in Tabelle~\ref{Tab:DynVal1}, da"s ein in der Konfiguration der Zust"ande {\sl Television}, {\sl Power\_On} und {\sl Standby} nicht durchf"uhrbares Ereignis {\sl sound\_on} nicht zu einem Zustands"ubergang und einer damit verbundenen Konfigurations"anderung f"uhrt.

In Anhang~\ref{Ann:SzenVal} ist exemplarisch ein Validierungsvorgang f"ur den in Abbildung~\ref{Fig:Event} spezifizierten Ereignispfad dargestellt. Ber"ucksichtigt ist dabei ein Ausschnitt des kompletten Ereignispfads. Ereignisse zwischen den Klassen {\sl Remote-Control} und {\sl Video Recorder} und den Klassen {\sl Video Recorder} und {\sl Television} entfallen.

Auf "ahnliche Weise wird eine interaktive Simulation (vgl. Anbindung des externen Dienstes {\sf StarView} an den Tycoon Validierungsprototypen in Abschnitt~\ref{SubSec:ExternDienst}) durchgef"uhrt. Aus einem externen {\sf StarView} Ereignis wird eine Ereignisliste generiert, welche ein einziges, mit diesem {\sf StarView} Ereignis assoziiertes Ereignis der zu validierenden Proze"sspezifikation umfa"st. Dieses externe Ereignis kann daraufhin einen \engl{Macro Step} innerhalb der Spezifikation des Systemverhaltens ausl"osen. Anhand der Ausgabe der ausgel"osten Zustands"uberg"ange und der eingenommenen Folgekonfiguration hat der Anwender zu entscheiden, ob das spezifizierte Systemverhalten seiner Erwartung entspricht.

\input{valid3}
