RoboCertProb: Property Specification for Probabilistic RoboChart Models
This work addresses the need for formal verification in robotics software engineering by enabling property specification and configuration for probabilistic models, though it is incremental as it builds on existing RoboChart and PRISM frameworks.
The authors tackled the problem of specifying quantitative properties for probabilistic robotic systems modeled in RoboChart by introducing RoboCertProb, a property specification language based on PCTL*, and implemented it in RoboTool to automatically generate PRISM properties for formal verification, applying it to analyze software controllers for an industrial painting robot and an agricultural UV-light robot.
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.