Seminar "Formale Software-Spezifikation"

 

1 Organisatorisches

Form: 2 SE    (3 ECTS-Punkte)

Veranstalter: E.R. E.-R. Olderog

 

2 Inhalt

In diesem Seminar wollen wir Ansätze zur formalen Spezifikation und Analyse von Software kennenlernen. Ein Schwerpunkt liegt auf der objekt-orientierten Spezifikation. Dazu sollen verschiedenene Spezifikationsmethoden vorgestellt und ihre Semantik erläutert werden. Einige Methoden sind werkzeugunterstützt, so dass auch die Vorstellung der verfügbaren Werkzeuge von Interesse ist.

 

3 Anmeldung

• Vorbesprechung:
  Montag, den 1.7.2002, um 14.15 Uhr
  im Raum A3 2-214 der Theoretischen Informatik
• Interessentinnen und Interessenten können auch per E-mail mit dem Veranstalter Kontakt aufnehmen:
  olderog@informatik.uni-oldenburg.de

 

4 Vortragsthemen

4.1 Spezifikation von Java-Programmen

Es werden Methoden zur Spezifikation und Analyse von Java-Programmen betrachtet.

• JML - Java Modeling Language

  JML ist die Spezifikationssprache, mit der das Verhalten von Java-Modulen beschrieben werden kann, bevor diese implementiert werden.

  G.T. Leavens, A.L. Baker and C. Ruby. JML: A Notation for Detailed Design, 1999.

  G.T. Leavens, A.L. Baker and C. Ruby. Preliminary Design of JML, 2002.

  Web-site: http://www.jmlspecs.org/
  Werkzeuge: s.o.

• Extended Static Checking for Java

  Es geht um eine Technik zur statischen Programmanalyse, durch die Programmierfehler wie überschrittene Arraygrenzen, Typfehler,Deadlocks gefunden werden sollen.

  D.L. Detlefs, K.R.M. Leino. G. Nelson and J.B. Saxe. Extended Static Checking, 1998.

  Web-site: http://research.compaq.com/SRC/esc/
  Werkzeug ESC/Java: s.o.

• Dynamic Invariant Detection

  In Programmen sollen Schleifeninvarianten und andere Zusicherungen zur Laufzeit entdeckt werden.

  M.D. Ernst, A. Czeisler, W.G. Griswold and D. Notkin. Quickly Detecting Relevant Program Invariants, 2000.

  Web-site: http://pag.lcs.mit.edu/daikon
  Daikon Werkzeug: http://www.cs.washington.edu/homes/mernst/daikon

4.2 Graphische Spezifikationen

Es werden graphische Notationen aus UML, der Unified Modeling Language, untersucht, insbesondere Sequenzdiagramme und State Charts.

• Message Sequence Charts

  S.Mauw and M.A. Reniers. An algebraic semantics of Message Sequence Charts, 1994.

• State Charts

  D. Harel and A. Naamad. The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology (ACM TOSEM) 5:4, pages 293--333, 1996.

4.3 Logische Spezifikationen

Es werden die logischen Spezifikationssprachen Z und Object-Z vorgestellt.

• Object-Z

  G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.

• Anwendung von Z

  U, Hamer and J. Peleska. Z applied to the A330/340 CIDS Cabin Communication System. In: M.G. Hinchey and J.P. Bowen (Editors). Applications of Formal Methods, Prentice Hall, 1995

  Das Buch enthält 16 Fallstudien, in denen formale Spezifikationmethoden auf konkrete Software-Entwurfsprobleme angewandt wurden.

4.4 Weitere mögliche Themen

• Eifel

  B. Meyer: Eiffel - Programmeiren mit Vertrag (als Vorbereitung auf JML)

• B

  E. Sekerinski und K. Sere (Editors). Program Development by Refinement: Case Studies Using the B Method. Springer-Verlag, 1999.