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 δ-decidability over Reals to achieve scalability while verifying the control software.