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

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.

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