TIME2006 Gargantini, Angelo Morzenti, Angelo

Automated Verification of Continuous Time Systems by Discrete Temporal Induction

in International Symposium on Temporal Representation and Reasoning TIME 2006, Budapest, Hungary June 15 - 17, 2006 (2006): 19 -26 ISBN 0-7695-2617-9

We present a temporal framework suitable for the specificationand 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 similarto the one usually found in discrete time temporal logics and can be safely and effectively used in specifications aswell 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, thewell-known thermostat example.

[read the copyright and download the pdf file] [DOI]

My sw links