Applying Formal Methods to Real-Size Object-Oriented Designs in Technical Environments


AFRODITE - 6500

Keywords object orientation, formal specifications, real-time systems


Start Date: 01-SEP-92 / Duration: 36 months

[ contact / participants ]


Objectives and Approach

AFRODITE aims to demonstrate the applicability of formal specification to the development of combined software/hardware systems in a technical environment, using an extended version VDM. The applications will include safety-critical and highly distributed systems and the design of a dedicated parallel real-time computer architecture for on-line data acquisition.

Progress and Results

In its first year the consortium designed the object-oriented, parallel and real-time part of what is now called VDM++. The consolidation based upon the experience of the pilot applications for the OO part has been achieved and the parallel part will follow by the end of 1993. The Real-time part is due mid 94. Tool support comprising syntax checking, extensive static semantic checking, pretty printing and (large scale) specification management is available for the OO part.

The efforts of AFRODITE to embed VDM++ into existing (non-formal) development methods and their tools led to the inclusion of this formal language into the Object Modelling Technique (OMT) as an extra module in an OMT case environment. Similarly the inclusion of VDM++ in the SDW development tool set will be realised. These activities provide widespread and common access for the new technology.

The range of applications is extended with the verification of a design for a new air traffic control architecture in France.

Apart from language consolidation and tool development the main focus of AFRODITE will gradually move into the development guidelines and support of Iterative Formal Development Approaches. The production of a complete set of ingredients to support the take-up (at a departmental level) by a company confronted with combined hardware/software design tasks is one of the objectives of the project.


CONTACT POINT

Mr Eugene Durr
CAP Gemini International Support BV
Dolderseweg 2 - Huis ter Heide
PO Box. 2575
NL - 3500 GN UTRECHT
tel: + 31 /3403 35411
fax: + 31 /3404 31174
email:durr@fys.vuu.nl.

Participants

CAP GEMINI INTERNATIONAL
SUPPORT BV - NL - C
CERN - CH - P
DRA (DEFENCE RESEARCH AGENCY) - UK - P
HELINTEC - GR - A
STNA - F - P
VERILOG - F - P
IFAD - DK - A
IMPERIAL COLLEGE LONDON - UK - A


ST synopses home page ST acronym index ST number index
All synopses home page all acronyms index all numbers index

AFRODITE - 6500, December 1993


please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook