• Uncertainty modelling in RoboChart
• Probabilistic modelling and verification [RoboChart] using PRISM
  • Probabilistic property language
  • Tool support
• Automated Reasoning for Probabilistic Programs with Theorem Proving
  • Probabilistic designs
  • Probabilistic relations

This poster shows thw work I and my colleagues were or are doing in recent years.

Uncertainty modelling in RoboChart

This is well discussed in Chapter 13: RoboStar Technology: Modelling Uncertainty in RoboChart Using Probability of book Software Engineering for Robotics.

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.

Particularly, I would like to point out some very interesting topics in the chapter:

• Section 2: a discussion of the sources of uncertainty in robotics and the contributions made by modelling. The examples are into six major categories: (1) abstractions of the real world, (2) hardware failures, (3) approximate control algorithms, (4) controller synthesis, (5) motion planning, and (6) self-adaptation.
• The random sample consensus (Ransac) algorithm is presented as a RoboChart model (Section 5.2) and analysed using model checking PRISM (Section 6). A simplified form of the algorithm is also analysed using model checking and a manual proof in Section 7.

Probabilistic modelling and verification [RoboChart] using PRISM

This work is published on SoSyM and can be found here. Several case studies can be found on the probabilistic models on the RoboStar website.

Another industrial related case study for a High Voltage Controller (HVC) of a paint robot can be found here.

• This case study is well analysed and presented in the two papers by Murray et al.
  • Safety Assurance of a High Voltage Controller for an Industrial Robotic System,
  • Safety assurance of an industrial robotic control system using hardware/software co-verification.
• Our analysis using PRISM of this case study hasn’t been published yet.

The full details of our translation rules can be found in our RoboChart manual.

Probabilistic property language

• The probabilistic property language in RoboCert is briefed in the SoSym paper, but full details are given in the manual.
• We don’t have a further publication about the recently updated probabilistic property language and the HVC yet.

Tool support

In order to use this work for verification, we have developed the PRISM plugins for RoboTool. Please follow the guidance in the RoboTool manual to install RoboTool and its plugins for analysis using PRISM.

Automated Reasoning for Probabilistic Programs with Theorem Proving

Denotational semantics for probabilistic programming in UTP

Probabilistic designs

This work is presented in the paper “Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving” published in RAMiCS 2021. My presentation can be found here.

Abstract:

Semantics for nondeterministic probabilistic sequential programs has been well studied in the past decades. In a variety of semantic models, how nondeterministic choice interacts with probabilistic choice is the most significant difference. In He, Morgan, and McIver’s relational model, probabilistic choice refines nondeterministic choice. This model is general because of its predicative-style semantics in Hoare and He’s Unifying Theories of Programming, and suitable for automated reasoning because of its algebraic feature. Previously, we gave probabilistic semantics to the RoboChart notation based on this model, and also formalised the proof that the semantic embedding is a homomorphism, and revealed interesting details. In this paper, we present our mechanisation of the proof in Isabelle/UTP enabling automated reasoning for probabilistic sequential programs including a subset of the RoboChart language. With mechanisation, we even reveal more interesting questions, hidden in the original model. We demonstrate several examples, including an example to illustrate the interaction between nondeterministic choice and probabilistic choice, and a RoboChart model for randomisation based on binary probabilistic choice.

Basically, it is a mechanisation of He at el.’s Deriving probabilistic semantics via the ‘weakest completion’ in Isabelle/UTP, an implementation of UTP in Isabelle/HOL.

Benefits of this work:

• Intrinsically support nondeterminism,
• Reuse the theory of designs in UTP and so its tool: Isabelle/UTP,
• Probabilistic choice is a refinement of nondeterministic choice,
• Total correctness can also be reasoned using current theorems for designs.

We have proved a randomisation algorithm modelled in RoboChart, that is used in the RANSAC algorithm, is truly a uniform distribution with reasoning about total correctness.

The repository for the Isabelle theories can be found here. There are detailed installation guidance.

Probabilistic relations

This work is based on Eric Hehner’s work on “Probabilistic Predicative Programming” and “A probability perspective”.

Our major contributions are

• the introduction of a Iverson Bracket notation to improve the syntax of the language,
• we bridge the semantics gap for recursion using fixed-point theorems, particularly Kleene’s fixed-point theorem,
• we mechanise it in Isabelle/HOL for reasoning.