Control software model checking using bisimulation functions for nonlinear systems

This paper extends a method for integrating source-code model checking with dynamic system analysis to verify properties of controllers for nonlinear dynamic systems. Source-code model checking verifies the correctness of control systems including features that are introduced by the software implementation, such as concurrency and task interleaving. Sets of reachable continuous states are computed using numerical simulation and bisimulation functions. The technique as originally proposed handles stable dynamic systems with affine state equations for which quadratic bisimulation functions can be computed easily. The extension in this paper handles nonlinear systems with polynomial state equations for which bisimulation functions can be computed in some cases using sum-of-squares (SoS) techniques. The paper presents the convex optimizations required to perform control system verification using a source-code model checker, and the method is illustrated for an example of a supervisory control system.