Abstract:
A large fraction of bugs discovered in the design flow of Embedded Control Software (ECS) embedded control software arises from the control softwares interaction with the plant it controls. Traditional formal analysis approaches using interleaved controller-plant reach-set analysis grossly over-approximate the reachable states and does not scale. In this article, 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 (SMT) constraints. We leverage ?-decidability over Reals to achieve scalability while verifying the control software.