loading...
Automated Verification of Continuous Time Systems by Discrete Temporal Induction
Budapest, Hungary June 15-June 17
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2006.8Thirteenth International Symposium on ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Angelo Gargantini, Universit? di Bergamo, Italy
Angelo Morzenti, Politecnico di Milano, Italy
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.