Introduction

The ESPRIT ProCoS Provably Correct Systems project is underway again. After discouraging delays and cuts, we have reformed a tightly focussed project with just four partners in 1992, dedicated to cover the fundamental technical aspects of a development process for critical embedded systems, from the original capture of requirements right down to the computers and special purpose hardware on which the programs run.

This breadth of scope is inspired by the brilliant work of Bob Boyer and J. Strother Moore at Computational Logic Inc. (CLInc) in Austin, Texas [28][17]. The distinctive approach of the European effort is to emphasise:

1. A constructive approach to correctness, using proven transformations between specifications and designs and programs and compilers and hardware. Thus errors at this stage are avoided, so their absence never needs proving subsequently.

2. The use of a common abstract mathematical model to ensure global consistency across all the interfaces between design phases, notations, and technologies.

3. The inclusion of explicit parallelism and timing constraints throughout the development.

In these ways we hope to achieve an advance in technology in spite of reductions in research funding; furthermore, we hope to deliver theories and transformations which can be cheaply reused without specialist knowledge on an industrial scale for new projects and new products, as the need arises.

The partners in the project are as follows:

1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, U.K. Responsible for coordination, political, financial and technical. Concentrates on a universal model to secure consistency of all the interfaces involved. Prof. Tony Hoare leads the site and the project, with the help of Jonathan Bowen, Stephen Brien, He Jifeng, Wayne Luk, Ian Page and Augusto Sampaio.

2. DTH, Department of Computer Science, Building 344, Technical University of Denmark, DK-2800 Lyngby, Denmark. Responsible for interface to reality, control engineering etc. Concentrates on capture and formalisation of total requirements, and the development of specifications for the computer-controlled components of the system. Anders P. Ravn is the site leader and is aided by Kirsten M. Hansen, Michael R. Hansen (currently visiting Oldenburg), Hans Henrik Løvengreen, Jens Nordahl, Hans Rischel, Jens U. Skakkebæk and E.V. Sørensen.

3. University of Oldenburg, FB10 - Informatik, Ammerländer Heerstraße 114-118, D-2900 Oldenburg, Germany. Responsible for production of correct programs. Concentrates on the design process from specification to the code of programs executed perhaps on multiple computers; plans mechanical checks and aids for this process. Prof. Ernst-Rüdiger Olderog is the site leader, with Stephan Rössig and Michael Schenke as team members.

4. Christian-Albrechts-Universität Kiel, Institut für Informatik und Praktische Mathematik, Preußerstraße 1-9, D-2300 Kiel 1, Germany. Responsible for production of correct machine code from timed high-level programs. Concentrates on the systematic development of a provably correct compiler. Prof. Hans Langmaack leads the site with Bettina Buth, Karl-Heinz Buth, Martin Fränzle, Burghard von Karger (currently visiting Oxford), Markus Müller-Olm and Ruben-Benjamin Reincke as members of the research group that do work for or related to the project.

Each site is responsible for progressing an agreed series of case studies, and for writing up a self-contained textbook for experts in the relevant area. In addition, there is a great deal of associated work not funded by the CEC. For example, Oxford hopes to explore the development of provably correct hardware compilers, targeting on Field Programmable Gate Arrays; and Lyngby are exploring theories to support reliability assessment.