Accession Number : ADA262848


Title :   A Temporal Proof Methodology for Reactive Systems,


Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE


Personal Author(s) : Manna, Zohar ; Pnueli, Amir


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a262848.pdf


Report Date : Feb 1993


Pagination or Media Count : 39


Abstract : The paper presents a minimal proof theory which is adequate for proving the main important temporal properties of reactive programs. The properties we consider consist of the classes of invariance, response, and precedence properties. For each of these classes we present a small set of rules that is complete for verifying properties belonging to this class. We illustrate the application of these rules on several examples. We discuss concise presentations of complex proofs using the devices of transition tables and proof diagrams.


Descriptors :   *COMPUTATIONS , *COMPUTER PROGRAM VERIFICATION , METHODOLOGY , VERIFICATION , THEORY , PROBLEM SOLVING , DIAGRAMS , INVARIANCE , RESPONSE , OPERATING SYSTEMS(COMPUTERS) , EMBEDDING , TRANSITIONS


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE