Verification and testing of mobile robot navigation algorithms: A case study in SPARK

Piotr Trojanek, Kerstin I Eder

Research output: Contribution to conferenceConference Paperpeer-review

10 Citations (Scopus)
115 Downloads (Pure)

Abstract

Navigation algorithms are fundamental for mobile robots. While the correctness of the algorithms is important, it is equally important that they do not fail because of bugs in their implementation. Yet, even widely-used robot navigation code lacks proofs of correctness or credible coverage reports from testing. Robot software developers usually point towards the cost of manual verification or lack of automated tools that would handle their code. We demonstrate that the choice of programming language is essential both for finding bugs in the code and for proving their absence. Our re-implementation of three robot navigation algorithms in SPARK revealed bugs that for years have not been detected in their original code in C/C++. For one of the implementations we demonstrate that it is free from run-time errors. Our code and results are available online to encourage uptake by the robot software developers community.
Original languageEnglish
Pages1489-1494
Number of pages6
Publication statusPublished - Sep 2014
EventIEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) - Chicago, Illinois, United States
Duration: 14 Sep 201418 Sep 2014

Conference

ConferenceIEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
CountryUnited States
CityChicago, Illinois
Period14/09/1418/09/14

Fingerprint Dive into the research topics of 'Verification and testing of mobile robot navigation algorithms: A case study in SPARK'. Together they form a unique fingerprint.

Cite this