بخشی از مقاله
چکیده بسیاری از مردم در سراسر جهان دارای دستگاه تنظیم کننده ضربان قلبی که برای کمک به بازیابی ضربان قلب نرمال در قفسه سینه شان قرار گرفته هستند. با این حال این دستگاه بدون مشکل هم نیست و در صورتی که با اشکال مواجه شود ممکن است اثرات جبران ناپذیری را تا سرحد مرگ بر جای بگذارد. دستگاه تنظیم کننده ضربان قلب ریتم ضربان قلب بیمار را کنترل کرده و از بروز بی نظمی های تپش قلب پیشگیری می کند، بنابراین هر نقصی در این نرم افزار باعث بدعمل کردن دستگاه می شود.
با توجه به اهمیت آنچه بیان شد هدف این مقاله درستی یابی عملکرد الگوریتم این دستگاه در تمامی شرایط ممکن است تا از بروز بحران جلوگیری کند. با وارسی رفتار نرم افزار می توان ریسک خرابی را به حداقل رساند. وارسی نرم افزاری به معنای بررسی کردن محدودیتهای کاربران سیستم با کمک سیستم نرم افزاری حین اجراست. در این مقاله وارسی دستگاه تنظیم ضربان بر پایه مدل چکر SMV انجام می شود و خصیصه های حیات و ایمنی که اهمیت بالایی دارد، در آن مورد بررسی قرارگرفته است.
مقدمه
استفاده از دستگاه های پزشکی قابل نصب بر روی بدن درحال افزایش است. طبق گزارش اداره غذا و داروی آمریکا - - FDA ، تعداد دستگاههای پزشکی فروخته شده بین سالهای 2004 تا 2009 افزایشی بالغ بر %56 داشته است در حالیکه دارو در همین مدت تنها %38 رشد داشته است .[1] هدف اصلی دستگاه های پزشکی مراقبت است، به گونه ای که بدون دخالت انسان برای درمان و نیز جلوگیری از پیشامد وضعیت فیزیکی غیرعادی در بدن بیمار استفاده می شود. تجهیزات پزشکی به سه دسته تقسیم می شود. دسته اول تجهیزاتی که کمترین احتمال زیان را برای بیماران دارد شامل لوازم ساده ای چون ادوات جراحی به صورت دستی. تجهیزاتی با احتمال زیان آفرینی بالاتر همچون سوزنهای جراحی و دستگاه تزریق انسولین در دسته دوم قرار می گیرد.
دسته سوم دستگاه هایی که احتمال خطر آفرینی بالاتری دارد یا حتی اگر احتمال خرابی آن کم باشد ولی اثر آن خرابی زیاد است بنابراین مهم است که تضمینی برای عملکرد دقیق آن وجود داشته باشد . دستگاه تنظیم ضربان قلب و دستگاه دریچه قلب مصنوعی از این دسته است. به سبب ارتباطی که این دستگاه ها با بدن بیمار دارد، می تواند وضعیت سلامت بیمار را در هر کجا و حتی به صورت از راه دور پایش کند. این دستگاه ها دارای نرم افزار کاربردی است که فعالیت و رفتار دستگاه را کنترل می کند.
به دلیل پراکندگی و یا دوری بیمارستانها نسبت به بیمار این دستگاه باید دقت در عملکرد را تضمین کند. بین سالهای 2006 تا 2011 بدلیل بد عمل کردن دستگاه ها 2294 مورد خطا و 1154451 مورد اثر جانبی توسط FDA گزارش شده است. بر اساس همین گزارش 92600 مورد باعث جراحات گردید و 4590 مورد مرگ در پی داشت. در1210مورد یعنی %22.9 از تمامی موارد، نرم افزار کاربردی دستگاه مقصر شناخته شد.[1] از راه های کاهش سوء عمل دستگاه استفاده از متد درستی یابی نرم افزار به عنوان آزمایشگر است . [2]
همانطور که بیان شد Pacemaker دستگاهی است که تنظیم ضربان قلب را برعهده دارد. این دستگاه توسط متخصص در زیر پوست بیمار قرار می گیرد تا مراقب بی نظمی ضربان قلب باشد، به این شکل که عضلات قلب را بوسیله تولید پالس منظم تحریک می کند. شکل a1 و b1 ساختار کلی دستگاه را در گذشته و حال نشان می دهد. شکل b1 نشان می دهد که در دستگاه های مدرن امروزی بخش کنترلی و منطقی اضافه شده است که می تواند بواسطه اطلاعاتی که از حسگر ها می گیرد برای عملکرد بهتر دستگاه تصمیم بگیرد.
دستگاه مدرن دارای یک یا تعدادی حسگر است که می تواند تغییرات ناشی از متابولیسم یا فعالیت بدنی را شناسایی کند تا به دستگاه تنظیم کننده ضربان قلب در عملکرد درست کمک کند. باتوجه به اینکه که این دستگاه برای مدت 5 تا 10 سال در بدن بیمار قرار می گیرد لذا باید تضمینی برای کارکرد درست این دستگاه وجود داشته باشد. برای رفع مشکل احتمالی و دادن تضمین مناسب برای عملکرد بهتر باید به روش وارسی استاتیک یا وارسی پویا عملیات درستی یابی را انجام داد [2] که در مقاله حاضر به دلیل برتری روش دوم عملیات وارسی به شیوه Runtime verification و با کمک زبان SMV برای اولین بار انجام شده است و خصیصه های حیات و ایمنی در آن به خوبی ارضا شده است.
مفاهیم درستی یابی - Verification -
در بحث اعتباریابی یا Validation به کلیت یک مساله پرداخته می شود درحالیکه در وارسی یا همان درستی یابی به بررسی درستی اجزا مساله اهمیت داده می شود. یعنی در درستی یابی با بیان مساله و خصیصه ها سروکار داریم و هدف نشان دادن این است که خصیصه های مساله برقرار است یا خیر. برای بررسی درستی یابی چند روش وجود دارد:
: Static Verification -1 بیان مساله را بدهند و بدون اینکه بیان مساله را تبدیل به کد کنیم ثابت کنیم خصیصه برقرار است یا خیر که به آن اثبات ریاضی نیز گویند.
: Dynamic Verification -2 صورت مساله به کد تبدیل می شود و در اجرای برنامه - پیاده سازی توصیف - بررسی می کنند که آیا خصیصه برقرار است یا خیر. درستی یابی پویا خود به دو دسته تقسیم می شوند:
الف-اجرای برنامه به شکل آزمایشی - - Software testing ب- اجرای برنامه در محیط واقعی - Runtime verification - هرجا صحبت از verification می شود باید از روشی استفاده شود که مبنای ریاضی داشته باشد که در توصیف ریاضی یا از منطق استفاده می شود یا از جبر. در روش آزمایشی - software testing - با مبنای ریاضی روبرو نیستیم بلکه با کد برنامه روبرو هستیم و در واقع اجرای برنامه با داده های آزمایشی بررسی می شوند هر چند تولید داده های آزمون که نرم افزار را به حد کافی تست کند مشکل است. در حالیکه در static verification و Runtime verification با مبنای ریاضی روبرو هستیم. مبنای ریاضی یا توصیف ریاضی را توصیف رسمی - Formal specification - می گویند. البته در روش Runtime verification اثبات ریاضی وجود ندارد بلکه رابطه های ریاضی با اجرای برنامه بررسی می شوند.
به چند روش می توان یک مساله را بیان یا توصیف کرد: formal، semi-formal و . informal در واقع informal زبانهایی هستند که هم نحو و هم معنا در آن غیر دقیق است همچون زبانهای محاوره که در این مدل زبان می توان چند برداشت داشت پس برای توصیف اصلا مناسب نیستند. Semi-formal زبانهایی هستند که نحو در آن تا حدی دقیق است اما معنا در آن غیر دقیق است لذا با اینکه در توصیف استفاده می شود اما قابل اثبات نیست مثل فلوچارت و .UML و اما formal زبانهایی اند که هم نحو و هم معنا در آن دقیق است و قابل اثبات است و برای اثبات ها در سیستم های حیاتی از formal استفاده می شود.
منظور از سیستمهای حیاتی سیستمی است که اگر اشتباه کند ممکن است جان انسان به خطر بیفتد و هزینه های مالی زیادی در پی داشته باشد مثل نرم افزارهای پزشکی که نرم افزار دستگاه تنظیم ضربان قلب یکی از آنهاست. پس چنانچه بخواهیم درستی یک مساله را ثابت کنیم فقط formal استفاده می شود زیرا منطق و جبر دارای قضیه ها و روابطی هستند که به وسیله آن ها می توان درستی بیان خود را نشان داد. اما semi-formal و informal فاقد مبنای ریاضی هستند بنابراین اثبات بیان ممکن نیست.
