Vorlesung Formale Methoden

Organisatorisches

 

Formale Methoden (3 VL,1 Ü) 

Wahlmodul ab 5. Semester           

      Vorlesung
        Dienstag       14-16, HS F         Wehrheim
        Donnerstag 16-17, HS F

       Beginn der Vorlesung: 16.10.03

       Am 22.1. findet keine Vorlesung statt. 

      Übungen                        
        Donnerstag 17-18, HS F         Wehrheim

      Scheinerwerb
         DPO4: mündliche Prüfung
         DPO3: 50% der Übungsaufgaben, aktive Teilnahme an der Übung

Inhalt

Formale Methoden sind Sprachen zur Modellierung/Spezifikation von Systemen. Ein Modell eines (Soft- oder Hardware) Systems beschreibt auf einer gewissen Abstraktionsebene die Funktionalität des Systems. Im Gegensatz zu (den meisten) Programmiersprachen besitzen formale Methoden eine genau festgelegte Semantik, d.h. eine mathematische Beschreibung der Bedeutung einer Spezifikation. Diese Festlegung der Semantik erlaubt es, das Systemmodell bereits vor der eigentlichen Implementierung formal zu analysieren und mögliche Fehler frühzeitig zu finden. In der Vorlesung sollen verschiedene formale Methoden (unter anderem Petrinetze, Prozeßalgebren, Z, TLA) eingeführt werden, die für unterschiedliche Systemarten geeignet sind. Für jede dieser formalen Methoden werden Semantik und Analysetechniken vorgestellt und Modellierungsbeispiele zur Illustration des Einsatzbereiches besprochen.

Links

 *Die* Überblicksseite für formale Methoden findet sich hier. Sie bietet viele Links auf Einzelformalismen, Projekte im Bereich formaler Methoden und Newsgroups.

Literatur

 Zur Einführung:

[1] J.M. Wing, A Specifier's Introduction to Formal Methods. IEEE Computer, 23(9):8-24, September 1990.

[2] E. Clarke and J. Wing, Formal Methods: State of the Art and Future Directions, CMU Computer Science Technical Report CMU-CS-96-178, August 1996.
erschienen in: ACM Computing Surveys, 28(4):626-643, 1996.


Zu den einzelnen formalen Methoden:

Petrinetze:

[1] W. Reisig, Petrinetze - Eine Einführung. Springer Verlag, 1985.

[2] B. Baumgarten, Petri-Netze - Grundlagen und Anwendungen. BI Wissenschaftsverlag, 1990.

[3] Petrinetz Seite im Web

CCS:

[1] R. Milner, Communication and Concurrency. Prentice Hall, 1989.

Z:

[1] M. Spivey, Z User Manual

[2] J. Woodcock, J. Davies, Using Z - Specification, Refinement, and Proof. Prentice Hall, 1996.

TLA:

[1] L. Lamport, Specifying Systems, Addison Wesley. Für den Eigengebrauch herunterladbar.

Übungsaufgaben

Heike Wehrheim