JavaScript is disabled for your browser. Some features of this site may not work without it.
Verifying Temporal Properties without using Temporal Logic

Author
Alpern, Bowen; Schneider, Fred B.
Abstract
An approach to proving temporal properties of concurrent programs that does not use temporal logic as an inference system is presented. The approach is based on using Buchi automata to specify properties. To show that a program satisfies a given property, proof obligations are derived from the Buchi automaton for that property. These obligations are discharged by devising suitable invariant assertions and variant functions for the program. The approach is shown to be sound and relatively complete. A mutual exclusion protocol illustrates its application.
Date Issued
1987-07Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-848
Type
technical report