RoboCertProb：概率RoboChart模型的属性规约
RoboCertProb: Property Specification for Probabilistic RoboChart Models
AI总结：
本文提出RoboCertProb，一种基于PCTL*的概率属性规约语言，用于RoboChart模型，支持配置未定义项和环境输入，并在RoboTool中实现以自动生成PRISM属性，已应用于两个真实机器人控制器的验证。
摘要：
RoboChart是RoboStar框架中的核心记号，该框架将现代建模和形式验证技术引入机器人软件工程。RoboChart是一种面向机器人的定时和概率领域特定语言，提供类似UML的架构和状态机建模。本文提出RoboCertProb，用于规约用RoboChart建模的概率机器人系统的定量属性。RoboCertProb的语义基于PCTL*。为了在RoboChart模型上解释RoboCertProb，我们为RoboChart赋予马尔可夫语义（DTMC和MDP），该语义源自其现有的到PRISM语言的转换语义。除了属性规约，RoboCertProb还允许我们配置RoboChart模型中的松散常量和未指定的函数与操作。它使我们能够设置环境输入，以验证反应式概率系统，这类系统在诸如PRISM之类的概率模型检查器中因采用封闭世界假设而不被直接支持。我们在RoboChart的配套工具RoboTool中实现了RoboCertProb，用于规约属性并自动从这些属性生成PRISM属性，从而使用PRISM对RoboChart模型进行形式验证。我们已使用它来分析两个真实机器人的软件控制器行为：一个工业喷漆机器人和一个用紫外线灯处理植物的农业机器人。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
