Semi-formal approach for validating compiler for safety critical software in airborne systems

For safety critical systems, porting the correct object code to perform the safety function is very critical. So apart from verifying the embedded software at hardware, software and system levels, safety critical systems need to be tested and validated even at the object code level [1,2,3] (ref: DO 178, Section 6.4.4.2). This paper proposes a novel semi-formal approach for validating compiler used for safety critical software for airborne systems. The novel approach is demonstrated as a case study for Microtec cross-compiler used for generating the object code for Motorola 68060 for indigenously developed Stall warning and aircraft interface computer system software. Program Analysis technique is used to validate the cross-compiler. The technique is incorporated in an in-house tool which integrates the manual knowledge database to carry out the compiler validation. This tool provides partial automation of the verification process which will be used to provide proof as per the RTCA DO-178B guidelines [3].