2025-11-23T00:40:16.980980

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

Rashid, Abed, Hasan
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.
academic

تشكيل رسوم بيانية كتل الدوائر البيولوجية للتحليل الرسمي لأنظمة التحكم الطبية الحيوية في تطبيقات التفاعل البشري الفيزيائي

المعلومات الأساسية

  • معرّف الورقة: 2501.00541
  • العنوان: تشكيل رسوم بيانية كتل الدوائر البيولوجية للتحليل الرسمي لأنظمة التحكم الطبية الحيوية في تطبيقات التفاعل البشري الفيزيائي
  • المؤلفون: عدنان رشيد (جامعة العلوم والتكنولوجيا الوطنية، باكستان)، سائد عابد (جامعة الكويت)، عثمان حسن (جامعة العلوم والتكنولوجيا الوطنية، باكستان)
  • التصنيف: cs.LO (المنطق في علوم الحاسوب)
  • تاريخ النشر: 31 ديسمبر 2024 (نسخة أولية من arXiv)
  • رابط الورقة: https://arxiv.org/abs/2501.00541

الملخص

تقدم هذه الورقة منهجية تحليل رسمية قائمة على إثبات النظريات التفاعلية لمعالجة مشاكل التحكم في الأنظمة الطبية الحيوية في التفاعل البشري الفيزيائي (pHRI). تعاني الإثباتات اليدوية وأدوات التحليل الحاسوبية التقليدية من الأخطاء البشرية وعدم موثوقية الخوارزميات. تستخدم هذه الورقة المنطق من الدرجة الأعلى (HOL) لبناء نماذج رياضية لمكونات التحكم، وتجري تحليل الاستدلال الاستنتاجي من خلال مثبت نظريات HOL Light. تقوم الطريقة بنمذجة أنظمة التحكم كتمثيلات رسوم بيانية، مستخدمة المعادلات التفاضلية ودوال النقل القائمة على تحويل لابلاس، وتتحقق من فعالية الطريقة من خلال دراسة حالة لعملية الترشيح الفائق.

السياق البحثي والدافع

تعريف المشكلة

  1. المشكلة الأساسية: يفتقر تحليل التحكم في الأنظمة الطبية الحيوية في التفاعل البشري الفيزيائي إلى طرق تحقق رسمية موثوقة
  2. قيود الطرق الموجودة:
    • الإثباتات اليدوية عرضة للأخطاء البشرية، خاصة عند التعامل مع الأنظمة الكبيرة والمعقدة
    • الأدوات القائمة على الحاسوب (مثل Maple و MATLAB و Mathematica) تحتوي على خوارزميات غير موثقة وأخطاء تقريب عددي
    • قد تتجاهل الافتراضات الحرجة المطلوبة للتحليل الرياضي

أهمية البحث

  • تتفاعل الأنظمة الطبية الحيوية مباشرة مع جسم الإنسان وتتحمل مسؤولية الوظائف الحيوية، مما يجعل موثوقيتها وسلامتها حاسمة
  • قد تؤدي أعطال النظام إلى تشخيص خاطئ وعلاج غير مناسب وحتى مخاطر الحياة
  • تنطوي أنظمة pHRI على اتصال فيزيائي مباشر أو غير مباشر بين الإنسان والآلة، مما يزيد من مخاطر السلامة
  • هناك حاجة ماسة إلى تقنيات تحقق صارمة لضمان التشغيل الصحيح لأنظمة التحكم

الدافع البحثي

نظراً للطبيعة الحرجة للسلامة في الأنظمة الطبية الحيوية، لا يمكن للطرق التحليلية التقليدية توفير ضمانات موثوقية كافية، مما يستدعي بشكل عاجل منهجية تحقق رسمية تضمن صحة نتائج التحليل.

المساهمات الأساسية

  1. اقتراح إطار عمل تحليل رسمي لأنظمة التحكم الطبية الحيوية قائم على إثبات النظريات التفاعلية، باستخدام نمذجة المنطق من الدرجة الأعلى لمكونات التحكم
  2. إنشاء طريقة تمثيل رسمية لرسوم بيانية الدوائر البيولوجية، تشمل كتل البناء الأساسية مثل التسلسل والتوازي والعقد الجمعية ونقاط التفرع والتغذية الراجعة
  3. تحقيق تحويل رسمي من المعادلات التفاضلية في المجال الزمني إلى دوال النقل في المجال الترددي، بناءً على نظرية تحويل لابلاس
  4. توفير التحقق من حالة عملية لعملية الترشيح الفائق، مما يثبت قابلية تطبيق الطريقة في الأنظمة الطبية الحيوية الحقيقية
  5. ضمان الصرامة الرياضية لنتائج التحليل، من خلال بيئة موثوقة لمثبت النظريات

شرح الطريقة

تعريف المهمة

الإدخال: نموذج المعادلات التفاضلية لنظام التحكم الطبي الحيوي ومعاملات النظام الإخراج: نتائج التحقق الرسمي من دالة النقل وتحليل الاستقرار القيود: يجب أن يستوفي النظام شروط وجود تحويل لابلاس والقابلية للتفاضل المتقطع

الأساس النظري

مثبت نظريات HOL Light

  • مثبت نظريات تفاعلي مطبق على أساس OCaml
  • يتمتع بنواة موثوقة صغيرة (حوالي 400 سطر من كود OCaml)
  • تم التحقق من صحته من خلال مشروع CakeML
  • يوفر دعماً غنياً لنظرية حساب التفاضل والتكامل متعدد المتغيرات

تشكيل تحويل لابلاس

التعريف 3: تشكيل تحويل لابلاس في HOL Light

⊢def ∀s g. ltfm g s = integ {x| &0 ≤ x} (λx. cexp (--(s ∗ Cx x)) ∗ g x)

التعريف 4: شروط وجود تحويل لابلاس

⊢def ∀s g. lexst g s ⇔ (∀b. g pcws_diff_on interval [&0,b]) ∧ (∃M a. Re s > a ∧ eord g M a)

تشكيل مكونات الرسم البياني

التكوين المتسلسل

التعريف 6: دالة النقل لـ N مكون متسلسل

⊢def ∀Ai. ser [A1; A2; ...; AN] = ∏(i=1 to N) Ai

عقدة الجمع

التعريف 7: جمع مكونات متعددة

⊢def ∀Ai. summ [A1; A2; ...; AN] = ∑(i=1 to N) Ai

نقطة التفرع

التعريف 8: التمثيل الرسمي لتفرع الإشارة

⊢def ∀α Ai. pick_point [A1; A2; ...; AN] = [α ∗ A1; α ∗ A2; ...; α ∗ AN]

نظام التغذية الراجعة

التعريف 9: فرع التغذية الراجعة

⊢def ∀α β n. branch α β n = ∏(i=0 to n) series_comp [α;β]

التعريف 10: كتلة التغذية الراجعة

⊢def ∀α β. feedback_block α β = series_comp [α; ∑(k=0 to ∞) branch α β k]

نقاط الابتكار التقني

  1. إطار عمل تشكيل كامل: أول تطبيق لإثبات النظريات التفاعلية على تحليل أنظمة التحكم الطبية الحيوية
  2. تعيين صارم من الرسم البياني إلى دالة النقل: إنشاء مراسلة رسمية من تمثيل الرسم البياني إلى النموذج الرياضي
  3. نمذجة دقيقة للأنظمة المستمرة: بالمقارنة مع طرق فحص الحالة المنفصلة، يمكن التقاط السلوك المستمر بدقة
  4. تصميم عام: يدعم التركيبات المتسلسلة والمتوازية لعدد عشوائي من المكونات والهياكل التغذية الراجعة المعقدة

إعداد التجربة

نظام الحالة: عملية الترشيح الفائق

  • وصف النظام: عملية الترشيح الفائق في غسيل الكلى، المستخدمة لإزالة السوائل الزائدة من جسم المريض
  • مكونات النظام: ثلاث وحدات (الذراع والجذع والساق)، بأحجام VA(t) و VT(t) و VL(t) على التوالي
  • معاملات التحكم: ثوابت النقل kTA و kTL و kA و kL، معدل الترشيح الفائق UFR(t)

النموذج الرياضي

معادلة ديناميكا نقل السوائل بين الذراع والجذع:

dVA(t)/dt = -kAVA(t) + kTAVT(t)  (المعادلة 2)

التطبيق الرسمي

التعريف 12: التمثيل الرسمي لديناميكا نقل السوائل

⊢def diff_eq_at VT VA t kA kTA ⇔ 
    diff_eq_nord 1 (olst_diff_eq_at kA) VA t = 
    diff_eq_nord 0 (ilst_diff_eq_at kTA) VT t

نتائج التجربة

التحقق من النظريات الرئيسية

النظرية 1: دالة النقل لنظام نقل السوائل بين الذراع والجذع

⊢thm ∀kA kTA s. s + Cx kA ≠ Cx (&0) ⇒ 
    blk_diag_rep_at kA kTA = (Cx kTA)/(s + Cx kA)

النظرية 2: المراسلة بين النموذج الديناميكي ودالة النقل

⊢thm ∀kA kTA VT VA s. [شروط الافتراض A1-A8] ⇒ 
    ltfm VA s / ltfm VT s = Cx(&1)/(s + Cx kA)

شروط التحقق

  • A1-A2: قيود الإيجابية للثوابت النقل (&0 < kA ∧ &0 < kTA)
  • A3-A4: وجود المشتقات وتحويل لابلاس
  • A5: شروط أولية صفرية
  • A6: تحقيق معادلة الديناميكا
  • A7-A8: عدم صفرية مقام دالة النقل

التحقق من مزايا الطريقة

  1. تنظيم الشروط الصريحة: يتم تحديد وتحقق جميع شروط التحليل بوضوح
  2. التكميم العام: تنطبق النظريات بشكل عام على جميع قيم المعاملات
  3. معالجة الأنظمة المستمرة: القدرة على نمذجة العمليات المستمرة مثل نقل السوائل بدقة
  4. موثوقية النتائج: ضمان الصرامة الرياضية من خلال مثبت النظريات

الأعمال ذات الصلة

تطبيق الطرق الرسمية في الهندسة

  • أنظمة التحكم في تشكيل المركبات ذاتية القيادة 5
  • تحليل المرشحات التناظرية الخطية 6
  • التحكم في المركبات تحت الماء بدون طيار 7
  • مرشحات معالجة الصور 8
  • الأنظمة الفيزيائية المعلوماتية 9

تشكيل الأنظمة البيولوجية

  • الأعمال السابقة للمؤلفين في البيولوجيا الاصطناعية 10: تحليل تنشيط البروتين والتثبيط والتنشيط الذاتي
  • تحليل المستقبلات متعددة المدخلات في التعرف على الخلايا السرطانية وتشخيص الأمراض

نقاط الابتكار في هذه الورقة

  • أول تطبيق لإثبات النظريات التفاعلية على أنظمة التحكم الطبية الحيوية في pHRI
  • طريقة تشكيل رسم بياني متخصصة للأنظمة الطبية الحيوية
  • مختلفة تماماً عن الأعمال السابقة في مجال التطبيق، على الرغم من استخدام تمثيل الرسم البياني

الخلاصة والنقاش

الاستنتاجات الرئيسية

  1. تم بنجاح إنشاء إطار عمل تحليل رسمي لأنظمة التحكم الطبية الحيوية، بناءً على المنطق من الدرجة الأعلى وإثبات النظريات
  2. تم التحقق من جدوى الطريقة في الأنظمة الحقيقية، من خلال حالة عملية الترشيح الفائق
  3. توفير نتائج تحليل أكثر موثوقية من الطرق التقليدية، مع تجنب الأخطاء البشرية وعدم اليقين الخوارزمي
  4. إنشاء تعيين تشكيل صارم من المعادلات التفاضلية إلى دوال النقل

القيود

  1. متطلبات التفاعل البشري عالية: تتطلب عملية إثبات النظريات تدخلاً بشرياً كبيراً، وقد تكون مرهقة وتستغرق وقتاً طويلاً
  2. منحنى التعلم حاد: يتطلب من المستخدمين امتلاك معرفة متخصصة بالطرق الرسمية وإثبات النظريات
  3. درجة الأتمتة محدودة: على الرغم من إمكانية تطوير استراتيجيات أتمتة، لا تزال بحاجة إلى توجيه يدوي
  4. تغطية الحالات محدودة: تم التحقق من حالة واحدة فقط من عملية غسيل الكلى، مما يتطلب المزيد من التحقق من التطبيقات العملية

الاتجاهات المستقبلية

  1. تطوير استراتيجيات أتمتة أكثر: مثل استراتيجية TF_TAC_UF الأوتوماتيكية المذكورة في الورقة
  2. توسيع دراسات الحالة: التحقق من المزيد من أنواع أنظمة التحكم الطبية الحيوية
  3. دمج طرق تحليل أخرى: الجمع بين تحليل الاستقرار وتحليل الثوبة وغيرها
  4. تحسين سلسلة الأدوات: تطوير واجهات مستخدم أكثر سهولة وأدوات مساعدة

التقييم المتعمق

المزايا

  1. قوة الابتكار المنهجي: أول تطبيق لطرق تشكيل صارمة في مجال تحليل أنظمة التحكم الطبية الحيوية
  2. أساس نظري متين: بناءً على مثبت نظريات HOL Light الناضج ونظرية تحويل لابلاس
  3. صرامة رياضية عالية: يتم التحقق من جميع النتائج من خلال استدلال منطقي صارم
  4. قيمة عملية واضحة: بالنسبة للأنظمة الطبية الحيوية الحرجة للسلامة، يتمتع التحقق الرسمي بأهمية كبيرة
  5. اكتمال الإطار: توفير عملية كاملة من نمذجة المعادلات التفاضلية إلى تحليل دالة النقل

أوجه القصور

  1. التحقق التجريبي محدود: توفير حالة واحدة فقط من الترشيح الفائق، مع نقص التحقق التجريبي الأوسع
  2. عدم كفاية اعتبارات الكفاءة: لم يتم مناقشة التعقيد الحسابي للطريقة وقضايا الكفاءة في التطبيقات العملية بالتفصيل
  3. مقارنة غير كافية مع الطرق التقليدية: نقص المقارنة الكمية مع أدوات مثل MATLAB/Simulink
  4. درجة أتمتة منخفضة نسبياً: على الرغم من الإشارة إلى استراتيجيات الأتمتة، لم يتم عرض تأثيرها بالتفصيل
  5. نقاش غير كافٍ حول نطاق التطبيق: نقص التحليل المنهجي لأنواع الأنظمة الطبية الحيوية المناسبة

التأثير

  1. المساهمة الأكاديمية: فتح اتجاه جديد لتطبيق الطرق الرسمية في الهندسة الطبية الحيوية
  2. القيمة العملية: توفير أداة تحليل أكثر موثوقية للأنظمة الطبية الحيوية الحرجة للسلامة
  3. الأهمية المنهجية: إظهار كيفية تطبيق النظرية الرياضية المجردة على مشاكل الهندسة الملموسة
  4. الاندماج متعدد التخصصات: تعزيز التعاون بين علوم الحاسوب ونظرية التحكم والهندسة الطبية الحيوية

السيناريوهات المناسبة

  1. الأنظمة الحرجة للسلامة: مناسبة بشكل خاص للأجهزة الطبية ذات متطلبات الموثوقية العالية جداً
  2. الموافقة التنظيمية: يمكن استخدامها للتحقق الرسمي من الأجهزة الطبية والموافقة التنظيمية
  3. تصميم النظام: إجراء التحقق الرياضي الصارم في مرحلة التصميم
  4. التدريس والبحث: كحالة نموذجية لتطبيق الطرق الرسمية في الهندسة

المراجع

1 J Fernández, C Galindo, J Barbacho, and A Luque. Automatic Control Systems in Biomedical Engineering, 2018.

2 O. Hasan and S. Tahar. Formal Verification Methods. In Encyclopedia of Information Science and Technology, Third Edition, pages 7162–7170. IGI Global, 2015.

13 A. Rashid and O. Hasan. Formalization of Lerch's Theorem using HOL Light. Journal of Applied Logics—IFCoLog Journal of Logics and their Applications, 5(8):1623–1652, 2018.

16 C. H. Houpis and S. N. Sheldon. Linear Control System Analysis and Design with MATLAB. CRC Press, 2013.

التقييم الشامل: هذه ورقة رائدة في مجال التخصصات المتقاطعة، تطبق بنجاح طرق التحقق الرسمية على تحليل أنظمة التحكم الطبية الحيوية. على الرغم من وجود مجال للتحسن في التحقق التجريبي والتطبيق العملي، فإن مساهماتها النظرية وقيمتها المنهجية جديرة بالتقدير، وتضع أساساً مهماً للبحث اللاحق في هذا المجال.