\documentstyle[11pt,german]{article}
%\input{../tex/trendsstyle}

\begin{document}


\twocolumn[{\vspace*{-5mm}
\huge\sf Dissertationen
\\[4mm]
}]

\tolerance=300
\baselineskip11.5pt


\newcommand{\xxxxxx}[4]{
% Name, Titel, Anschrift, restliche items
   \noindent
   {\large \bf #1: \baselineskip15pt #2 \par}
      % hier mu"s Absatzende rein!}
   
   \medskip
   \begin{description}
   \item[Anschrift:] #3
   #4
   \end{description}
   
   \paragraph{Zusammenfassung:}
}


\pagebreak\xxxxxx
{Christian Facchi}
{Methodik zur formalen Spezifikation des
   ISO/ OSI Schich\-ten\-mo\-dells
}
{Fakult"at f"ur Informatik, Lehrstuhl
  Prof. Dr. M. Broy, 80290 M"unchen}
{\item[1. Gutachter:] Prof. Dr. M. Broy
\item[2. Gutachter:] Prof. Dr. E. Jessen
\item[Datum des Rigorosums:] 14.06.1995
}


Die Standardisierungseinrichtung ISO hat mit dem ISO/OSI
Schichtenmodell eine Grundlage f"ur die Kommunikation in
heterogenen Rechensystemen festgelegt. Eine
Modularisierung erfolgt hierbei nach verschiedenen
Aufgaben in sieben Schichten, wobei die Festlegung der
schichtenspezifischen Aufgaben in den ein\-zel\-nen
Nor\-men in gr"o"stenteils textueller Form vorliegt.  Da
in\-for\-mel\-le De\-fi\-ni\-tionen unter anderen
Nachteilen den der m"oglichen Mi"s\-in\-ter\-pre\-ta\-tion
be\-sit\-zen, wird in dieser Dissertation eine Methodik
zur formalen Spezifikation des ISO /OSI Schichtenmodells
vorgestellt, mit der die Dienst"-erbringer aller Schichten
beschreibbar sind. Mit dieser Methodik wird, im
Ge\-gen\-satz zu bisherigen Arbeiten, durch den Einsatz
eines Mo\-du\-lari\-sierungs\-kon\-zepts bei der
Spezifikation ein hoher Wie\-der\-ver\-wen\-dungs\-grad
erreicht. Dazu wird jeweils f"ur mehrere der in den Normen
verwendeten Be\-schrei\-bungs\-tech\-ni\-ken eine
eigenst"andige for\-ma\-le Se\-man\-tik angegeben, die
selbstverst"andlich auch au"serhalb des ISO/OSI
Schich\-ten\-modells anwendbar ist. So wird unter anderem
erstmalig eine formale Semantik f"ur die weit verbreiteten
Time Sequence Diagrams beschrieben.

Durch die Entwicklung der formalen Semantik f"ur die in
den Normen verwendeten Beschreibungstechniken werden mit
dieser Arbeit einige Ungenauigkeiten bei den Normen belegt
und L"osungsvorschl"age zur Behebung angeboten.

Die in den bisherigen Verfahren verwendeten An\-s"at\-ze
schr"anken das Verhalten der Dienstbenutzer, die kein
Spezifikationsgegenstand der schichtenspezifischen Normen
sind, ein. Die in dieser Ar\-beit ent\-wickel\-te formale
Semantik l"a"st dagegen ein freies Verhalten der
Dienst\-be\-nut\-zer zu. Somit wird ausschlie"slich das
Verhalten des Diensterbringers, der die zu
implementierende Komponente darstellt, formal spezifiziert.


Aufbauend auf den formalen Semantiken werden die
Be\-zie\-hun\-gen zwi\-schen den einzelnen
Beschrei\-bungs\-techniken untersucht. Dabei wird die
un\-ter\-schied\-liche Ausdrucksst"arke der zuvor
betrachteten Be\-schrei\-bungs\-tech\-ni\-ken festgestellt.




\pagebreak\xxxxxx
{Rudolf Hettler}
{Entity / Relationship-Datenmodellierung ~ in ~
  axiomatischen Spe\-zi\-fi\-ka\-tions\-spra\-chen}
{Fakult"at f"ur Informatik, Lehrstuhl Prof. Dr. M. Broy,
  80290 M"unchen}
{\item[1. Gutachter:] Prof. Dr. M. Broy
  \item[2. Gutachter:] Prof. Dr. B. Mitschang
  \item[Datum des Rigorosums:] 26.06.1995
}


Die Arbeit integriert die
Technik der Entity/Relation\-ship-Datenmodellierung mit
der axiomatischen Spezifikationstechnik {\sc Spectrum}.
Dies geschieht durch die formale Definition der Semantik
des E/R-Modells in der Spezifikationssprache {\sc
Spectrum}. Dazu wird eine Vorschrift angegeben, die ein
E/R-Schema in eine {\sc Spectrum}-Spezifikation
"ubersetzt, welche den durch das Schema beschriebenen
Datenbestand repr"asentiert. In der Folge wird untersucht,
welche Vorteile sich aus dieser Integration f"ur beide
Techniken ergeben.

Auf der einen Seite ergibt sich die M"oglichkeit, das
E/R-Modell als Technik zur Datenmodellierung in die
formale Softwareentwicklung mit {\sc Spec\-trum} zu
integrieren. Dazu wird die angegebene
"Uber\-set\-zungs\-vor\-schrift so weiterentwickelt, da"s
einem E/R-Schema eine Spe\-zi\-fi\-ka\-tion
zu\-ge\-ord\-net wird, die zur weiteren
Softwareentwicklung prag\-ma\-tisch einsetzbar ist. Damit
wird eine Schw"ache der Sprache {\sc Spectrum} behoben,
die sich wie alle auf algebraischen
Spezifikationstechniken basierenden Ans"atze besser zur
Beschreibung algorithmisch komplexer als stark
daten"-orientierter Systeme eignet. Bei der
Weiterentwicklung wird die formale Beziehung zwischen den
durch die verschiedenen "Uber\-setzungs\-vor\-schrif\-ten
generierten Spezifikationen klar heraus\-ge\-ar\-bei\-tet.

Auf der anderen Seite wird die in der Welt der formalen
Soft\-ware\-ent\-wick\-lung vorhandene Idee der
schrittweisen Verfeinerung von Spe\-zi\-fi\-ka\-tionen in
die Welt der E/R-Datenmodel\-lierung "ubertragen. Die
Arbeit un\-ter\-sucht, welche (informell definierten)
Beziehungen zwischen Schemata in der Welt der
E/R-Datenmodellierung Verwendung finden und wie sie sich
zu den in {\sc Spectrum} bekannten Beziehungen zwischen
Spe\-zi\-fi\-ka\-tionen verhalten. Insbesondere wird ein
in der Literatur in\-for\-mell gegebener Satz von
Transformationsregeln zur Entwicklung von E/R-Sche\-ma\-ta
auf seine Vertr"aglichkeit mit dem in {\sc Spectrum}
definierten Begriff der Realisierungsbeziehung zwischen
Spezifikationen untersucht.  Darauf aufbauend wird ein mit
dem {\sc Spectrum}-Re\-a\-li\-sie\-rungs\-be\-griff
vertr"aglicher Entwicklungsbegriff f"ur E/R-Sche\-mata
definiert. Mit Hilfe dieses Entwicklungsbegriffs wird eine
Technik zur Integration verschiedener Schemata ({\em View
Integration\/}) angegeben, die mit {\sc Spectrum}
vertr"aglich ist.




\pagebreak\xxxxxx
{Wilhelm Hasselbring}
{Prototyping Parallel Algorithms in a
   Set-Ori\-ent\-ed Language}
{Universit"at Dortmund, Lehr\-stuhl In\-for\-ma\-tik 10
   (Software-Tech"-nologie)}
{\item[1. Gutachter:] Prof.\ Dr.\ Ernst-Erich Doberkat
   (Universit"at Dortmund)
 \item[2. Gutachter:] Prof.\ Dr.\ Franz Stetter
   (Universit"at Mannheim)
 \item[Datum der Pr"ufung:] 3.2.1994
}

Parallele Programmierung ist
konzeptionell schwie\-ri\-ger durchzuf"uhren und zu
verstehen als die sequentielle Programmierung, weil sich
ein Programmierer bei der parallelen Programmierung oft
gleich\-zei\-tig auf mehrere Prozesse konzentrieren mu"s.
Im Rahmen dieser Arbeit wurde ein Ansatz zum Prototyping
paralleler Algorithmen in der mengen-orientierten Sprache
ProSet entworfen und implementiert. Das Ziel dieses
Ansatzes ist es, das Prototyping von parallelen
Algorithmen durch die Be\-reit\-stel\-lung von Konstrukten
mit hohem Niveau zur expliziten
Pa\-rallel\-pro\-gram\-mierung zu erleichtern.

In ProSet wird das Konzept der Proze"skreation durch
Multilisp's Futures auf die mengen-orientierte
Programmierung zugeschnitten und mit dem Kon\-zept zur
Koordination durch Linda's Tupelr"aume kombiniert. Linda
ist eine Koordinationssprache, die ein flexibles Konzept
zur Synchronisation und Kommunikation durch sogenannte
Tupelr"aume bietet. Diese Tupelr"aume sind virtuelle
gemeinsame Datenr"aume, "uber die die Prozesse
kommunizieren.  Synchronisation und Kommunikation erfolgen
in ProSet-Linda durch das Einf"ugen, Entfernen, Lesen und
durch unteilbares "Andern von einzelnen Tupeln im
Tupelraum.

Der pr"asentierte Ansatz zum Entwurf und zur
Implementation von ProSet-Linda basiert auf dem Einsatz
der formalen Spezifikationssprache Object-Z und der
Prototyping-Sprache ProSet selbst.

(Erschienen im Verlag Dr.\ Kova$\check{\mbox{c}}$,
Hamburg, 1994, ISBN 3-86064-202-2)
\\[10mm]



\xxxxxx
{Dieter Nazareth}
{A Polymorphic Sort System for Axiomatic
   Specification Languages}
{Fakult"at f"ur Informatik, Lehrstuhl Prof. Dr. M. Broy,
  80290 M"unchen}
{\item[1. Gutachter:] Univ-Prof. T. Nipkow, Ph.D.
   \item[2. Gutachter:] Univ-Prof. Dr. M. Broy
   \item[Datum des Rigorosums:] 18.05.1995
}


Die Dissertation stellt ein neuartiges polymorphes
Sor\-ten\-system f"ur axioma\-ti\-sche
Spezifikationssprachen vor. Das Sor\-ten\-system selbst
kann durch eine eigene Spe\-zi\-fi\-kationssprache
dy\-na\-misch spezifiziert wer\-den. Dieser Ansatz
erm"oglicht ein flexibles Sor\-ten\-sys\-tem, das
dynamisch an unt\-er\-schied\-liche Anwendungsgebiete
angepa{\ss}t wer\-den kann.  Ins\-be\-son\-de\-re erlaubt
dieses Sortensystem un\-ter\-schied\-liche
Po\-ly\-mor\-phie\-kon\-zep\-te zu modellieren.  Die
Arbeit untersucht die syn\-tak\-tische und semantische
Behandlung von axiomatischen
Spe\-zi\-fi\-kations\-spra\-chen basierend auf einem
derartigen Sortenkonzept.

Das Sortensystem basiert auf dem Konzept der
eingeschr"ankten Sorten.  Es erlaubt mit Hilfe von
Sortenvariablen von konkreten Sorten zu abstrahieren und
die Sortenvariablen dann durch Sortenpr"adikate
ein\-zu\-schr"an\-ken.  Die verwendete
Spezifikationssprache gliedert sich in zwei Ebenen. Die
Beschreibung der Funktionen auf der Termebene basiert auf
einer klassischen Pr"adikatenlogik 1.\ Stufe. Sie erlaubt
die Verwendung von polymorphen Bezeichnern und die
Deklaration von unsortierten Varia\-blen. Die
Eigenschaften der Sortenpr"adikate werden mit Hilfe einer
eigenen Spezifikationssprache basierend auf Horn-Klauseln
beschrieben.

Um die Wohlsortiertheit von Spezifikationen zu
"uber\-pr"u\-fen, wird ein Sorteninferenzkalk"ul angegeben.
Dieser Kalk"ul berechnet da\-r"u\-ber\-hin\-aus die
Instantiierung von polymorphen Bezeichnern sowie die
Sor\-tie\-rung von unsortiert deklarierten Variablen.
Dabei kann es zu einer Spe\-zi\-fi\-ka\-tion mehrere
Herleitungen geben. Ein erster Modellbegriff wird
des\-halb unter Betrachtung aller m"oglichen
Sortenherleitungen definiert.  An\-schlie{\ss}end werden
die semantischen Beziehungen zwischen unterschiedlichen
Sor\-ten\-her\-lei\-tungen einer Spezifikation untersucht.
Es wird gezeigt, da{\ss} syntaktisch all\-ge\-mei\-nere
Herleitungen weniger Modelle besitzen. Dieses Ergebnis
erlaubt uns einen "aquivalenten Modellbegriff zu
definieren der nur auf einer all\-ge\-meinsten
Sor\-ten\-her\-lei\-tung einer Spezifikation basiert.

Abschlie{\ss}end wird die Implementierbarkeit des
Sor\-ten\-in\-fe\-renz\-kal\-k"uls untersucht. Es wird
ein Inferenzalgorithmus vorgestellt, der sich in zwei
Abschnitte gliedert. Im ersten Abschnitt wird die
Wohl\-ge\-formt\-heit der Spezifikation untersucht und es
werden die dazu notwendigen
Sor\-ten\-pr"a\-di\-kat\-be\-schr"an\-kun\-gen berechnet.
Dar"uberhinaus wird eine all\-ge\-meinste
Sortenherleitung f"ur die Spezifikation berechnet. Im
zwei\-ten Abschnitt werden dann mit Hilfe eines
Resolutionsverfahrens die be\-rech\-ne\-ten
Beschr"ankungen gegen"uber der Sortenspezifikation als
kor\-rekt bewiesen. Es wird gezeigt, da{\ss} der
Inferenzalgorithmus korrekt und vollst"andig ist
gegen"uber dem Sorteninferenz\-kal\-k"ul.

Der Sorteninferenzalgorithmus terminiert im allgemeinen
nur f"ur wohl\-sor\-tier\-te Spezifikationen, da das
Problem f"ur allgemeine Sor\-ten\-spe\-zi\-fi\-ka\-tionen
lediglich semientscheidbar ist. Modelliert man jedoch
spe\-ziel\-le Poly\-mor\-phie\-kon\-zep\-te, wie
beispielsweise das Sorten\-klassen\-kon\-zept von Haskell,
dann wird das Problem entscheidbar und der angegebene
Sor\-ten\-in\-ferenz\-al\-go\-rith\-mus terminiert f"ur
alle Spezifikationen.

\end{document}
