DocumentCode
2773500
Title
A temporal proof methodology for reactive systems
Author
Manna, Zohar ; Pnueli, Amir
Author_Institution
Dept. of Appl. Math., Weizmann Inst., Rehovot, Israel
fYear
1990
fDate
22-25 Oct 1990
Firstpage
757
Lastpage
773
Abstract
A minimal proof theory that is adequate for proving the main important temporal properties of reactive programs is presented. The properties considered consist of the classes of invariance and response properties. For each of these classes a small set of rules that is complete for verifying properties belonging to the class is given. The application of these rules is illustrated by several examples. Concise presentations of complex proofs using the devices of transition tables and proof diagrams are discussed
Keywords
program verification; invariance; minimal proof theory; proof diagrams; reactive programs; reactive systems; response properties; temporal proof methodology; transition tables; Computer science; Contracts; Control systems; Force control; Industrial plants; Investments; Logic; Mathematics; Operating systems; Quality assurance;
fLanguage
English
Publisher
ieee
Conference_Titel
Information Technology, 1990. 'Next Decade in Information Technology', Proceedings of the 5th Jerusalem Conference on (Cat. No.90TH0326-9)
Conference_Location
Jerusalem
Print_ISBN
0-8186-2078-1
Type
conf
DOI
10.1109/JCIT.1990.128359
Filename
128359
Link To Document