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