Time-Aware Relational Abstractions for Hybrid Systems
Sergio Mover, Fbk Trento, Ashish Tiwari, Stefano Tonetta · 2015
Hybrid Systems model both discrete switches and continu-ous dynamics and are suitable to represent embedded sys-tems where discrete controllers interact with a physical plant. Relational abstraction is a new approach for verifying hy-brid systems. In relational abstraction, the continuous dy-namics 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) transi-tion. 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 can-not verify timing properties. We present a technique to compute a time-aware rela-tional abstraction for verifying (timing-related) safety prop-erties of cyber-physical systems. We show the effectiveness of the new abstraction on several case studies on which the previous techniques fail. Categories and Subject Descriptors C.3 [Special-purpose and application-based systems]: Real-time and embedded systems; D.2.4 [Software verifi-cation]: Formal methods