Model Checking of Robotic Control Systems - Robotics Institute Carnegie Mellon University

Model Checking of Robotic Control Systems

Sebastian Scherer, Flavio Lerda, and Edmund M. Clarke
Conference Paper, Proceedings of 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS '05), September, 2005

Abstract

Reliable software is important for robotic applications. We propose a new method for the verification of control software based on Java PathFinder, a discrete model checker developed at NASA Ames Research Center. Our extension of Java PathFinder supports modeling of a real-time scheduler and a physical system, defined in terms of differential equations. This approach not only is able to detect programming errors, like null-pointer dereferences, but also enables the verification of control software whose correctness depends on the physical, real-time environment. We applied this method to the control software of a line-following robot. The verified source code, written in Java, can be executed without any modifications on the microcontroller of the actual robot. Performance evaluation and bug finding are demonstrated on this example.

BibTeX

@conference{Scherer-2005-9286,
author = {Sebastian Scherer and Flavio Lerda and Edmund M. Clarke},
title = {Model Checking of Robotic Control Systems},
booktitle = {Proceedings of 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS '05)},
year = {2005},
month = {September},
keywords = {Verification, Control Systems, Software Testing, Java},
}