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 mechanical systems with multiple contacts as an extended version of the classical hybrid automaton, which we call multi-rigid-body hybrid automaton. One of the chief characteristics of the multi-rigid-body 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.