Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties

What if we designed a tool to automatically generate a dynamical transition system for the formal specification of mechanical systems subject to multiple impacts, contacts and discontinuous friction? Such a tool would represent an advance in the description and simulation of these complex systems. This is precisely what this paper offers: Dyverse Rigid Body Toolbox (DyverseRBT). This tool requires a sufficiently expressive computational model that can accurately describe the behaviour of the system as it evolves over time. For this purpose, we propose an alternative abstraction of multi-rigid-body (MRB) mechanical systems with multiple contacts as an extended version of the classical hybrid automaton, which we call MRB hybrid automaton. One of the chief characteristics of the MRB hybrid automaton is the inclusion of computation nodes to encode algorithms to calculate the contact forces. The computation nodes consist of a set of non-dynamical discrete locations, discrete transitions and guards between these locations, and resets on transitions. They can account for the energy transfer not explicitly considered within the rigid-body formalism. The proposed modelling framework is well suited for the automated verification of dynamical properties of realistic mechanical systems. We show this by the falsification of safety properties over the transition system generated by DyverseRBT.

倘若我们设计一款可自动生成针对存在多冲击、接触与非连续摩擦特性的机械系统的形式化规范所需的动态转移系统的工具，将会如何？此类工具将为这类复杂系统的描述与仿真研究带来突破性进展。本文所提供的正是这样一款工具：Dyverse刚体工具箱（Dyverse Rigid Body Toolbox，简称DyverseRBT）。该工具需要具备足够表达能力的计算模型，以精准描述系统随时间演化的行为特性。为此，我们提出一种针对存在多接触场景的多刚体（multi-rigid-body，MRB）机械系统的替代性抽象方法，将其建模为经典混合自动机（hybrid automaton）的扩展形式，我们将其命名为MRB混合自动机。MRB混合自动机的核心特征之一，是纳入了用于编码接触力计算算法的计算节点（computation nodes）。此类计算节点由一系列非动态离散位置（non-dynamical discrete locations）、离散转移（discrete transitions）以及位置间的警戒条件（guards）与转移重置（resets on transitions）操作共同构成。其可涵盖刚体形式化体系中未被显式考虑的能量传递过程。本文提出的建模框架非常适用于对实际机械系统的动态特性开展自动化验证。我们通过在DyverseRBT生成的转移系统上对安全属性进行证伪，验证了这一点。