Specification and Correctness Proofs of the MSX Ada Software.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 30, 1993
Accession Number
ADA329536

Entities

People

  • Beth H. Levy
  • J. M. Boulder
  • John E. Doner
  • T. K. Menas

Organizations

  • The Aerospace Corporation

Tags

Communities of Interest

  • Materials and Manufacturing Processes
  • Space

DTIC Thesaurus Topics

  • Abstracts
  • Application Software
  • Artificial Satellites
  • Assembly Languages
  • Boundaries
  • Coding
  • Computer Programming
  • Computer Science
  • Computers
  • Debugging
  • Engineering
  • Language
  • Lisp Programming Language
  • Notation
  • Spacecraft
  • Standards
  • Two Dimensional

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Missile Defense Systems.

Technology Areas

  • Space