From Simulation to Verification of Hybrid and Distributed Systems

Design defects in embedded systems can be elusive and expensive. Effective formal verification of such systems has been a challenge problem for several years. The simulation to verification research program aims to exploit finite data generated from validated simulation tools or from system's executions to provide formal guarantees about uncountable sets of executions. In this talk, I will present two recent developments in this area: (1) a sound and relatively complete simulation-based verification algorithm for nonlinear and switched systems and and (2) an algorithm for checking bounded time safety properties of distributed systems for executions that are consistent with recorded data. The first approach introduces the idea of model annotations, in the spirit of loop invariants, which are used effectively verify bounded time properties of moderately high dimensional systems. The second approach combines static analysis of the system model with dynamically generated data and can be applied to distributed systems with imperfectly synchronized clocks. Along the way, I will mention some of the case studies we have performed.