Formalization of Bond Graph using Higher-order-logic Theorem Proving

TL;DR

This paper formalizes bond graph analysis using higher-order-logic theorem proving to improve accuracy and reliability in analyzing complex physical systems, demonstrated through stability verification of a prosthetic hand.

Contribution

It introduces a formalization of bond graphs in higher-order-logic theorem proving and applies it to stability analysis of a prosthetic system, enhancing precision over traditional methods.

Findings

Formalization enables accurate stability verification.

HOL Light theorem prover effectively models bond graph dynamics.

MATLAB encoding facilitates non-expert stability analysis.

Abstract

Bond graph is a unified graphical approach for describing the dynamics of complex engineering and physical systems and is widely adopted in a variety of domains, such as, electrical, mechanical, medical, thermal and fluid mechanics. Traditionally, these dynamics are analyzed using paper-and-pencil proof methods and computer-based techniques. However, both of these techniques suffer from their inherent limitations, such as human-error proneness, approximations of results and enormous computational requirements. Thus, these techniques cannot be trusted for performing the bond graph based dynamical analysis of systems from the safety-critical domains like robotics and medicine. Formal methods, in particular, higher-order-logic theorem proving, can overcome the shortcomings of these traditional methods and provide an accurate analysis of these systems. It has been widely used for analyzing the dynamics of engineering and physical systems. In this paper, we propose to use higher-order-logic theorem proving for performing the bond graph based analysis of the physical systems. In particular, we provide formalization of bond graph, which mainly includes functions that allow conversion of a bond graph to its corresponding mathematical model (state-space model) and the verification of its various properties, such as, stability. To illustrate the practical effectiveness of our proposed approach, we present the formal stability analysis of a prosthetic mechatronic hand using HOL Light theorem prover. Moreover, to help non-experts in HOL, we encode our formally verified stability theorems in MATLAB to perform the stability analysis of an anthropomorphic prosthetic mechatronic hand.