Formalization of Biological Circuit Block Diagrams for formally analyzing Biomedical Control Systems in pHRI Applications
Adnan Rashid, Sa'ed Abed, Osman Hasan
TL;DR
The paper advocates formal verification of biomedical control systems in pHRI by modeling block diagrams and their dynamics in higher-order logic using HOL Light, and then analyzing the Laplace-domain transfer functions to assess correctness and stability. It develops a formal block-diagram framework with serial, summation, pickoff, and feedback constructs, enabling rigorous TF and stability reasoning for continuous biomedical processes. A real-world case study on ultrafiltration dialysis demonstrates the approach: translating fluid-transport dynamics into HOL Light proofs that a given block diagram yields a transfer function and verifying the associated theorem under explicit assumptions. The work highlights the benefits of deductive reasoning for safety-critical pHRI applications while acknowledging the interactive proof burden and the potential for automation through specialized tactics.
Abstract
The control of Biomedical Systems in Physical Human-Robot Interaction (pHRI) plays a pivotal role in achieving the desired behavior by ensuring the intended transfer function and stability of subsystems within the overall system. Traditionally, the control aspects of biomedical systems have been analyzed using manual proofs and computer based analysis tools. However, these approaches provide inaccurate results due to human error in manual proofs and unverified algorithms and round-off errors in computer-based tools. We argue using Interactive reasoning, or frequently called theorem proving, to analyze control systems of biomedical engineering applications, specifically in the context of Physical Human-Robot Interaction (pHRI). Our methodology involves constructing mathematical models of the control components using Higher-order Logic (HOL) and analyzing them through deductive reasoning in the HOL Light theorem prover. We propose to model these control systems in terms of their block diagram representations, which in turn utilize the corresponding differential equations and their transfer function-based representation using the Laplace Transform (LT). These formally represented block diagrams are then analyzed through logical reasoning in the trusted environment of a theorem prover to ensure the correctness of the results. For illustration, we present a real-world case study by analyzing the control system of the ultrafilteration dialysis process.