ForMooS
Kontakt
Leitung
Sekretariat
ForMooS
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.