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

 

1 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

 

2 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 CSP_jassda 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.

 

3 Publikationen

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

[M05]

M. Möller. Mapping formal specifications to java contracts. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 100-102. University of Copenhagen, Denmark, October 2005.
[ bib | .pdf ]

[MORW04]

M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Linking CSP-OZ with UML and Java: A Case Study. In E. Boiten, J. Derrick, and G. Smith, editors, Integrated Formal Methods, number 2999 in Lecture Notes in Computer Science, pages 267-286. Springer-Verlag, March 2004.
[ bib | .pdf | Abstract ]

[RW03]

H. Rasch and H. Wehrheim. Checking Consistency in UML Diagrams: Classes and State Machines. In E. Najm, U. Nestmann, and P. Stevens, editors, Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 229-243. Springer, 2003.
[ bib | .ps ]

[RW02]

H. Rasch and H. Wehrheim. Consistency between UML classes and associated state machines. In L. Kuzniarz, G. Reggio, J. L. Sourrouille, and Z. Huzar, editors, UML 2002 - Workshop on Consistency Problems in UML-based Software Development, volume 06, pages 46-60, 2002.
[ bib ]

[BM02]

M. Brörkens and M. Möller. Dynamic Event Generation for Runtime Checking using the JDI. In Klaus Havelund and Grigore Rosu, editors, Proceedings of the Second Workshop on Runtime Verification (RV'02), Copenhagen, Denmark, July 2002, volume 70 of Electronic Notes in Theoretical Computer Science. Elsevier Science, July 2002. This publication is available at ENTCS.
[ bib | .pdf | Abstract ]

[M02]

Michael Möller. Specifying and Checking Java using CSP. In Workshop on Formal Techniques for Java-like Programs - FTfJP'2002. Computing Science Department, University of Nijmegen, June 2002. Technical Report NIII-R0204.
[ bib | .pdf | Abstract ]

[Weh02]

H. Wehrheim. Checking behavioural subtypes via refinement. In B. Jacobs and A. Rensink, editors, FMOODS 2002: Formal Methods for Open Object-Based Distributed Systems, pages 79-93. Kluwer, May 2002.
[ bib | .ps | Abstract ]

[BFMW01]

D. Bartetzko, C. Fischer, M. Möller, and H. Wehrheim. Jass - Java with Assertions. In Klaus Havelund and Grigore Rosu, editors, Proceedings of the First Workshop on Runtime Verification (RV'01), Paris, France, July 2001, volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001. This publication is available at ENTCS.
[ bib | .pdf | Abstract ]

[FOW01]

C. Fischer, E.-R. Olderog, and H. Wehrheim. A CSP view on UML-RT structure diagrams. In H. Husmann, editor, Fundamental Approaches to Software Engineering, volume 2029 of Lecture Notes in Computer Science, pages 91-108. Springer-Verlag, 2001.
[ bib | .ps | Abstract ]

[Weh00]

Heike Wehrheim. Specification of an automatic manufacturing system - a case study in using integrated formal methods. In FASE 2000, Fundamental Approaches to Software Engineering, volume 1783 of LNCS, 2000.
[ bib | .ps | Abstract ]