Abstract
RoboChart is a UML-like language designed for modelling autonomous and mobile robots. It includes timed and probabilistic primitives. In this chapter, we discuss first why we need probability by surveying how we use it in designing robots. To illustrate our approach, we focus on the verification of probabilistic robotic algorithms for pose estimation. We verify a model-fitting algorithm: random sample consensus (Ransac). This is a popular algorithm, representative of a class of particle-filter algorithms. We analyse the aspects of the algorithm and show how to model-check properties and how to get stronger guarantees using a program logic. Our contributions are a survey of probabilistic robotic applications and an approach to verifying probabilistic algorithms developed using RoboStar technology.
| Original language | English |
|---|---|
| Title of host publication | Software Engineering for Robotics |
| Publisher | Springer International Publishing AG |
| Pages | 413-465 |
| Number of pages | 53 |
| ISBN (Electronic) | 9783030664947 |
| ISBN (Print) | 9783030664930 |
| DOIs | |
| Publication status | Published - 5 Jul 2021 |
Bibliographical note
Publisher Copyright:© Springer Nature Switzerland AG 2021. All rights reserved.