生物电路框图形式化化用于 pHRI 应用中生物医学控制系统的形式化分析
计算机科学中的逻辑
2025-01-03 v1
摘要
在物理人机交互 (pHRI) 中的生物医学系统控制，对于确保整体系统中各子系统的预期传递函数和稳定性，发挥着关键作用。传统上，生物医学系统的控制方面使用手动证明和计算机分析工具进行分析。然而，这些方法由于手动证明中的人为错误以及计算机工具中的未验证算法和舍入误差，导致结果不准确。我们认为应使用交互式推理（通常称为定理证明）来分析生物医学工程应用中的控制系统，特别是物理人机交互 (pHRI) 的语境中。我们的 метод论涉及使用高阶逻辑 (HOL) 构造控制组件的数学模型，并通过 HOL Light 定理证明器中的演绎推理进行分析。我们提议将这些控制系统建模为其框图表示，这些框图表示最终利用相应的微分方程及其基于拉普拉斯变换 (LT) 的传递函数表示。随后，这些形式化表示的框图将在定理证明器中可信环境下的逻辑推理中进行分析，以确保结果的正确性。为进行说明，我们通过分析 ultrafiltration 透析过程的控制系统来呈现一个真实案例研究。
引用
@article{arxiv.2501.00541,
title = {Formalization of Biological Circuit Block Diagrams for formally analyzing Biomedical Control Systems in pHRI Applications},
author = {Adnan Rashid and Sa'ed Abed and Osman Hasan},
journal= {arXiv preprint arXiv:2501.00541},
year = {2025}
}
备注
11th International Conference on Mechatronics and Robotics Engineering (ICMRE), Lille, France, 2025