SMT-based Control Safety Property Checking in Cyber-Physical Systems under Timing Uncertainties

This paper outlines formal methods and design automation techniques for exact checking of control safety and reachability properties of cyber-physical systems (CPS), under timing uncertainties (common deadline miss handling and control update policies). While such checking is often fraught with state-space explosion problems and is hence not scalable. This paper discusses a new joint encoding of control and scheduling behaviors as a satisfiability-modulo-theory (SMT) formulation and a novel abstraction-refinement procedure with incremental solving, to scale the analysis. In addition, we also outline empirical performance results of multiple well-known SMT solvers for this problem. These results can inform practical decision making for large scale control safety verification in the industry.