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
PDF Url : ADA289684
Report Date : 26 FEB 1994
Pagination or Media Count : 27
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