Combining Control and Data Abstraction in the Verification of Hybrid Systems

This paper addresses the verification of hybrid systems built as the composition of a discrete software controller interacting with a physical environment exhibiting a continuous behavior. The goal is to attack the problem of the combinatorial explosion of discrete states that may happen if a complex software controller is considered. It proposes as a solution to extend an existing abstract interpretation technique, namely dynamic partitioning, to hybrid systems described in a symbolic formalism. Dynamic partitioning allows us finely tune the tradeoff between precision and efficiency in a reachability analysis. It shows the effectiveness of the approach by a case study that combines a nontrivial controller specified in the synchronous dataflow programming language Lustre with its physical environment.