Timelines and Proofs of Safety Properties in the State Delta Verification System (SDVS).
AEROSPACE CORP EL SEGUNDO CA
Pagination or Media Count:
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.
- Computer Programming and Software