ESPRIT ProCoS-WG Working Group
(no. 8694, 1993-1997)

The final report (10 pages) is available in PostScript format:

A ProCoS-WG Working Group Project Final Report: ESPRIT Working Group 8694, Jonathan Bowen (The University of Reading, UK), C.A.R. Hoare (Oxford University, UK), Hans Langmaack (Christian-Albrechts-Universität zu Kiel, Germany), Ernst-Rüdiger Olderog (Universität Oldenburg, Germany) and Anders P. Ravn (Technical University of Denmark), Bulletin of the European Association for Theoretical Computer Science (EATCS), Volume 64, pages 63-72, February 1998.

The last major meeting was held 7-9 April 1997, at the University of Reading, UK, in conjunction with ZUM'97.

A Hardware Synthesis and Verification Workshop was held at Cornell University, Ithaca, New York, USA, 14-16 August 1996.

This document contains information relevant to the European ESPRIT Basic Research ProCoS-WG Working Group (no. 8694) of 24 academic and industrial partners interested in Provably Correct Systems associated with the ProCoS II project (no. 7071). A ProCoS-WG description of the objectives, activities, potential, etc., of the Working Group is available. A bibliography of relevant publications mainly by Working Group members has been produced in BibTeX format. A robot-based production cell has been chosen as a common case study for partners wishing to compare formal methods.

As co-ordinators of the Working Group, the Oxford University Computing Laboratory welcomes visits by other Working Group sites and an on-line guide to Oxford is available.

Synopsis

ProCoS-WG - Provably Correct Systems

Work Area
Theories for Concurrency and Real-time;
Specification and Verification

COORDINATOR (Country)
Oxford University (UK)
Computing Laboratory
Wolfson Building, Parks Road
UK - OXFORD OX1 3QD

Participants
Graz University of Technology (A)
DST Deutsche System Technik GmbH (D)
Forschungszentrum Informatik, Karlsruhe (D)
Universität Kiel (D)
Universität Oldenburg (D)
Philips GmbH Forschungslaboratorien (D)
RWTÜV Anlagentechnik (D)
Technische Hochschule Darmstadt (D)
Danish State Railways (DK)
IFAD (DK)
Technical University of Denmark (DK)
GEC Alsthom (F)
Verimag (F)
Politecnico di Milano (I)
University of Oslo (N)
University of Reading (UK)
University of Twente (NL)
Swedish Institute for Computer Science (S)
Åbo Akademi University (SF)
University of Cambridge (UK)
Lloyd's Register (UK)
National Physical Laboratory (UK)
Praxis Systems plc (UK)
University of York (UK)

CONTACT POINT
Jonathan Bowen
Tel: +44-118-931-6544
Fax: +44-118-975-1994
Email: procos-request@comlab.ox.ac.uk

Keywords: Programming Methodology, Safety-Critical Systems, Specification Languages, Programming Languages

Start date: 1 January 94
Duration 36 months (extended by 6 months)
Status: running

Abstract: The ProCoS-WG Working Group is based around the existing Basic Research project (7071) to aid dissemination of the project's results. ProCoS-WG aims to improve dependability, reduce timescales and cut development costs of construction for embedded systems, particularly in real-time and safety-critical applications. It uses and develops the results of basic research into fundamental properties of interactive systems. It aims to provide a scientific basis for future standards of practice in the development of embedded systems, ensuring correctness of all stages in the development, from elicitation and analysis of requirements through design and implementation of programs down to compilation and execution on verified hardware.

Aims

ProCoS-WG aims to aid the dissemination of results of the existing project. The long term objective of the Working Group is to contribute to radical improvement in standards of professional practice in the design and implementation of information technology products, involving both hardware and software. The first target for improvement is in the area of safety critical application; but we believe that much of the same technology will eventually spin off to improve quality and reduce life cycle costs of other products in widespread use.

Topics of interest to members of the Working Group include theories and methodology to handle the following: (1) Requirements capture and analysis; (2) System specification and design; (3) Programming language processing and compilation; (4) Machine hardware, including multiprogramming kernels; (5) Implementation in hardware down to gate level.

Activities

The ProCoS-WG Working Group is closely associated with the ProCoS II Basic Research project (7071). Joint workshops were held during the lifetime of that project, approximately every 6 months at project sites in Denmark, Germany and the UK.

The 1st Working Group meeting was held at Gentoft, Denmark, 18-20 January 1994. An "active" photograph of the participants is available.

The major event for the Working Group was an open School and Symposium organised jointly with the existing Formal Techniques in Real-Time and Fault-Tolerant Systems series, held 19-23 September 1994 at Lübeck, Germany. A published proceedings is available as Springer LNCS volume 863. ISBN 3-540-58468-4.

The 2nd ProCoS-WG meeting (for ProCoS-WG participants and invited guests only) was held on 10-12 January 1995 in Oxford, UK, organized by Jonathan Bowen. Information for participants and an agenda including summaries of the talks and a copy of the original invitation are available.

The 3rd ProCoS-WG meeting was held 21-23 August 1995 at the Hotel Marina, Vedbæk, just outside Copenhagen, Denmark. The local organizers were Hans Rischel (programme) and Disa la Cour (secretary), ID/DTU. A theme of Linking Theories was suggested by Prof. Tony Hoare.

The 4th ProCoS-WG meeting, was held 11-13 March 1996, in Oldenburg, Germany, organized by Prof E-R. Olderog.

An associated ProCoS-US Hardware Synthesis and Verification Workshop was held at Cornell University, Ithaca, New York, USA, 14-16 August 1996.

The last major meeting was the 5th ProCoS-WG meeting, 7-9 April 1997, at the University of Reading, UK, in conjunction with ZUM'97 (see below). This was the 5th and final meeting of the Working Group. The local organizing secretary was Christina Simmons in the Department of Computer Science.

The group also supports the Z User Meeting series of conferences. The 8th Z User Meeting (ZUM'94) was was held on 29-30 June 1994 at the University of Cambridge, UK. The 9th International Conference of Z Users (ZUM'95) was held 7-9 September 1995 at the University of Limerick, Ireland, both supported by ProCoS-WG. The last meeting was ZUM'97 which was held at the University of Reading, UK, 3-4 April 1997.

Potential

The Working Group will seek a simplification of the technology produced by the ProCoS project to make it truly useful for engineers in an industrial setting. We hope to be influential in the area of European and international standards, particularly for safety-critical systems.

Other information

A 2-page formatted summary of the Working Group, on which the information above is based, and a more detailed 10-page article (published in Bulletin of the EATCS, 53, pp 136-145, June 1994, also available in hypertext format) are available. Personnel involved with ProCoS at OUCL include Jonathan Bowen (manager of the Working Group), Prof. C.A.R. Hoare (manager of the ProCoS II project) and Prof. He Jifeng (who was employed fulltime on the ProCoS project). Joan Arnold was the Working Group secretary. Christina Simmons has also provided some funded secretarial support.