Verifying temporal properties without temporal logic
- 1 January 1989
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 11 (1) , 147-167
- https://doi.org/10.1145/59287.62028
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 automata specifying 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.Keywords
This publication has 10 references indexed in Scilit:
- Complementing deterministic Büchi automata in polynomial timeJournal of Computer and System Sciences, 1987
- Avoiding the state explosion problem in temporal logic model checkingPublished by Association for Computing Machinery (ACM) ,1987
- Adequate proof principles for invariance and liveness properties of concurrent programsScience of Computer Programming, 1984
- The ``Hoare Logic'' of CSP, and All ThatACM Transactions on Programming Languages and Systems, 1984
- Specifying Concurrent Program ModulesACM Transactions on Programming Languages and Systems, 1983
- Temporal logic can be more expressiveInformation and Control, 1983
- Proving Liveness Properties of Concurrent ProgramsACM Transactions on Programming Languages and Systems, 1982
- Impartiality, justice and fairness: The ethics of concurrent terminationPublished by Springer Nature ,1981
- The modal logic of programsPublished by Springer Nature ,1979
- An axiomatic basis for computer programmingCommunications of the ACM, 1969