عنوان پایان‌نامه
درستی یابی سیستمهای توزیع شده شامل مولفه های نامشخص
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 3209;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 81388;کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 3209;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 81388
- تاریخ دفاع
- ۱۶ شهریور ۱۳۹۵
- دانشجو
- رزا عباسی بروجنی
- استاد راهنما
- رامتین خسروی, فاطمه قاسمی اصفهانی
- چکیده
- در حوزه‌ی مهندسی نرم‌افزار مؤلفه‌بنیاد، سیستم شامل چندین مؤلفه با قابلیت استفاده‌ی مجدد است. این مؤلفه‌ها توسط توسعه‌دهندگان مختلف تأمین می‌شوند و عموماً قابل تعویض هستند. هنگام وارسی چنین سیستمی در مقابل خاصیت‌های مد نظر، معمولاً یک سیستم گذار یکپارچه تولید‌شده و ارضای خاصیت برروی آن بررسی می‌گردد. در این پژوهش برآنیم تا همانگونه که از مؤلفه‌های نرم‌افزار مجدداً استفاده می‌کنیم، از نتایج درستی‌یابی نیز مجدداً بهره ببریم. به بیان دیگر هنگامی که یک مؤلفه به سیستم اضافه شده و یا توسط یک نسخه جدیدتر جایگزین می‌شود، بجای تولید سیستم گذار یکپارچه برای کل سیستم، تنها مؤلفه‌ی تغییریافته یا اضافه‌شده را درستی‌یابی کنیم. نظر به گرایشات روزافزون در استفاده از سیستمهای توزیع شده و با توجه به ارتباط ناهمگام در این سیستم‌ها، در این پژوهش ما مسئله‌ی وارسی مدل سیستمهای توزیع‌شده‌ی با ارتباط ناهمگامی را مورد مطالعه قرار می‌دهیم که شامل یک مؤلفه‌ی نامشخص باشند و خاصیت‌هایی را در این سیستم‌ها مورد بررسی قرار می‌دهیم که از نوع ایمنی باشند. راهکار ارائه‌شده بر اساس استدلال فرض-تضمین است: یک فرض را به‌گونه‌ای تولید می‌کنیم که چنانچه مؤلفه‌ی اضافه‌شده یا تغییریافته آن را ارضاء کند، آنگاه خاصیت مدنظر در سیستم ارضاء خواهدشد. تا جایی که می‌دانیم این استدلال مشخصاً تاکنون در مورد محیط‌های ناهمگام توزیع‌شده به کار گرفته نشده‌است. در راهکار ارائه‌شده ابتدا با استفاده از اطلاعاتی که در مورد تعاملات مؤلفه‌های مشخص سیستم موجود است، یک واسط تولید می‌شود که تقریب بالایی از مؤلفه‌ی نامشخص است. این واسط و همچنین مابقی مؤلفه‌های سیستم توسط یک زبان سطح بالا توصیف می‌شوند. اینگونه مدل‌سازی منجر به حذف تعدادی از گام‌های میانی تولید فرض و در نتیجه کاهش محاسبات می‌گردد. نهایتاً سیستم گذار حاصل از ترکیب واسط تولیدی و مابقی مؤلفه‌های سیستم، بدست آمده و به گونه‌ای پالایش می‌شود که ردهای نقض کننده‌ی خاصیت مدنظر از آن حذف شوند و فرض مدنظر تولید گردد. راهکار ارائه شده را بر روی دو مطالعه‌ی موردی سیستم کنترلی توزیع‌شده‌ی یک ربات و سیستم الکترونیک انتقال سرمایه پیاده‌سازی کردیم. با توجه به اینکه در تولید فرض از اطلاعات موجود در مورد تعاملات مؤلفه‌های مشخص سیستم استفاده شد، فرض تولیدی با استفاده از این راهکار به مراتب از فرض تولیدی حاصل از راهکارهای مستقیم تولید فرض، اندازه‌ی کوچکتری خواهد داشت. واژه‌های کلیدی: درستی‌یابی صوری . وارسی مدل . درستی‌یابی سیستمهای درحال تحول . سیستمهای توزیع‌شده‌ی ناهمگام . استدلال فرض-تضمین . سیستمهای گذار برچسب‌دار . خاصیت‌های ایمنی
- Abstract
- Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may results in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. In other words, should we generate the monolithic transition system for the whole system when a new component is added or an existing one is replaced by a newer version, or we can find a way to verify the newly added or modified component? To this aim, we study the problem of model checking component-based asynchronously communicating systems in presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous distributed environments. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by composition of it with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property. We have implemented our approach on two case studies. Our produced assumption is smaller in size than the produced assumption using the state of the art direct approaches. Keywords Formal Verification . Model Checking . Verification of Evolving Systems . Asynchronous Distributed Systems . Assume-Guarantee reasoning . Labeled Transition Systems . Safety Properties
