In this paper, we enable automated property verification of deliberative components in robot control architectures. We focus on formalizing the execution context of Behavior Trees (BTs) to provide a scalable, yet formally grounded, methodology to enable runtime verification and prevent unexpected robot behaviors. To this end, we consider a message-passing model that accommodates both synchronous and asynchronous composition of parallel components, in which BTs and other components execute and interact according to the communication patterns commonly adopted in robotic software architectures. We introduce a formal property specification language to encode requirements and build runtime monitors. We performed a set of experiments, both on simulations and on the real robot, demonstrating the feasibility of our approach in a realistic application and its integration in a typical robot software architecture. We also provide an OS-level virtualization environment to reproduce the experiments in the simulated scenario.
翻译:在本文中,我们允许对机器人控制结构中的议事构件进行自动财产核查。 我们侧重于将行为树(BTs)的执行环境正规化,以提供一个可扩展的、但有正式基础的方法,使运行时间的核查能够进行,并防止出乎意料的机器人行为。 为此,我们考虑一种信息传递模式,既包括平行构件的同步和不同步构成,也包括平行构件的同步和不同步构成,BTs和其他构件根据机器人软件结构中常用的通信模式执行和互动。我们引入了正式财产规格语言,用于编码要求和构建运行时间监测器。我们进行了一系列实验,既包括模拟实验,也包括实际机器人实验,展示了我们在现实应用中的方法的可行性,并将其纳入典型的机器人软件结构中。 我们还提供了一个OS级别的虚拟化环境,以便在模拟情景中复制实验。