Home/Model Checking of Robotic Control Systems

Model Checking of Robotic Control Systems

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

Download Publication (PDF)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author’s copyright. These works may not be reposted without the explicit permission of the copyright holder.

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 Reference
@conference{Scherer-2005-9286,
title = {Model Checking of Robotic Control Systems},
author = {Sebastian Scherer and Flavio Lerda and Edmund M. Clarke},
booktitle = {Proceedings of the 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS)},
keyword = {Verification, Control Systems, Software Testing, Java},
school = {Robotics Institute , Carnegie Mellon University},
month = {September},
year = {2005},
address = {Pittsburgh, PA},
}
2017-09-13T10:43:13+00:00