Title :
A temporal proof methodology for reactive systems
Author :
Manna, Zohar ; Pnueli, Amir
Author_Institution :
Dept. of Appl. Math., Weizmann Inst., Rehovot, Israel
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;
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
DOI :
10.1109/JCIT.1990.128359
