A system for object code validation

Abstract

In several key safety-critical embedded applications, it has become mandatory to verify the process of translation by compilers since usually compilers are only certified rather than verified. In this paper, we shall describe a methodology and a system for the validation of translation of a safe-subset of Ada to assembly language programs. The work described here is an application of Translation Validation technique to safety-critical programs that are developed using standard software engineering practices using safe subsets of Ada such as SPARK Ada [3]. Our method consists of converting the high level language (HLL) program and its object code to a common semantic representation such as Fair Transition System (FTS) [6], and then establishing that the object code is a refinement of the HLL program. The proof of refinement is performed using STeP (Stanford Temporal Prover) theorem prover. The proposed approach also has the additional advantage that the embedded system remains unaffected by compiler revisions/updates. We conclude with a discussion of our practical experience, effectiveness and further possibilities.