وارسی مدل ضربان ساز قلب با استفاده از اوپال

سال انتشار: 1394
نوع سند: مقاله کنفرانسی
زبان: فارسی
مشاهده: 668

فایل این مقاله در 6 صفحه با فرمت PDF قابل دریافت می باشد

استخراج به نرم افزارهای پژوهشی:

لینک ثابت به این مقاله:

شناسه ملی سند علمی:

ICIKT07_122

تاریخ نمایه سازی: 22 مهر 1394

چکیده مقاله:

سیستم هایی که نقص در آنها باعث بروز مرگومیر و زیان سنگین اقتصادی شود، سیستم حیاتی نامیده می شود، پس پیاده سازی این سیستم ها با کمینه کردن نقص ها بسیار مهم است. در این مقاله سیستم ضربان ساز قلب تعریف و به صورت بسیار دقیق در سیستم گذار حالت بیان و ضوابط ایمنی آن استخراج می شود. سپس مدل توسط ابزار وارسی مدل اوپال شبیه سازی می شود و ضوابط ایمنی در آن به عنوان ناظر بیان می شوند. با اجرای ضوابط ایمنی، در صورت ارضاءنشدن، محل بروز نقص شناسایی می شود تا با اصلاح، سیستم برای پیاده سازی، آماده شود. ضوابط در این مقاله توسط منطق درخت محاسباتی بیان و در سیستم اعمال شده اند.

نویسندگان

آرش عبداله میرزائی

دانشجوی کارشناسی ارشد مهندسی نرم افزار دانشگاه تربیت مدرس

سعید جلیلی

دانشیار، گروه مهندسی کامپیوتر، دانشگاه تربیت مدرس

محمد فتاحیان

دانشجوی کارشناسی ارشد مهندسی نرم افزار دانشگاه تربیت مدرس

مراجع و منابع این مقاله:

لیست زیر مراجع و منابع استفاده شده در این مقاله را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود مقاله لینک شده اند :
  • Sommerville, Ian. "Software engine ering--9th ed. p. cm." 2011. ...
  • Sriram Radhakri shnan, Varun Sampath, Shilpa Sarode, PVS: Pacemaker Verification ...
  • Drusinsky, Doron. "Runtime monitoring and verification of systems with hidden ...
  • Colombo, Christian, Gordon J. Pace, and Gerardo Schneider. "Safe runtime ...
  • Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. Vol. ...
  • Leungwattanaki t, Watcharin, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu ...
  • Transactions on 40, no. 5 , 2014, 483-501. ...
  • Augusto, Juan Carlos, and Miguel J. Hornos. "Software simulation and ...
  • Software 58 , 2013, 18-34. ...
  • Corno, Fulvio, and Muhammad Sanaullah. "Design-time formal verification for smart ...
  • Larsen, Kim G., Paul Pettersson, and Wang Yi. "Uppaal in ...
  • Love, Charles J. Cardiac pacemakers and defibrillators. Georgetown: Landes Bioscience, ...
  • Schaldach, Max. Electrotherapy of the heart: technical aspects in cardiac ...
  • نمایش کامل مراجع