Title :
Time-aware relational abstractions for hybrid systems
Author :
Mover, Sergio ; Cimatti, Alessandro ; Tiwari, Anish ; Tonetta, Stefano
Author_Institution :
FBK, Trento, Italy
fDate :
Sept. 29 2013-Oct. 4 2013
Abstract :
Hybrid Systems model both discrete switches and continuous dynamics and are suitable to represent embedded systems where discrete controllers interact with a physical plant. Relational abstraction is a new approach for verifying hybrid systems. In relational abstraction, the continuous dynamics in each location of the hybrid system is abstracted by a binary relation that relates the current value of the continuous variables with all future values of the variables that are reachable after a time elapse (continuous) transition. The abstract system is an infinite-state system, which can be verified using k-induction or abstract interpretation. Existing techniques for computing relational abstractions are time-agnostic: they do not construct any relationship between the state variables and the time elapsed during the continuous evolution. Time-agnostic abstractions cannot verify timing properties. We present a technique to compute a time-aware relational abstraction for verifying (timing-related) safety properties of cyber-physical systems. We show the effectiveness of the new abstraction on several case studies on which the previous techniques fail.
Keywords :
continuous systems; control engineering computing; discrete systems; formal verification; reachability analysis; abstract interpretation; abstract system; binary relation; continuous dynamics; continuous transition; continuous variables; cyber-physical systems; discrete controllers; discrete switch; embedded systems; hybrid system verification; hybrid systems; infinite-state system; k-induction; physical plant; time elapse transition; time-agnostic abstraction; time-aware relational abstraction; timing properties; timing-related safety property verification; Abstracts; Automata; Eigenvalues and eigenfunctions; Encoding; Equations; Mathematical model; Safety; Abstraction; Formal Methods; Hybrid Systems; Verification;
Conference_Titel :
Embedded Software (EMSOFT), 2013 Proceedings of the International Conference on
Conference_Location :
Montreal, QC
DOI :
10.1109/EMSOFT.2013.6658592