A Formal Verification Methodology for DDD Mode Pacemaker Control Programs
المؤلفون المشاركون
Shuja, Sana
Jabeen, Shaista
Nawarathna, Dharmakeerthi
Srinivasan, Sudarshan K.
المصدر
Journal of Electrical and Computer Engineering
العدد
المجلد 2015، العدد 2015 (31 ديسمبر/كانون الأول 2015)، ص ص. 1-10، 10ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2015-09-01
دولة النشر
مصر
عدد الصفحات
10
التخصصات الرئيسية
تكنولوجيا المعلومات وعلم الحاسوب
الملخص EN
Pacemakers are safety-critical devices whose faulty behaviors can cause harm or even death.
Often these faulty behaviors are caused due to bugs in programs used for digital control of pacemakers.
We present a formal verification methodology that can be used to check the correctness of object code programs that implement the safety-critical control functions of DDD mode pacemakers.
Our methodology is based on the theory of Well-Founded Equivalence Bisimulation (WEB) refinement, where both formal specifications and implementation are treated as transition systems.
We develop a simple and general formal specification for DDD mode pacemakers.
We also develop correctness proof obligations that can be applied to validate object code programs used for pacemaker control.
Using our methodology, we were able to verify a control program with millions of transitions against the simple specification with only 10 transitions.
Our method also found several bugs during the verification process.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Shuja, Sana& Srinivasan, Sudarshan K.& Jabeen, Shaista& Nawarathna, Dharmakeerthi. 2015. A Formal Verification Methodology for DDD Mode Pacemaker Control Programs. Journal of Electrical and Computer Engineering،Vol. 2015, no. 2015, pp.1-10.
https://search.emarefa.net/detail/BIM-1068163
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Shuja, Sana…[et al.]. A Formal Verification Methodology for DDD Mode Pacemaker Control Programs. Journal of Electrical and Computer Engineering No. 2015 (2015), pp.1-10.
https://search.emarefa.net/detail/BIM-1068163
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Shuja, Sana& Srinivasan, Sudarshan K.& Jabeen, Shaista& Nawarathna, Dharmakeerthi. A Formal Verification Methodology for DDD Mode Pacemaker Control Programs. Journal of Electrical and Computer Engineering. 2015. Vol. 2015, no. 2015, pp.1-10.
https://search.emarefa.net/detail/BIM-1068163
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-1068163
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر