Model Checking Cyber-Physical Systems using Particle Swarm Optimization
For developers of cyber-physical systems, this provides a new way to find safety violations, but the approach is demonstrated on a single example and lacks comparison to existing methods.
The authors transform model checking of cyber-physical systems into an optimization problem and use particle swarm optimization to find counter-examples. They demonstrate the approach on a Quickbot rover controller, quickly finding a bug that could cause collision.
We present a novel approach to the problem of model checking cyber-physical systems. We transform the model checking problem to an optimization one by designing an objective function that measures how close a state is to a violation of a property. We use particle swarm optimization (PSO) to effectively search for a state that minimizes the objective function. Such states, if found, are counter-examples describing safe states from which the system can reach an unsafe state in one time step. We illustrate our approach with a controller for the Quickbot ground rover. Our PSO model checker quickly found a bug in the controller that could cause the rover to collide with an obstacle.