面向pHRI应用中生物医学控制系统形式化分析的生物电路框图形式化
Formalization of Biological Circuit Block Diagrams for formally analyzing Biomedical Control Systems in pHRI Applications
AI总结：
本文提出在pHRI场景下用HOL Light定理证明器对生物医学控制系统框图进行形式化建模与演绎推理，并以超滤透析控制为例验证方法有效性。
摘要：
物理人机交互（pHRI）中生物医学系统的控制对于实现期望行为起着关键作用，其方式是确保整个系统内子系统的预期传递函数和稳定性。传统上，生物医学系统的控制方面一直使用人工证明和基于计算机的分析工具进行分析。然而，由于人工证明中的人为错误以及基于计算机的工具中未经验证的算法和舍入误差，这些方法提供的结果不准确。我们主张使用交互式推理（通常称为定理证明）来分析生物医学工程应用中的控制系统，特别是在物理人机交互（pHRI）的背景下。我们的方法涉及使用高阶逻辑（HOL）构建控制组件的数学模型，并在HOL Light定理证明器中通过演绎推理对其进行分析。我们提出以框图表示的形式对这些控制系统进行建模，框图表示进而利用相应的微分方程及其基于拉普拉斯变换（LT）的传递函数表示。然后，在定理证明器可信环境中通过逻辑推理对这些形式化表示的框图进行分析，以确保结果的正确性。为了说明，我们通过分析超滤透析过程的控制系统，展示了一个真实世界的案例研究。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
