Carnegie Mellon University
Browse
file.pdf (1.77 MB)

Model Checking of Robotic Control Systems

Download (1.77 MB)
journal contribution
posted on 2005-09-01, 00:00 authored by Sebastian SchererSebastian Scherer, Flavio Lerda, Edmund M Clarke

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.

History

Date

2005-09-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC