Accession Number : ADA291548

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

Corporate Author : AEROSPACE CORP EL SEGUNDO CA

Personal Author(s) : Marcus, L. G. ; Menas, T. K.

PDF Url : ADA291548

Report Date : 30 SEP 1992

Pagination or Media Count : 28

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).

Descriptors :   *COMPUTER PROGRAM VERIFICATION, COMPUTER LOGIC, SEMANTICS, SAFETY, NUMBERS, SYNTAX.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE