Accession Number : ADA329347

Title :   Using SDVS to Assess the Correctness of Ada Software used in the Midcourse Space Experiment.

Corporate Author : AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s) : Menas, T. K. ; Bouler, J. M. ; Doner, J. E. ; Filippenko, I. V. ; Levy, B. H.

PDF Url : ADA329347

Report Date : 30 SEP 1994

Pagination or Media Count : 23

Abstract : 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.

Descriptors :   *SOFTWARE ENGINEERING, *COMPUTER PROGRAM VERIFICATION, *ADA PROGRAMMING LANGUAGE, *MIDCOURSE GUIDANCE, GUIDED MISSILE TRACKING SYSTEMS, TELEMETERING DATA, DIGITAL COMMUNICATIONS.

Subject Categories : Computer Programming and Software
      Space Navigation and Guidance

Distribution Statement : APPROVED FOR PUBLIC RELEASE