Timelines and Proofs of Safety Properties in the State Delta Verification System (SDVS).
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).
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 30, 1992
- Accession Number
- ADA291548
Entities
People
- L. G. Marcus
- T. K. Menas
Organizations
- The Aerospace Corporation