ارائه يك روش رسمي جهت اعتبارسنجي ماشين قلب-ريه

Proposing a Formal Approach for Verification of Heart-Lung Machine

مقدمه: رخداد خطا در سيستم هاي كامپيوتري، مخصوصاً سيستم هايي كه در پزشكي استفاده مي شوند، مي تواند منجر به صدمات جبران ناپذيري شود. بنا بر اين وارسي چنين سيستم هايي اهميت زيادي دارد. چك كردن مدل يكي از روش هايي است كه براي اطمينان از عدم وجود خطا در يك مدل استفاده مي شود. ماشين قلبريه ماشيني است كه در جراحي هايي كه نياز است قلب ساكن باشد به كار مي رود و وظايف قلب و ريه را به عهده مي گيرد. هدف از اين مطالعه ارايه روش رسمي براي اعتبارسنجي ماشين قلب ريه است. مواد و روش ها: عملكرد ماشين قلبريه با استفاده از ابزار UPPAAL كه از ماشين خودكار زماني پشتيباني مي كند مدل شده است. چون در اين ماشين سه مجموعه كار به طور موازي انجام مي شود، كه در سه زيرسيستم ماشين عملكرد كلي سيستم، ماشين تزريق دارو و ماشين تحويل محلول كارديوپلژيا مدل شده است. يافته هاي پژوهش: پس از مدل سازي، با جستجوي جامع روي فضاي حالت مدل، خصوصيات مهم سيستم وارسي شد. وضعيت هايي كه موجب ورود سيستم به حالت هاي ناامن مي شود شناسايي شدند. دسترس پذيري تمام حالات مهم سيستم بررسي شد. در نهايت از بد عمل نكردن سيستم و صحت خصوصيات آن اطمينان لازم كسب گرديد. بحث و نتيجه گيري: مدل سازي يك روش كم هزينه براي مطالعه يك سيستم و ارزيابي واكنش آن به تغييرات محيطي قبل از ساخت آن است. نظر به اهميت ماشين قلبريه در جراحي ها در اين مقاله يك مدل رسمي براي وارسي عملكرد اين ماشين ارائه شده است.

Introduction: error occurrence in computer systems, can lead to irreparable damage, especially those used in medical systems. As a result, verification of such systems is important. Model checking as a method is used to ensure the absence of errors in the model. The heartlung machine is used in surgeries in which heart must stop working and assumes the heart and lungs duties. In this article, a formal approach is to verify the operation of the heartlung machine. Methods: The heartlung machine has been modeled by using the UPPAAL tool which supports time automatic machine, since, this machine do three sets operations in parallel which has been modeled in three subsystems: system overall performance machine, heparin injection machine and cardioplegia solution delivery machine. Finding: After modeling by a complete search on state space of model, the most important characteristics of system were verified. Situations were identified which cause entering the system to unsecure states. The reachability of all important states of the system was investigated. Finally, we ensured about system accuracy features and the system operates correctly. Conclusion: Modelling is a cheap way to study a system and evaluate its reaction to environmental changes before implementation of the system. Considering to importance of heartlung machine in surgeries, in this research a formal model has been presented to verify the operation of this machine.