Embedding of an object-oriented formal method into an object-oriented software development process. (ForMooS)

 

1 Description

project management: E.-R. Olderog and H. Wehrheim

project duration: 1. Oct. 2001 to 31. Dez. 2005

financed by: DFG

The aim of this project is to embed an object-oriented Formal Method into the software development process and thus providing the necessary formal precision in the description of software components. The embedding will preserve the advantages of the object-oriented graphical modelling language (UML) and guarantee a continuity till the object-oriented implementation language (Java). The main idea for formalising the functionality of components is an extended concept of Design-by-Contract, a contract between provider and consumer of a component. This concept will be used in all three levels of description: in the graphical modelling language UML, the formal specification method (CSP-OZ) for defining the contracts, and finally the object-oriented implementation in Java for checking the contracts.

scientific staff: H. Rasch, M. Möller

 

2 Tools

In the context of this project several tools were developed and/or used for which we provide brief information.

• Jass - Java with Assertions
  We still support and maintain the tool that has national and international users, although we use the Java Modeling Language (JML) for the assertions at the Java level, now.
• Jassda - Jass Debugger Architecture
  The tool that Mark Brörkens developed in his master's thesis provides a platform for runtime checking of Java programs. In the context of the project we are maintaining and extending the tool, especially the "trace-checker" that ensures consistency of a program execution with a CSP_jassda specification.
• CSP-OZ for Rational Rose
  In the context of the project we are developing a UML-profile for CSP-OZ, for which support in Rational Rose was implemented.
• FDR
  The commercial model-checker FDR is used within the ForMooS field especially for the intermediate level (CSP-OZ).

 

3 Publications

Here we provide a selection of publications with relevance to the ForMooS project.

[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 ]