ASE2 CARD CATALOG ENTRY

Instructions:

• Scroll forward and backward through this Card Catalog Entry to view it.
• Strike the PRINT button on your browser to print this Card Catalog Entry.
• Go to the FILE SPECS section of this Card Catalog Entry to find out where the associated directories and files are. If they are on this Website, you can transfer to them by clicking on the indicated hyperlinks. Note: the FILE SPECS hyperlink in this bullet will take you directly to the FILE SPECS section.
• Use the FIND command of your browser to search this Card Catalog Entry.
• Click here to go to the Card Catalog Taxonomy.
• Click here to go to the Card Catalog Index. Warning: the index file is large, so this may take a while on slower systems.
• Click here to go to the Title Page.

---

ASSET OVERVIEW

UNIT NAME

PENDEMO

VERSION

STARS-AC-A023/006/00, 26-FEB94

ORIGIN

ASSET

REVIEW CODE

OK

INET ADDRESS

librarian@source.asset.com

AUTHOR

Douglas Hoover, Maryl M. McCullough
UNISYS

RIGHTS

Approved for public release; distribution unlimited

COPYRIGHT

1994 UNISYS

LOCATION

ASSET
PAL

---

CLASSIFICATION

KEYWORDS

Penelope
Software Measurement
Measurement, Software

INDEX

Hoover, Douglas
McCullough, Maryl M.
Unisys

DEPENDENCIES

None

SEE ALSO

SHORT DESCRIPTION

An exercise in formal program verification

TAXONOMY

Documents

Software Verification

Penelope

Verification Demonstration

---

FILE LISTING

FILE SPECS

Click here to enter Asset Directory/transfer Asset File(s): ../../ase02_01/docs/penelope/pendemo

DIRECTORY DISPLAY

Follow path to see directory

---

ABSTRACT

Verifying Launch Interceptor Routines with the Asymptotic Method Using Penelope

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.

The exercise consisted of specifying the routines using the asymptotic method and verifying a number of them using Penelope. The asymptotic method is a relatively simple approach to specification and verification of numerical programs that takes account of numerical error without quantifying it. It is important to take account of numerical error, even if it is small, because even a small error can change the result of a numerical program if it is a discontinuous function of the input. All non-constant discrete-valued (integer or Boolean) functions of real number arguments are discontinuous, and many real-valued functions appearing in geometry are discontinuous at certain degenerate configurations. When a specification, like the LIP specification, does not say anything quantitative about permissible error, the asymptotic method is the appropriate way to formalize that specification. The asymptotic method exposes problems of this kind, without requiring any more work than is necessary for that purpose. Classical error analysis will expose similar problems and give quantitative measures of how bad they are, but also requires more effort and expertise.

This verification exercise had the following results.

• A number of weaknesses in the specification were found regarding the treatment of near-degenerate geometrical situations. We adopted what seemed to be a reasonable solution to these problems and adapted the programs accordingly.
• Some problems were found with the programs in that they used discontinuous formulas to compute continuous quantities, creating problems dealing with exceptions and permitting unpredictable results near singularities.
• A few other errors were found in the programs. In particular, in one place an incorrect formula was used and in another uninitialized variables were read.
• Considering the effect of error cast doubt on the method that Knight and Leveson used to test programs for faults, and on their evaluation of some program variants as faulty.
• We outlined a development method for numerical programs that would appear to address the problems exposed by this verification exercise.

---

REVISION HISTORY

STARS-AC-A023/006/00  1 June 94  Initial release to the PAL

---

RELEASE NOTICE

Approved for public release; Distribution unlimited

---

DISCLAIMER

This documentation is provided "AS IS" and without any expressed or
implied warranties whatsoever.  No warranties as to performance,
merchantability, or fitness for a particular purpose exist.
The user must assume the entire risk and liability of using this
document.  In no event shall any person or organization of people be
held responsible for any direct, indirect, consequential or
inconsequential damages or lost profits.

---

ASE CARD CATALOG ENTRY NAVIGATION

• Go to Title Page
• Go to Taxonomy
• Go to Index (warning: the index file is large, so this may take a while on slower systems)
• Go to Top of this Page

Powered by the Generic Web-Based Reuse Library (GWRL)