Probabilistic modelling and verification using RoboChart and PRISM
Probabilistic modelling and verification using RoboChart and PRISM
复制标题
DOI：
10.1007/s10270-021-00916-8
复制
发表时间：
2021-10
影响因子：
2
通讯作者：
Kangfeng Ye;Ana Cavalcanti;S. Foster;Alvaro Miyazawa;J. Woodcock
中科院分区：
文献类型：
--
作者：
Kangfeng Ye;Ana Cavalcanti;S. Foster;Alvaro Miyazawa;J. Woodcock
RoboChart是一种用于机器人的特定于领域的语言，其独特之处在于它支持通过模型检查和定理证明进行自动验证。由于不确定性是机器人系统的重要组成部分，我们在这里提出了一个扩展RoboChart模型的不确定性，使用概率。该扩展通过一个新的构造丰富了RoboChart状态机的概率：概率连接作为具有概率值的转换源。RoboChart有一个配套工具，称为RoboTool，用于功能和实时行为的建模和验证。我们在这里还提出了一个自动化的技术，在RoboTool中实现，将RoboChart模型转换为PRISM模型进行验证。我们已经扩展了RoboTool的属性语言，以便可以使用受控的自然语言编写时序逻辑中表示的概率属性。
RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.