Accession Number:

ADA329536

Title:

Specification and Correctness Proofs of the MSX Ada Software.

Descriptive Note:

Technical rept,

Corporate Author:

AEROSPACE CORP EL SEGUNDO CA

Report Date:

1993-09-30

Pagination or Media Count:

202.0

Abstract:

The Midcourse Space Experiment MSX is a Strategic Defense Initiative Organization program whose primary purpose is to conduct tracking event experiments of targetsphenomena 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.

Subject Categories:

  • Computer Programming and Software
  • Space Navigation and Guidance

Distribution Statement:

APPROVED FOR PUBLIC RELEASE