Formalization of bond graph using higher-order-logic theorem proving

Area of Science:

• Engineering
• Computer Science
• Formal Methods

Background:

• Bond graphs are a graphical method for analyzing complex system dynamics across various fields.
• Traditional analysis methods (paper-and-pencil, computational) have limitations including errors, approximations, and high computational costs.
• These limitations make traditional methods unsuitable for safety-critical systems in robotics and medicine.

Purpose of the Study:

• To propose and formalize the use of higher-order-logic theorem proving for bond graph-based dynamical analysis.
• To develop functions for converting bond graphs to state-space models and verifying system properties like stability.
• To demonstrate the practical application and effectiveness of this formal approach.

Main Methods:

• Formalization of bond graphs using higher-order-logic theorem proving.
• Development of functions for automated conversion to state-space models.
• Implementation of stability verification for physical systems.
• Application of HOL Light theorem prover for formal stability analysis of a prosthetic mechatronic hand.
• Encoding verified theorems in MATLAB for accessibility to non-experts.

Main Results:

• Successful formalization of bond graphs and their conversion to state-space models.
• Demonstrated formal verification of system properties, specifically stability.
• Practical application showcased through the stability analysis of a prosthetic mechatronic hand.
• MATLAB encoding of verified theorems to facilitate broader use.

Conclusions:

• Higher-order-logic theorem proving provides a robust and accurate alternative to traditional methods for bond graph analysis.
• The proposed formalization and verification approach enhances the reliability of dynamical analysis, especially for safety-critical systems.
• The integration with MATLAB makes advanced formal methods more accessible for analyzing complex systems like prosthetic devices.