The Robotics Institute

Carnegie Mellon Robotics Institute

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.

Keywords

Verification, Control Systems, Software Testing, Java

Notes

Associated Center(s) / Consortia: Field Robotics Center

Number of pages: 8

Text Reference

Sebastian Scherer, Flavio Lerda, and Edmund M. Clarke, "Model Checking of Robotic Control Systems," Proceedings of the 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS), September, 2005.

BibTeX Reference

@inproceedings{Scherer_2005_5116,
   author = "Sebastian Scherer and Flavio Lerda and Edmund M. Clarke",
   title = "Model Checking of Robotic Control Systems",
   booktitle = "Proceedings of the 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS)",
   month = "September",
   year = "2005",
}

The Robotics Institute

Menu