Project leaders: E.-R. Olderog and H. Wehrheim

Project duration: 1.10.2001 to 31.12.2005

Financing by: DFG

The aim of the project is to embed an object-orientated formal method into the software development process and thereby achieve the necessary formal precision in the description of software components. The embedding is intended to preserve the advantages of the object-oriented graphical modelling language (UML) and ensure consistency right through to the object-oriented implementation language (Java). The guiding idea for formalising the functionality of components is an extended concept of design-by-contract, a contract between the developer and the user of a component. This concept is to be used consistently at three levels of description: in the graphical modelling language UML and the formal specification method (CSP-OZ) to define the contracts and in the object-oriented implementation language Java to check the contracts.

Scientific collaboration: H. Rasch, M. Möller

Tools have been and are being developed and used as part of the project, which we would like to refer to here.

• Jass - Java with Assertions
  Even though the Java Modelling Language(JML) is now used for assertions in Java programs, the tool, which has found users at home and abroad, continues to be maintained.
• Jassda - Jass Debugger Architecture
  This tool, which was developed as part of Mark Brörkens' Diplom thesis, provides a platform for checking the runtime of Java programmes. As part of ForMooS, the "trace-checker" in particular is maintained and further developed, which ensures the consistency of programme execution with CSPjassda specifications.
• CSP-OZ for Rational Rose
  As part of the project, a UML profile for CSP-OZ has been/is being developed, for which support has been implemented in Rational Rose.
• FDR
  The commercial model checker FDR is used in the ForMooS environment, particularly in the middle layer (CSP-OZ).

Here you will find a selection of publications relevant to the ForMooS project.