Formalization of Bond Graph using HOL Light

Abstract

Bond graph is a uni ed graphical approach for describing the dynamics of complex engineering and physical systems and is widely adopted in a variety of energy domains, such as, electrical, mechanical, medical, thermal and uid mechanics. Traditionally, these dynamics are analyzed using paper-and-pencil based proof methods and computer-based techniques. However, both of these techniques su er from their inherent limitations, such as, human-error proneness, approximations of results and limited computer resources. Thus, these techniques cannot be trusted for performing the bond graph based dynamical analysis of systems from the safetycritical domains like robotics and medicine. Formal methods in particular, theorem proving, can overcome the shortcomings of the traditional methods and provide an accurate analysis of the systems. It has been used for analyzing the dynamics of engineering and physical systems. In this thesis, we propose to use higher-orderlogic theorem proving for performing the bond graph based analysis of the physical systems. In particular, we provide a formalization of bond graph, which mainly include conversion of a bond graph model to its corresponding mathematical model (state-space model) and veri cation of its various properties, such as, stability. To illustrate the practical e ectiveness of our proposed approach, we present the formal stability analysis of a prosthetic mechatronic hand using HOL Light theorem prover. Moreover, to facilitate a non-HOL user, we encode our formally veri ed stability theorems in MATLAB to perform the stability analysis of the prosthetic mechatronic hand.