Accession Number : ADA262086

Title :   Putting Time Into Proof Outlines.

Descriptive Note : Interim rept.,

Corporate Author : CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE

Personal Author(s) : Schneider, Fred B. ; Bloom, Bard ; Marzullo, Keith

Report Date : 10 MAR 1993

Pagination or Media Count : 33

Abstract : A logic for reasoning about timing properties of concurrent programs is presented. The logic is based on Hoare-style proof outlines and can handle maximal parallelism as well as certain resource-constrained execution environments. The correctness proof for a mutual exclusion protocol that uses execution timings in a subtle way illustrates the logic in action. A soundness proof using structural operational semantics is outlined in the appendix. Concurrent program verification, Timing properties, Safety properties, Real-time programming, Real-time actions, Proof outlines.

Descriptors :   *COMPUTER PROGRAM VERIFICATION, *COMPUTER LOGIC, REASONING, RESOURCES, SEMANTICS, REAL TIME.

Subject Categories : Computer Systems Management and Standards

Distribution Statement : APPROVED FOR PUBLIC RELEASE