Verification and testing of mobile robot navigation algorithms: A case study in SPARK
Verification and testing of mobile robot navigation algorithms: A case study in SPARK
复制标题
移动机器人导航算法的验证和测试：以 SPARK 为例
DOI：
10.1109/iros.2014.6942753
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
K. Eder
中科院分区：
文献类型：
--
作者：
P. Trojanek;K. Eder
导航算法是移动机器人的基础。虽然算法的正确性很重要，但同样重要的是，它们不会因为实现中的错误而失败。然而，即使是广泛使用的机器人导航代码也缺乏正确性的证明或来自测试的可信覆盖报告。机器人软件开发人员通常会指出人工验证的成本，或者缺乏自动化工具来处理他们的代码。我们演示了编程语言的选择对于发现代码中的错误和证明它们的存在都是至关重要的。我们在SPARK中重新实现了三种机器人导航算法，发现了多年来在C/ c++原始代码中没有发现的错误。对于其中一个实现，我们演示了它没有运行时错误。我们的代码和结果可在线获得，以鼓励机器人软件开发人员社区采用。
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.
DOI：
10.1007/s10817-009-9149-2
发表时间：
2010-03-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Akbarpour, Behzad;Paulson, Lawrence Charles
通讯作者：
Paulson, Lawrence Charles