Provably Correct Systems | Concluded in 1997

This project is dedicated to cover the entire development process for critical embedded systems, from the original capture of requirements to the computers and special-purpose hardware on which the developed programs run.

The cooperation proposed here is in the context of the ESPRIT Basic Research PROCOS II project (no.7071) on Provably Correct Systems. The emphasis is on a constructive approach to correctness, using proven algebraic transformations between adjacent phases of development: specifications, designs, programs, compilers and hardware. The purpose of this cooperation is to explore the development of embedded systems in such a way that the final implementation may include both software and hardware components. Rather than producing only machine code as the final implementation (as stated in the original objectives of PROCOS I), the aim is to design a partitioning algorithm which, based on some function of cost, determines what should be implemented in software and in hardware. The main concern is not the discovery of an original partitioning algorithm, but rather a correct design of (possibly an existing) one.