Robostar technology: Modelling uncertainty in robochart using probability

Jim Woodcock*, Simon Foster, Alexandre Mota, Kangfeng Ye

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapter


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 languageEnglish
Title of host publicationSoftware Engineering for Robotics
PublisherSpringer International Publishing AG
Number of pages53
ISBN (Electronic)9783030664947
ISBN (Print)9783030664930
Publication statusPublished - 5 Jul 2021

Bibliographical note

Publisher Copyright:
© Springer Nature Switzerland AG 2021. All rights reserved.

Cite this