|
|
مجله دانشگاه علوم پزشکی ایلام، جلد ۲۳، شماره ۳، صفحات ۸۴-۹۶
|
|
|
| عنوان فارسی |
ارائه یک روش رسمی جهت اعتبارسنجی ماشین قلب-ریه |
|
| چکیده فارسی مقاله |
مقدمه: رخداد خطا در سیستم های کامپیوتری، مخصوصاً سیستم هایی که در پزشکی استفاده می شوند، می تواند منجر به صدمات جبران ناپذیری شود. بنا بر این وارسی چنین سیستم هایی اهمیت زیادی دارد. چک کردن مدل یکی از روش هایی است که برای اطمینان از عدم وجود خطا در یک مدل استفاده می شود. ماشین قلب-ریه ماشینی است که در جراحی هایی که نیاز است قلب ساکن باشد به کار می رود و وظایف قلب و ریه را به عهده می گیرد. هدف از این مطالعه ارایه روش رسمی برای اعتبارسنجی ماشین قلب- ریه است. مواد و روش ها: عملکرد ماشین قلب-ریه با استفاده از ابزار UPPAAL که از ماشین خودکار زمانی پشتیبانی می کند مدل شده است. چون در این ماشین سه مجموعه کار به طور موازی انجام می شود، که در سه زیرسیستم ماشین عملکرد کلی سیستم، ماشین تزریق دارو و ماشین تحویل محلول کاردیوپلژیا مدل شده است. یافته های پژوهش: پس از مدل سازی، با جستجوی جامع روی فضای حالت مدل، خصوصیات مهم سیستم وارسی شد. وضعیت هایی که موجب ورود سیستم به حالت های ناامن می شود شناسایی شدند. دسترس پذیری تمام حالات مهم سیستم بررسی شد. در نهایت از بد عمل نکردن سیستم و صحت خصوصیات آن اطمینان لازم کسب گردید. بحث و نتیجه گیری: مدل سازی یک روش کم هزینه برای مطالعه یک سیستم و ارزیابی واکنش آن به تغییرات محیطی قبل از ساخت آن است. نظر به اهمیت ماشین قلب-ریه در جراحی ها در این مقاله یک مدل رسمی برای وارسی عملکرد این ماشین ارائه شده است. |
|
| کلیدواژه‌های فارسی مقاله |
|
|
| عنوان انگلیسی |
Proposing a Formal Approach for Verification of Heart-Lung Machine |
|
| چکیده انگلیسی مقاله |
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 heart-lung 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 heart-lung machine. Methods: The heart-lung 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 heart-lung machine in surgeries, in this research a formal model has been presented to verify the operation of this machine. |
|
| کلیدواژه‌های انگلیسی مقاله |
|
|
| نویسندگان مقاله |
رضا رافع | reza rafeh
sardasht square, faculty of engineering, arak university, arak, iran
اراک،میدان سردشت، دانشکده فنی و مهندسی دانشگاه اراک
سازمان اصلی تایید شده: دانشگاه اراک (Arak university)
فاطمه یوسفی فرد |
islamic azad university, arak branch
دانشگاه آزاد اسلامی واحد اراک
سازمان اصلی تایید شده: دانشگاه اراک (Arak university)
سیده زینب حسینی کب | seyedeh zeinab hosseini کب
arak university
اراک،میدان سردشت، دانشکده فنی و مهندسی دانشگاه اراک
سازمان اصلی تایید شده: دانشگاه آزاد اسلامی اراک (Islamic azad university of arak)
|
|
| نشانی اینترنتی |
http://sjimu.medilam.ac.ir/browse.php?a_code=A-10-1522-1&slc_lang=fa&sid=fa |
| فایل مقاله |
فایلی برای مقاله ذخیره نشده است |
| کد مقاله (doi) |
|
| زبان مقاله منتشر شده |
fa |
| موضوعات مقاله منتشر شده |
|
| نوع مقاله منتشر شده |
1 |
|
|
|
برگشت به:
صفحه اول پایگاه |
نسخه مرتبط |
نشریه مرتبط |
فهرست نشریات
|