Using SDVS to Assess the Correctness of Ada Software used in the Midcourse SpaceExperiment

摘要

This paper gives an overview of a 1993 project performed at The AerospaceCorporation in cooperation with the Johns Hopkins Applied Physics Laboratory to formally verify, using the State Delta Verification System (SDVS), a portion of the Midcourse Space Experiment (MSX) tracking processor software. SDVS is an automated system developed at The Aerospace Corporation for use in formal computer verification. The tracking processor software is written in Ada and 175OA assembly language. The project has been one of the largest experiments in the formal verification of production Ada code. This paper presents (1) an overview of SDVS, (2) a functional overview of a portion of the MSX tracking processor software (the target software), (3) a discussion of the modifications that were made to the MSX software, and (4) a description of the correctness proofs of the modified MSX software and of the two different strategies used in the proofs. The modifications were due primarily to the presence of Ada tasks in the target software.