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.
