Accession Number:

ADA289684

Title:

Verifying Launch Interceptor Routines With the Asymptotic Method.

Descriptive Note:

Technical rept.

Corporate Author:

UNISYS CORP RESTON VA RESTON TECHNOLOGY CENTER

Personal Author(s):

Report Date:

1994-02-26

Pagination or Media Count:

27.0

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.

Descriptors:

• *BALLISTIC MISSILE INTERCEPT SYSTEMS
• *INTERCEPTORS
• GUIDED MISSILES
• VERIFICATION
• STUDENTS
• LAUNCHING

Subject Categories:

• Antimissile Defense Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE