Project duration: 1.10.1999 to 30.9.2001

Financing by: DFG

The goal of this project is a methodology for the development of communicating and time-critical systems, starting from graphical descriptions of requirements up to the creation of design specifications. The main focus is on how system requirements can be decomposed in a semantically correct way into process-orientated, data-orientated and time-critical aspects, so that these aspects can first be developed independently of each other and then finally be combined again and possibly restructured.

As a basis for this, a common semantic model is to be developed that combines the essential elements of the individual methods CSP, Object-Z and Duration Calculus in a consistent manner. On this basis, correct transformations for the decomposition, composition and restructuring of system specifications can then be specified.

These transformations will be tested in particular on the reference case study from traffic control technology. To this end, existing tool support will be used and further developed.

This project continues the work begun in the ProCoS and UniForM projects and is associated with the DFG Priority Programme Integration of Software Specification Techniques for Engineering Applications.

Scientific collaboration: J. Hoenicke

In CSP-OZ, the already existing integration of CSP and Object-Z, a specification of the production automation case study of the focus programme was created. Simple properties of this specification (e.g. deadlock-free) have been verified by translating the CSP-OZ specification into the input language of the CSP model checker FDR and subsequent model checking. The results of this work will be presented at the ETAPS conference FASE, Berlin, March 2000:

H. Wehrheim, Specification of an Automatic Manufacturing System -- A case study in using integrated formal methods.

The translation, which was done by hand for this case study, is currently being implemented as part of a Diplom thesis.

J. Hoenicke specified the braking curve and its monitoring in more detail for the traffic control technology case study. The braking curve itself was represented with Z, the monitoring process with CSP and DC formulae are used to determine that monitoring takes place frequently enough. A proof of the correctness of this specification is currently being prepared. This proof is being carried out manually.