کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6874063 | 686062 | 2014 | 15 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Quantitative verification of implantable cardiac pacemakers over hybrid heart models
ترجمه فارسی عنوان
تأیید کمی از پیمانکاران قلب قابل برنامه ریزی بیش از مدل های قلب هیبریدی
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
اتوماتای هیبرید، تأیید کمی، تأیید تقریبی، ضربان قلب
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
We develop a model-based framework which supports approximate quantitative verification of implantable cardiac pacemaker models over hybrid heart models. The framework is based on hybrid input-output automata and can be instantiated with user-specified pacemaker and heart models. For the specifications, we identify two property patterns which are tailored to the verification of pacemakers: “can the pacemaker maintain a normal heart behaviour?” and “what is the energy level of the battery after t time units?”. We implement the framework in Simulink based on the discrete-time simulation semantics and endow it with a range of basic and advanced quantitative property checks. The advanced property checks include the correction of pacemaker mediated Tachycardia and how the noise on sensor leads influences the pacing level. We demonstrate the usefulness of the framework for safety assurance of pacemaker software by instantiating it with two hybrid heart models and verifying a number of correctness properties with encouraging experimental results.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 236, August 2014, Pages 87-101
Journal: Information and Computation - Volume 236, August 2014, Pages 87-101
نویسندگان
Taolue Chen, Marco Diciolla, Marta Kwiatkowska, Alexandru Mereacre,