Accession Number:

ADA291548

Title:

Timelines and Proofs of Safety Properties in the State Delta Verification System (SDVS).

Descriptive Note:

Corporate Author:

AEROSPACE CORP EL SEGUNDO CA

Personal Author(s):

Report Date:

1992-09-30

Pagination or Media Count:

28.0

Abstract:

Proofs of typical safety properties of programs in temporal-logic-based systems can be facilitated by the use of two proof rules the Rule of Negation and the w-Induction Rule. We show that each of these rules is valid only on timelines of certain order types the joint use of these two rules is valid only on timelines that are finite, or ordered like the natural numbers. We demonstrate the use of these rules by giving proofs of safety properties of a simple concurrent program in the State Delta Verification System SDVS.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE