Thirteenth International Symposium on Temporal Representation and Reasoning (TIME'06)
Automated Verification of Continuous Time Systems by Discrete Temporal Induction
Budapest, Hungary
June 15-June 17
ISBN: 0-7695-2617-9
DOI Bookmark:
http://doi.ieeecomputersociety.org/10.1109/TIME.2006.8
We present a temporal framework suitable for the specification and verification of safety properties of real time hybrid systems. We show that, given suitable assumptions (like non Zenoness and left continuity) continuous time can be discretized by introducing a next operator that is similar to the one usually found in discrete time temporal logics and can be safely and effectively used in specifications as well as in verification. The proofs of properties can be conducted in a deductive style, and can be easily automated, especially when they are based on induction. We validate this approach by applying it to a simple hybrid system, the well-known thermostat example.
Citation:
Angelo Gargantini, Angelo Morzenti, "Automated Verification of Continuous Time Systems by Discrete Temporal Induction," time, pp.19-26, Thirteenth International Symposium on Temporal Representation and Reasoning (TIME'06), 2006
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||