Specification and Correctness Proofs of the MSX Ada Software.
AEROSPACE CORP EL SEGUNDO CA
Pagination or Media Count:
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.
- Computer Programming and Software
- Space Navigation and Guidance