Accession Number : ADA324421

Title :   Continuous Verification by Discrete Reasoning,

Corporate Author : STANFORD UNIV CA

Personal Author(s) : De Alfaro, Luca ; Manna, Zohar

PDF Url : ADA324421

Report Date : SEP 1994

Pagination or Media Count : 29

Abstract : Two semantics are commonly used for the behavior of real time and hybrid systems: a discrete semantics, in which the temporal evolution is represented as a sequence of snapshots describing the state of the system at certain times, and a continuous semantics, in which the temporal evolution is represented by a series of time intervals, and therefore corresponds more closely to the physical reality. Powerful verification rules are known for temporal logic formulas based on the discrete semantics. This paper shows how to transfer the verification techniques of the discrete semantics to the continuous one. We show that if a temporal logic formula has the property of finite variability, its validity in the discrete semantics implies its validity in the continuous one. This leads to a verification method based on three components: verification rules for the discrete semantics, axioms about time, and some temporal reasoning to bring the results together. This approach enables the verification of properties of real-time and hybrid systems with respect to the continuous semantics.

Descriptors :   *VERIFICATION, *REASONING, *SEMANTICS, TIME INTERVALS, REAL TIME, MATHEMATICAL LOGIC, VARIATIONS, HYBRID SYSTEMS.

Subject Categories : Linguistics

Distribution Statement : APPROVED FOR PUBLIC RELEASE