Navigation

Kontakt

Leitung

Prof. Dr. Ernst-Rüdiger Olderog

Sekretariat

Andrea Göken

+49-(0)441-798-3121

+49-(0)441-798-2965

A3 2-208

Einbettung einer objekt-orientierten formalen Methode in einen objekt-orientierten Software-Entwicklungsprozess (ForMooS)

Projektbeschreibung

Projektleitung: E.-R. Olderog und H. Wehrheim

Projektdauer: 1.10.2001 bis 31.12.2005

Finanzierung durch: DFG

Das Ziel des Projektes ist es, eine objekt-orientierte formale Methode in den Software-Entwicklungssprozess einzubetten und dadurch die nötige formale Präzision in der Beschreibung von Software-Komponenten zu erreichen. Die Einbettung soll die Vorteile der objekt-orientierten graphischen Modellierungssprache (UML) erhalten sowie eine Durchgängigkeit bis hin zur objekt-orientierten Implementierungssprache (Java) gewährleisten. Die Leitidee für die Formalisierung der Funktionalität von Komponenten ist ein erweitertes Konzept des Design-by-Contract, eines Vertrages zwischem dem Entwickler und dem Benutzer einer Komponente. Dieses Konzept soll durchgängig auf drei Beschreibungsebenen verwendet werden: in der graphischen Modellierungssprache UML und der formalen Spezifikationsmethode (CSP-OZ) zur Festlegung der Contracts sowie in der objekt-orientierten Implementierungssprache Java zur Überprüfung der Contracts.

Wissenschaftliche Mitarbeit: H. Rasch, M. Möller

Werkzeuge

 

Im Rahmen des Projektes wurden und werden Werzeuge entwickelt und benutzt, auf die wir hier verweisen wollen.

  • Jass - Java with Assertions
    Auch wenn für die Zusicherungen in Java-Programmen inzwischen die Java Modeling Language (JML) benutzt wird, wird dennoch das Werkzeug, das Anwender in In- und Ausland gefunden hat, weiter gepflegt.
  • Jassda - Jass Debugger Architecture
    Das in der Diplomarbeit von Mark Brörkens entstandene Werkzeug liefert eine Plattform für Laufzeitüberprüfungen von Java Programmen. Im Rahmen von ForMooS wird insbesondere der "trace-checker" gepflegt und weiterentwickelt, der die Konsistenz einer Programmausführung mit CSPjassda Spezifikationen sicherstellt.
  • CSP-OZ für Rational Rose
    Im Rahmen des Projektes wurde/wird ein UML-Profile für CSP-OZ entwickelt, für das eine Unterstützung in Rational Rose implementiet wurde.
  • FDR
    Der kommerzielle Modelchecker FDR kommt im ForMooS Umfeld insbesondere in der mittleren Schicht (CSP-OZ) zum Einsatz.

 

Publikationen

Hier finden Sie eine Auswahl der Publikationen mit Relevanz für das Projekt ForMooS.

Webmaster (m.wzpgiqtesekinhdwc9g@uol.de) (Stand: 17.12.2019)