Using SDVS to Assess the Correctness of Ada Software used in the Midcourse Space Experiment.
AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP
Pagination or Media Count:
This paper gives an overview of a 1993 project performed at The Aerospace Corporation 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.
- Computer Programming and Software
- Space Navigation and Guidance