عنوان پایان‌نامه
توصیف رسمی و وارسی دستگاه تنظیم کننده ضربان قلب با استفاده از Z و N Model
- رشته تحصیلی
- مهندسی کامپیوتر- آلگوریتم ها و محاسبات
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه پردیس یک فنی شماره ثبت: 7..;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 43767
- تاریخ دفاع
- ۱۱ مهر ۱۳۸۸
- دانشجو
- پیمان فیضیان
- استاد راهنما
- علی معینی
- چکیده
- با توجه به ماهیت حیاتی دستگاههای پزشکی و پیچیدگی نرم افزارهای به کار رفته در آنها ، طراحی قابل اعتماد و عاری از خطای این گونه دستگاهها از اهمیت والایی برخوردار است. به همین خاطر وجود راهکاری برای اثبات درستی عملکرد و انطباق نرم افزار با استانداردها و ملزومات طراحی ضروری به نظر می رسد. برای رفع این نیاز از دسته ای از تکنیکهای ریاضی موسوم به روشهای رسمی در توصیف ، توسعه و راستی آزمایی نرم افزارها استفاده می شود. در این پایان نامه با استفاده از روشهای رسمی و ابزارهایی که در اختیار ما قرار می دهند ، مرحله طراحی نرم افزار کنترل کننده یک تنظیم کننده ضربان قلب را طی می کنیم. ابتدا با استفاده از زبان Z مجموعه ای از توصیفات غیررسمی موجود از عملکرد سامانه را به یک توصیف رسمی تبدیل می کنیم. سپس با استفاده از ابزار Z/Eves به Syntax Checking ، Domain Checking و Type Checking توصیف می پردازیم. در مرحله بعد با استفاده از تشابه ساختاری بسترهای Z و NModel و تکنیکهای پالایش داده ای و رفتاری ، به انتقال مدل ضربان ساز از محیط Z به محیط NModel می پردازیم. NModel بستری است مبتنی بر C# و .NET که امکانات زیادی برای مدل سازی سامانه ها و راستی آزمایی آنها در اختیار ما قرار می دهد. در نهایت با استفاده از ابزارهای بستر NModel، در جهت راستی آزمایی مدل نهایی ، مشخصات ایمنی و حیات آن را بررسی می کنیم. نشان خواهیم داد که بکارگیری Z در توصیف رسمی سامانه مذکور، کمک شایانی در لحاظ نمودن کلیه نیازمندیها در مدل می نماید و راستی آزمایی و ایمنی و حیات با اطمینان کافی مورد بررسی قرار می گیرند
- Abstract
- Considering the life critical nature of the medical devices and the complexity of the software used in them, reliable and error-free design of such systems is highly valuable. Therefor a mechanism to prove the correct function of the software along its correspondence with the project requirements seems necessary. To fulfil this, group of mathematical techniques, namely formal methods, are used to specify, develop and verify softwares. In this thesis, we are going to specify a cardiac pacemaker using formal methods and their related tools. First we formally specify the informal requirements document using Z language. Then we use the Z/Eves tool for syntax checking, domain checking and type checking of the specifications. Using the refinement techniques and structural similarity between the Z and NModel frameworks, we transform the model to the NModel framework. NModel is a framework based on C# and .NET which facilitates most of the model checking and verification processes. Finally we explore the resulting model, using NModel, and check the safety and liveness properties as a part of verification process.
