Accession Number:

ADA288812

Title:

Safety Properties of Terminating and Nonterminating Ada Programs in the State Delta Verification System (SDVS),

Descriptive Note:

Corporate Author:

AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s):

• Menas, T. K.

Report Date:

1992-09-30

Pagination or Media Count:

41.0

Abstract:

We describe recent enhancements to the implementation of invariance in SDVS, the purpose of the new weaknexttr flag, and enhancements to the omegainduct command. We use these enhancements to SDVS to prove a safety property of both a terminating and a nonterminating Ada program.

Descriptors:

• *COMPUTER PROGRAM VERIFICATION
• *ADA PROGRAMMING LANGUAGE
• *SYSTEM SAFETY
• MODIFICATION
• INVARIANCE

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE