Experiences from the European ProCoS Projects: Provably Correct Systems

This paper presents the collaborative European ESPRIT ProCoS projects on “Provably Correct Systems”, and associated initiatives of the 1990s. The influence of the projects in the field of formal methods is also discussed. A general overview of the projects is provided, together with a number of reminiscences by those involved with the projects, including the influence on the subsequent careers of participants. The projects addressed the issues of connecting formal approaches at different connected levels of formality, including requirements, specification, and compilation down to machine code and even directly into hardware. The investigations were based on a representative subset of the programming language Occam, which was subsequently extended by elements indicative of particular problems of compilation, yet not found in Occam, and the related Transputer microprocessor. In practice, two of the most important and enduring results after the projects were Duration Calculus and Unifying Theories of Programming, both subfields of formal methods, with associated communities of researchers and practitioners.