In 1990 we performed a study for RSRE (now QinetiQ) into how to develop a compiler for high integrity applications that is itself of high integrity. We developed a technique for specifying a compiler and proving it correct, and built a small proof-of-concept prototype.
The technique is described, and a small case study is worked up in full, including all the proofs, in High Integrity Compilation . The technique involves writing a formal specification of the compiler in terms of translation templates. The denotational semantics of the source and target language are also formally specified. The proof shows that the compiler is ‘meaning preserving’, that it always produces a target language program that has the same meaning as the corresponding source language program. The compiler specification is implemented in a high level language to give an executable compiler. (The source and target language specifications can also be implemented, to provide interpreters for these languages.)
Engineers at AWE read about the study and asked us to use these techniques to implement a compiler for their own high integrity processor, called the ASP (Arming System Processor). We developed for them a high integrity compiler, integrated in a development and test environment, for a non-trivial subset of Pascal, including functions and procedures, and modules for separate compilation .
The software produced with these techniques had a much higher degree of correctness than traditionally developed software. The team leader says:
We believe that the methodology provides us with a high level of confidence in the correctness of the embedded software required to drive high integrity controllers.
publications on DeCCo: