Model Checking Cyber-Physical Systems using Particle Swarm Optimization

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 effectiv...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2017-03
Main Authors: Phan, Dung, Smolka, Scott A, Grosu, Radu, Mehmood, Usama, Stoller, Scott D, Yang, Junxing
Format: Article
Language:English
Subjects:
Controllers
Cyber-physical systems
Logic programming
Particle swarm optimization
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422