Entwicklung korrekter Systeme

Spezifikation von Daten und Prozessen

Stammvorlesung

Auf dieser Seite

 
 

zum Seitenanfang

Inhalt

In dieser Vorlesung stehen zwei Spezifikationssprachen im Mittelpunkt, die Anfang der 80er Jahre in der berühmten Programming Research Group an der Universität Oxford entwickelt wurden und seitdem weite Beachtung und Verbreitung gefunden haben: Z und CSP.

Z eignet sich gut für die Beschreibung von sequentiellen Systemen, die durch Zustandsräume und deren Veränderungen gekennzeichnet sind. Z-Spezifikationen benutzen Notationen aus der Logik und Mengentheorie und werden durch den sogenannten Schema-Kalkül strukturiert. Dadurch lassen sich große Systeme in kleinen übersichtlichen Teilen beschreiben und der Zusammenhang dieser Teile durch die Schema-Operatoren darstellen. Außerdem kann die formale Beschreibung mit erklärendem Text vermischt werden. Solche Spezifikationsdokumente können also gut lesbar und trotzdem formal gestaltet werden. Aus diesem Grund wird Z auch im Bereich des Software-Engineerings beachtet.

CSP (Communicating Sequential Processes) eignet sich gut für die Beschreibung von reaktiven Systemen, die aus mehreren Komponenten bestehen, die unabhängig voneinander arbeiten und gelegentlich miteinander kommunizieren. CSP besitzt ein klares semantisches Modell, daß Konzepte wie Kommunikation, Nichtdeterminismus, Parallelismus, interne und externe Aktionen erklärt. Eigenschaften von CSP-Prozessen können mit Hilfe eines Model-Checkers automatisch überprüft werden.

In jüngster Zeit hat es vermehrt Anstrengungen gegben, die Vorteile beider Spezifikationssprachen zu kombinieren. Eine solche Kombination CSP-OZ wurde von C. Fischer in seiner 2000 fertiggestellten Dissertation beschrieben. Sie ist eine Grundlage für aktuelles Forschungen in der Abteilung ``Semantik'', bei denen es um die Anbindung von CSP-OZ einerseits an Java und andererseits an die Unfied Modeling Language (UML) geht.

Die Vorlesung führt in die Notation und Semantik von Z und CSP ein und erläutert deren Verwendung an Hand von Beispielen. Die Übungen vertiefen das Verständnis des Themas und führen in die Werkzeugunterstützung von Z und CSP ein. Ziel der Veranstaltung ist die Vermittlung von Fertigkeiten und Kenntnissen, die auch für die Praxis ein hohes Anwendungspotential haben.

Neben dem Vordiplom sind keine weiteren Vorkenntnisse erforderlich. Die Vorlesung eignet sich gut als Startpunkt für Diplomarbeiten in der Abteilung ``Semantik''.

 

zum Seitenanfang

Relevante Links

Formal Methods
http://www.afm.sbu.ac.uk/fm/
CSP
http://www.afm.sbu.ac.uk/archive/csp.html
FDR
http://www.fsel.com/
Z
http://www.afm.sbu.ac.uk/archive/z.html
Spivey. Z Reference Manual
http://spivey.oriel.ox.ac.uk/~mike/zrm/index.html

 

zum Seitenanfang

Literatur

M. Spivey. The Z Notation - A Refernce Manual. 2nd Edition. Prentice Hall, 1992.

Jim Woodcock, Jim Davies. Using Z - Specification, Refinement, and Proof. Prentice Hall, 1996.

C.A.R. Hoare.. Communicating Sequential Processes. Prentice Hall, 1985.

A.W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998.

C. Fischer. CSP-OZ: A Combination of Object-Z and CSP. In H. Bowmann, J. Derrick (Editors). Formal Methods for Open Object-Based Distributed Systems (Chapman & Hall, 1997) 423-438.

C. Fischer. Combination and Implementation of Processes and Data: from CSP-OZ to Java. Dissertation, Berichte aus dem Fachbereich Informatik 2/2000, Univ. Oldenburg, 332 Seiten, April 2000.

 

zum Seitenanfang

Vorlesungsskript

Das handschriftliche Skript zur Vorlesung ist an dieser Stelle nun in gesetzter Form erhältlich.

 

zum Seitenanfang

Übungsaufgaben

Hier wird die Möglichkeit geboten, die aktuellen Übungsblätter zu dieser Lehrveranstaltung im Postscript- oder DVI-Format abzurufen. Wir bitten jedoch im Interesse aller, die Übungsblätter nicht gedankenlos auszudrucken, insbesondere nicht auf den Laserdruckern der ARBI. Photokopien sind unter Berücksichtigung aller Kosten in der Regel günstiger als Laserdrucke!

Dieses Angebot richtet sich hauptsächlich an diejenigen, die auf anderem Wege kein Exemplar der Übungsblätter erhalten konnten.

 

zum Seitenanfang

Hinweise zur 4. Übung

Für die Bearbeitung der 3. Aufgabe auf dem 4. Übungsblatt benutzen Sie bitte das Werkzeug Z/EVES. Dieses ist auf den Solaris-Rechnern der Theoretischen Informatik installiert. Um nicht die gesamte bisherige Spezifikation eingeben zu müssen, können sie die Datei ``tel.tex'' benutzen, die Sie bei den Übungsaufgaben finden.

Sie können Ihre Türkarte für den Rechnerraum der Theorie (A3 2-207) freischalten lassen. Alternativ können Sie aber auch remote arbeiten. Der folgende Abschnitt erklärt eine mögliche Vorgehensweise hierzu. Der letzte Abschnitt führt in die Benutzung von Z/EVES im XEmacs ein.


zurück

Einloggen

Um sich von einem entfernten Rechner (z.B. von der ARBI) auf den Rechnern der Theorie einzuloggen und dort X11 zur Verfügung zu haben müssen Sie die Verbindung authentifizieren. Gehen Sie dazu bitte wie folgt vor:

Lassen Sie sich den MAGIC-COOKIE ausgeben. 

athen$ xauth list $DISPLAY
athen:0  MIT-MAGIC-COOKIE-1  adf....

Loggen Sie sich auf dem Theorie-Rechner ein und setzen Sie die Umgebungsvariable DISPLAY. 

athen$ rsh -l <theorie-login> celan
Password: 
celan$ export DISPLAY=athen:0

Fügen Sie den ermittelten MAGIC-COOKIE der Xauthority mittels ``xauth add <komplette cookie Zeile>'' hinzu (kopieren und einfügen). 

celan$ xauth add athen:0  MIT-MAGIC-COOKIE-1  adf.... 
celan$

Nun sollten Sie X-Anwendungen starten können. Als weitere Solaris-Rechner stehen Ihnen ``fats'', ``maceo'', ``chick'', ``chet'' und ``harry'' zur Verfügung (statt celan).
Bitte nicht mehr ``huxley'' benutzen!

(P.S.: Der relativ leichte Umweg über den Rechner ``zola'', wie in der Übung angekündigt, funktioniert leider nicht. Ich bitte um Entschuldigung)


zurück

Z/EVES im XEmacs

Z/EVES kann auch aus der Kommandozeile benutzt werden, dann ist die X-Authentifizierung nicht notwendig. Wir empfehlen jedoch die Benutzung im xemacs (Achtung: funktioniert nicht vollständig im emacs, also bitte xemacs benutzen!).

Starten Sie bitte den xemacs und öffenen Sie eine Z-Spezifikation (z.B. ``z-eves-bbook.tex''). Der XEmacs befindet sich dann zunächst im LaTeX-Modus (zu sehen in der Status-Zeile unter dem Buffer). Um Z/EVES aufrufen zu können wechseln Sie bitte in den ``z-latex-mode'', indem Sie die Tastenkombination Meta-x (meistens Alt-x) drücken, ``z-latex-mode'' eingeben (Tab-Erweiterung möglich!) und Return drücken. Die Statuszeile sollte sich entsprechend ändern. Im Hilfe-Menü können Sie über ``Describe Mode'' eine Kurzanleitung zum jeweils aktiven Modus erhalten.

Im ``z-latex-mode'' wird Z/EVES nun über die Tastenkombination Ctrl-c Ctrl-l gestartet. Falls Sie die Hilfe aufgerufen haben, müssen Sie vorher wieder in Ihre Spezifikation klicken, damit der richtige Buffer aktiv ist. Im XEmacs erscheint ein neuer Buffer, in dem das Z/EVES Prompt erscheint. (Das Fenster wird in zwei Hälften geteilt, wobei Z/EVES im unteren Teil auftaucht.)

Im folgenden kann dann die Z-Spezifikation eingelesen werden. Dazu platziert man den Cursor innerhalb eines Z-Teils und drückt die Tastenkombination Ctrl-c Ctrl-e, oder man markiert einen Bereich und benutzt Ctrl-c Ctrl-r. Im Birthday-Book Beispiel könnten Sie den Cursor z.B. im Bereich

 
\begin{zed}
[NAME, DATE]
\end{zed}

platzieren und dann diese Deklaration durch die Tastenkombination Ctrl-C Ctrl-e von Z-Eves einlesen lassen. Z/EVES bestätigt dann Ihre Eingabe durch die Meldung

given sets NAME, DATE
=>

Soll ein eingelesenes Z-Konstrukt wieder entfernt werden, so geben Sie bitte am Z/EVES-Promt ``undo;'' ein. Wenn Sie nun versuchen das Schema ``BirthdayBook'' einzulesen, werden Sie eine Meldung von Z/EVES erhalten, dass die Namen ``NAME'' und ``DATE'' noch nicht deklariert sind.

Für die axiomatische Definition der Anschlüsse Tel1, ... Tel4 im Telefon-Beispiel müssen Sie Z/EVES unterstützen. Dieses erreicht man durch die Eingabe von ``reduce;'' am Z/EVES Prompt. In vielen Fällen führt der Befehl ``prove by reduce;'' zum Erfolg. Beweisschritte dieser Art können auch in der Spezifikationsdatei festgehalten werden durch die Umgebung ``zproof'' nach der Z-Umgebung, im Beispiel also:

...
\end{axdef}
\begin{zproof}
reduce;
\end{zproof}

Weitere Informationen können Sie der Dokumentation zu Z/EVES entnehmen, die im Verzeichnis /usr/local/zeves/doc zu finden ist. Insbesondere der ``User's Guide'' ist für die ersten Schritte zu empfehlen. Die Homepage zu Z/EVES finden Sie unter http://www.ora.on.ca/z-eves/welcome.html .

 

zum Seitenanfang

Hinweise zum CSP-Werkzeug FDR

Formal System Ltd. (Europe), eine von A.W. Roscoe geleitete Spin-Off-Firma der Universität Oxford, vertreibt das Werkzeug FDR zum automatischen Überprüfen von semantischen Eigenschaften von CSP-Prozessen mit endlicher Zustandsmenge. FDR steht für ``Failures Divergence Refinement''. Aktuelle Informationen zu FDR findet man im WWW unter http://www.fsel.com/ .

Mit diesem Werkzeug können CSP-Prozesse in ASCII-Syntax eingegeben werden und auf folgende Eigenschaften hin überprüft werden:

  • Deadlock- und Livelock-Freiheit, sowie Determinismus
  • Verfeinerung (engl. refinement) auf Basis der Semantiken Trace, Stable-Failures und Failures-Divergence-Semantik.
  • Falls die Verfeinerungsbeziehung zwischen Implementierung P und Spezifikation Q nicht gilt, wird ein Gegenbeispiel in Form einer Trace angezeigt, die in P möglich ist, aber nicht in Q.

Im folgenden ist der ASCII-Eingabecode eines Puffers für den FDR-Model-Checker sowie das entsprechende Ausgabefenster wiedergegeben. 

 
      channel in, out: {0,1}

      Puffer1  =    in.0 -> out.0 -> Puffer1
                 [] in.1 -> out.1 -> Puffer1

      Puffer2  =    in.0 -> Puffer20 [] in.1 -> Puffer21

      Puffer20 =   out.0 -> Puffer2
                 [] in.0 -> out.0 -> Puffer20
                 [] in.1 -> out.0 -> Puffer21

      Puffer21 =   out.1 -> Puffer2
                 [] in.0 -> out.1 -> Puffer20
                 [] in.1 -> out.1 -> Puffer21


      channel lk: {0,1}
      A = {lk.0, lk.1}

      PufferImpl2 =
        (        Puffer1[[out.0 <- lk.0, out.1 <- lk.1]]
         [| A |] Puffer1[[in.0 <- lk.0, in.1 <- lk.1]]) \ A

      assert Puffer2     [T= PufferImpl2

      assert PufferImpl2 [T= Puffer2
Hierbei ist [T= die ASCII-Darstellung der Trace-Inklusion.

Hauptfenster von FDR


zurück

Bedienung von FDR

Das Tool liegt auf den Rechnern der Theorie unter /usr/local/fdr. Die Dokumentation findet man im HTML-Format im Verzeichnis help. In FDR ist zwar ein Browser eingebaut, es ist aber besser, das Manual mit einem herkömmlichen Browser - z.B. netscape - zu lesen. Im Verzeichnis manual liegt eine Postscriptversion desselben Dokuments.

Im Verzeichnis demo findet man einige Beispieldateien.

Das Tool wird mit xfdr gestartet (bzw. am besten mit nice xfdr). Nach dem Starten muss man die Datei angeben, mit der man arbeiten möchte. Die Eingabedatei erstellt man vorher mit seinem Lieblingseditor. Dann erscheint das Fenster aus der Abbildung. Weitere Erklärungen zur Benutzung findet man im Abschnitt 2 ``Using FDR'' des Manuals.

Die Fehlermeldungen von FDR sind sehr schlecht und nicht besonders übersichtlich. Fehler werden nur im Fenster Options -> show Status angezeigt. Dieses Fenster sollte man daher immer geöffnet haben.

Beim Laden werden nur sehr wenige syntaktische Eigenschaften überprüft. Erst beim Überprüfen von Eigenschaften kann man feststellen, ob ein Prozeß syntaktisch richtig ist. Man sollte daher insbesondere am Anfang einfache Eigenschaften wie Livelocks überprüfen, um die syntaktische Korrektheit sicherzustellen.