A challenging research direction in robotics is dealing with uncertainty, which arises when a robot lacks vital and accurate information that it needs to operate satisfactorily. Thrun et al. [1] identify five sources of uncertainty:
The physical world is unpredictable.
Sensors are subject both to physical laws (they have limited range and can’t see through walls) and are sensitive to noise.
Motor actuators suffer from control noise and wear-and-tear.
Models abstract underlying physical processes of a robot and its environment, and model errors are a source of uncertainty.
Control algorithms sacrifice accuracy in order to compute in real time.
All of these factors give rise to uncertainty and a modern approach to robotic development must address this phenomenon.
RoboChart is a diagrammatic, domain-specific notation for modelling robotic controllers with their hardware platforms and operating environments [2]. It is designed to be usable by robotics practitioners and has first-class primitives for describing real-time and probabilistic behaviour.
We outline the probabilistic denotational semantics for RoboChart and show how models are analysed using the Prism probabilistic model checker [3] and the Isabelle automated theorem prover [4]. We illustrate this using a RoboChart model of a robust pose-estimation algorithm, based on Ransac (random-sample consensus) [5], that gives a probabilistic guarantee of accurately determining a robot’s current pose. We conclude with a discussion of future research directions. The talk complements others on verification and certification of robotic systems and their development, simulation, and deployment.
[1] Sebastian Thrun, Wolfram Burgard, and Dieter Fox. Probabilistic robotics: Intelligent robotics and autonomous agents, MIT Press, (2005)
[2] Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, Jon Timmis, and Jim Woodcock. RoboChart: modelling and verification of the functional behaviour of robotic applications, Software and Systems Modeling 18(5):3097-3149 2019
[3] Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of Probabilistic Real-Time Systems, Ganesh Gopalakrishnan and Shaz Qadeer (eds), Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, July 14-20, 2011. Springer, Lecture Notes in Computer Science 6806, 585-591, 2011
[4] Simon Foster, Frank Zeyda, and Jim Woodcock. Isabelle/UTP: A Mechanised Theory Engineering Framework, David Naumann (ed.), Unifying Theories of Programming - 5th International Symposium, UTP 2014, Singapore, May 13, 2014. Springer, Lecture Notes in Computer Science 8963, 21–41, 2015
[5] Martin A. Fischler and Robert C. Bolles. Random Sample Consensus: A Paradigm for Model Fitting with Applications to Image Analysis and Automated Cartography. Comm. ACM. 24(6):381-395 1981
