SMT-Based Verification of Safety-Critical Embedded Control Software

A large fraction of bugs discovered in the design flow of embedded control software (ECS) arises from the control software's interaction with the plant it controls. Traditional formal analysis approaches using interleaved controller-plant reach-set analysis grossly overapproximate the reachable states and does not scale. In this letter, we examine a verification approach that considers a control system with the (possibly nonlinear) plant dynamics and mode switches specified along with the actual control software implementation. Given this input, we generate a bounded-time safety verification problem encoded as satisfiability modulo theories (SMTs) constraints. We leverage delta-decidability over Reals to achieve scalability while verifying the control software.