Formalization of Biological Circuit Block Diagrams for formally analyzing Biomedical Control Systems in pHRI Applications

TL;DR

This paper introduces a formal method using higher-order logic and theorem proving to analyze biomedical control systems in pHRI applications, aiming for more accurate and verified results than traditional manual or computational approaches.

Contribution

It presents a novel formalization of biomedical control system block diagrams using HOL Light theorem prover for rigorous analysis and verification.

Findings

Formal models of control systems are constructed in HOL Light.

The approach improves accuracy and verification of biomedical control systems.

A case study on ultrafiltration dialysis demonstrates the method's applicability.

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.