Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

RoboCertProb: Property Specification for Probabilistic RoboChart Models

Kangfeng Ye, Jim Woodcock

TL;DR

This work presents RoboCertProb for specifying quantitative properties of probabilistic robotic systems modelled in RoboChart, and implements RoboCertProb in an accompanying tool of RoboChart, RoboTool, for specifying properties and automatically generating PRISM properties from them to formally verify RoboChart models using PRISM.

Abstract

RoboChart is a core notation in the RoboStar framework which brings modern modelling and formal verification technologies into software engineering for robotics. It is a timed and probabilistic domain-specific language for robotics 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's semantics is based on PCTL*. To interpret RoboCertProb over RoboChart models, we give a Markov semantics (DTMCs and MDPs) to RoboChart, derived from its existing transformation semantics to the PRISM language. In addition to property specification, RoboCertProb also entitles us to configure loose constants and unspecified functions and operations in RoboChart models. It allows us to set up environmental inputs to verify reactive probabilistic systems not directly supported in probabilistic model checkers like PRISM because they employ a closed-world assumption. We implement RoboCertProb in an accompanying tool of RoboChart, RoboTool, for specifying properties and automatically generating PRISM properties from them to formally verify RoboChart models using PRISM. We have used it to analyse the behaviour of software controllers for two real robots: an industrial painting robot and an agricultural robot for treating plants with UV lights.

RoboCertProb: Property Specification for Probabilistic RoboChart Models

TL;DR

This work presents RoboCertProb for specifying quantitative properties of probabilistic robotic systems modelled in RoboChart, and implements RoboCertProb in an accompanying tool of RoboChart, RoboTool, for specifying properties and automatically generating PRISM properties from them to formally verify RoboChart models using PRISM.

Abstract

RoboChart is a core notation in the RoboStar framework which brings modern modelling and formal verification technologies into software engineering for robotics. It is a timed and probabilistic domain-specific language for robotics 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's semantics is based on PCTL*. To interpret RoboCertProb over RoboChart models, we give a Markov semantics (DTMCs and MDPs) to RoboChart, derived from its existing transformation semantics to the PRISM language. In addition to property specification, RoboCertProb also entitles us to configure loose constants and unspecified functions and operations in RoboChart models. It allows us to set up environmental inputs to verify reactive probabilistic systems not directly supported in probabilistic model checkers like PRISM because they employ a closed-world assumption. We implement RoboCertProb in an accompanying tool of RoboChart, RoboTool, for specifying properties and automatically generating PRISM properties from them to formally verify RoboChart models using PRISM. We have used it to analyse the behaviour of software controllers for two real robots: an industrial painting robot and an agricultural robot for treating plants with UV lights.
Paper Structure (6 sections, 16 equations, 4 figures)

This paper contains 6 sections, 16 equations, 4 figures.

Table of Contents

  1. Introduction
  2. RoboChart
  3. Markov semantics for RoboChart and PCTL* for specification
  4. Markov models: DTMCs and MDPs
  5. Markov semantics for RoboChart
  6. PCTL* for specifying RoboChart properties

Figures (4)

  • Figure 1: The RoboChart model for the simple random walk: data interface SRWIntf, event interface EventIntf, module SRWMod, robotic platform SRWRP, controller SRWCtrl, state machine SRWSTM, and three functions Plus, Minus, and Update.
  • Figure 2: Definition of a Markov state.
  • Figure 3: The semantics of RoboChart transitions in Markov models.
  • Figure 4: The semantics of RoboChart transitions with communication in Markov models.

Theorems & Definitions (3)

  • definition thmcounterdefinition: Discrete-Time Markov chains
  • definition thmcounterdefinition: Cost and rewards
  • definition thmcounterdefinition: Markov decision processes