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