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

    Research output: Contribution to journalArticlepeer-review

    Abstract

    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.
    Original languageEnglish
    Number of pages37
    JournalMathematical and Computer Modelling of Dynamical Systems
    DOIs
    Publication statusPublished - 29 Aug 2017

    Keywords

    • Hybrid systems
    • Hybrid automata models
    • Design automation
    • Computational methods
    • Computer simulation
    • Automated verification
    • Complex behaviours
    • Systems with impacts and friction
    • Dynamical systems
    • Bounded model checking

    Fingerprint

    Dive into the research topics of 'Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties'. Together they form a unique fingerprint.
    • Electromagnetic Sensing Group

      Peyton, A., Fletcher, A., Daniels, D., Conniffe, D., Podd, F., Davidson, J., Anderson, J., Wilson, J., Marsh, L., O'Toole, M., Watson, S., Yin, W., Regan, A., Williams, K., Rana, S., Khalil, K., Hills, D., Whyte, C., Wang, C., Hodgskin-Brown, R., Dadkhahtehrani, F., Forster, S., Zhu, F., Yu, K., Xiong, L., Lu, T., Zhang, L., Lyu, R., Zhu, R., She, S., Meng, T., Pang, X., Zheng, X., Bai, X., Zou, X., Ding, Y., Shao, Y., Xia, Z. & Zhang, Z.

      1/10/04 → …

      Project: Research

    Cite this