We presentROSCoq, a framework for developing certifiedCoq programs for robots. ROSCoq subsystems communicate using messages, as they do in the Robot Operating System (ROS). We extend the logic of events to enable holistic reasoning about the cyber-physical behavior of robotic systems. The behavior of the physical world (e.g. Newton’s laws) and associated devices (e.g. sensors, actuators) are specified axiomatically. For reasoning about physics we use and extend CoRN’s theory of constructive real analysis. Instead of floating points, our Coq programs use CoRN’s exact, yet fast computations on reals, thus enabling accurate reasoning about such computations. As an application, we specify the behavior of an iRobot Create. Our specification captures many real world imperfections. We write a Coq program which receives requests to navigate to specific positions and computes appropriate commands for the robot. We prove correctness properties about this system. Using the ROSCoq shim, we ran the program on the robot and provide even experimental evidence of correctness.
CITATION STYLE
Anand, A., & Knepper, R. (2015). ROSCoq: Robots powered by constructive reals. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9236, pp. 34–50). Springer Verlag. https://doi.org/10.1007/978-3-319-22102-1_3
Mendeley helps you to discover research relevant for your work.