A System for Object Code Validation

In several key safety-critical embedded applications, it has become mandatory to verify the process of translation by compilers since usually compilers are only certi ed rather than veri ed. 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 re nement of the HLL program. The proof of re nement is performed using STeP (Stanford Temporal Prover) theorem prover. The proposed approach also has the additional advantage that the embedded system remains unaected by compiler revisions/updates. We conclude with a discussion of our practical experience, eectiveness and further possibilities