Accession Number : ADA329536

Title :   Specification and Correctness Proofs of the MSX Ada Software.

Descriptive Note : Technical rept,

Corporate Author : AEROSPACE CORP EL SEGUNDO CA

Personal Author(s) : Menas, T. K. ; Boulder, J. M. ; Doner, John E. ; Levy, Beth H.

PDF Url : ADA329536

Report Date : 30 SEP 1993

Pagination or Media Count : 202

Abstract : The Midcourse Space Experiment (MSX) is a Strategic Defense Initiative Organization program whose primary purpose is to conduct tracking event experiments of targets/phenomena in midcourse. In this report we give a detailed account of the SDVS verification of a modified portion of the MSX tracking processor software. We present a functional overview of this part of the software, discuss and fully annotate our modifications to it, list the SDVS enhancements implemented during the course of the project, and present a proof of correctness of a simple but nontrivial specification.

Descriptors :   *COMPUTER PROGRAMS, *ADA PROGRAMMING LANGUAGE, *MIDCOURSE GUIDANCE, EXPERIMENTAL DATA, SPACE ENVIRONMENTS, STRATEGIC DEFENSE INITIATIVE, COMPUTER PROGRAM VERIFICATION.

Subject Categories : Computer Programming and Software
      Space Navigation and Guidance

Distribution Statement : APPROVED FOR PUBLIC RELEASE