Verifying Launch Interceptor Routines With the Asymptotic Method.

Abstract

This report describes the results of an exercise in formal program verification conducted at ORA. In this exercise, we started with code written by students at Syracuse University as part of work conducted by Professor Amrit Goel on program development methods. The code was an implementation of the routines of the Launch Interceptor Program (LIP), a specification of a protocol for launching an interceptor missile. This specification was used by Knight and Leveson in a well-known experiment in N-version programming.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 26, 1994
Accession Number
ADA289684

Entities

Organizations

  • Unisys

Tags

Communities of Interest

  • C4I
  • Materials and Manufacturing Processes
  • Sensors
  • Weapons Technologies

DTIC Thesaurus Topics

  • Accuracy
  • Air Force
  • Computations
  • Computer Programming
  • Contractors
  • Contracts
  • Discontinuities
  • Error Analysis
  • Errors
  • Governments
  • Guarantees
  • Numbers
  • Real Numbers
  • Specifications
  • Square Roots
  • Standards
  • Triangles

Fields of Study

  • Computer science

Readers

  • Missile Defense Systems.
  • STEM Education
  • Software Engineering.