RSE2023 talk - How to Specify Properties of Probabilistic RoboChart Models

Jim Woodcock will be talking about “How to Specify Properties of Probabilistic RoboChart Models” at the Robotics Software Engineering Symposium 2023, King’s College London.

Abstract: RoboChart is a core notation in the RoboStar framework that brings modern modelling and formal verification technologies to software engineering for robotics. It is a timed, probabilistic domain-specific language and provides a UML-like architectural and state machine modelling. This work presents RoboCertProb for specifying quantitative properties of probabilistic robotic systems modelled in RoboChart. RoboCertProb is the probabilistic extension of RoboCert, a property specification for robotics. RoboCertProb is based on PCTL* and is a subset of the discrete-time part of the Prism property language with extensions to support RoboChart. In addition to property specification, RoboCertProb configures loose constants and uninterpreted functions and operations in RoboChart models. It lets us set up environmental inputs to verify reactive probabilistic systems not directly supported in Prism with its closed-world assumption. The grammar of RoboCertProb is flexible. We implement RoboCertProb in RoboTool for specifying properties and automatically generating Prism properties. We have used it to analyse the behaviour of software controllers for two real-world robots: an industrial painting robot and an agricultural robot for treating plants with UV lights.