SMT-Based Verification of Safety-Critical Embedded Control Software
Sunandan Adhikary, Amit Gurung, Jay Thakkar, Antonio Anastasio Bruto da Costa, Soumyajit Dey, Aritra Hazra, Pallab Dasgupta · IEEE Embedded Systems Letters · 2020
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.