Automated probabilistic verification of RoboChart using PRISM

This showcase demonstrates how RoboTool is used to automatically verify probabilistic behaviour of RoboChart using PRISM

Jan 26, 2023
Project

Here we demonstrate the verification of a mail delivery robot, documented online.

The theoretical semantics and model-based technologies are well-documented in this paper: “Probabilistic modelling and verification using RoboChart and PRISM”.

This work is also presented at MODELS2022 and the presentation can be found here.

Kangfeng (Randall) Ye
Kangfeng (Randall) Ye
Research Associate (Computer Science)

My research interests include probabilistic modelling and verification using formal specification and verification (both model checking and theorem proving) and model-based engineering.