Paper Info
Title
Time-aware relational abstractions for hybrid systems
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.
Year
DOI
Venue
2013
10.1109/EMSOFT.2013.6658592
Embedded Software
Keywords
Field
DocType
relational abstraction,continuous evolution,abstract system,hybrid system,time-aware relational abstraction,continuous variable,cyber-physical system,continuous dynamic,embedded system,new abstraction,abstraction,formal methods,hybrid systems,verification,formal verification
Abstraction,Abstract interpretation,Computer science,Binary relation,Real-time computing,Theoretical computer science,State variable,Physical plant,Formal methods,Hybrid system,Distributed computing,Formal verification
Conference
ISBN
Citations 
PageRank 
978-1-4799-1443-2
11
0.49
References 
Authors
27
4
Name
Order
Citations
PageRank
Sergio Mover121815.23
Alessandro Cimatti25064323.15
Ashish Tiwari31630106.62
Stefano Tonetta457341.61