Model Checking Cyber-Physical Systems using Particle Swarm Optimization

TL;DR

This paper introduces a novel method for model checking cyber-physical systems by transforming the problem into an optimization task and applying particle swarm optimization to efficiently find potential safety violations.

Contribution

It presents a new approach that uses PSO to identify unsafe states in cyber-physical systems, enabling effective bug detection in system controllers.

Findings

Successfully identified safety violations in a Quickbot controller

Demonstrated rapid bug detection using PSO-based model checking

Validated the approach on a real-world cyber-physical system

Abstract

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.