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