This co-operation started in the context of the ESPRIT Basic Research I project (no. 7071) on Provably Correct Systems, 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 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 co-operation 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 ), 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.
The algorithm should be designed as a set of transformation rules which are provably correct from the semantics of the programming language. The result of the partitioning is still a program, but its structure reflects the software and hardware components, and how they interact to achieve the overall goal. It is possible to express this result as a program because the programming language of ProCoS includes features to express parallelism and communication. Another objective of the co-operation is to use a term rewriting system both to verify the transformation rules and to carry out the partitioning task using the rules.
The software components generated by the process should then be compiled using the current methods in use in ProCoS . The hardware parts need also be compiled in to some hardware description language. This latter step has been explored at Oxford in work associated with ProCoS , and we plan to use/adapt the work carried out at Oxford for this task.