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.

翻译：RoboChart是RoboStar框架的核心表示法，该框架将现代建模与形式验证技术引入机器人软件工程。作为一种面向机器人的时态与概率领域特定语言，它提供了类似UML的架构与状态机建模能力。本文提出RoboCertProb，用于规约以RoboChart建模的概率机器人系统定量属性。RoboCertProb的语义基于PCTL*。为在RoboChart模型上解释RoboCertProb，我们基于其到PRISM语言的现有转换语义，赋予RoboChart马尔可夫语义（DTMC与MDP）。除属性规约外，RoboCertProb还允许我们配置RoboChart模型中的松散常量及未指定函数与操作。通过设定环境输入，我们得以验证概率模型检验器（如PRISM）因采用封闭世界假设而无法直接支持的反应式概率系统。我们在RoboChart的配套工具RoboTool中实现了RoboCertProb，用于规约属性并自动生成对应的PRISM属性，从而借助PRISM对RoboChart模型进行形式验证。我们已将其应用于分析两台真实机器人的软件控制器行为：一台工业喷涂机器人与一台利用紫外线处理植物的农业机器人。