Model Checking Cyber-Physical Systems using Particle Swarm Optimization
Systems and Control
2017-03-06 v1
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.
Keywords
Cite
@article{arxiv.1703.01257,
title = {Model Checking Cyber-Physical Systems using Particle Swarm Optimization},
author = {Dung Phan and Scott A. Smolka and Radu Grosu and Usama Mehmood and Scott D. Stoller and Junxing Yang},
journal= {arXiv preprint arXiv:1703.01257},
year = {2017}
}