عنوان پایان‌نامه
وارسی مبتنی بردیاگرام سیستم های واکنشی تر کیبی وپارامتریک با استفاده از منطق زمانی
- رشته تحصیلی
- مهندسی کامپیوتر- آلگوریتم ها و محاسبات
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه پردیس یک فنی شماره ثبت: 2.;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 39391
- تاریخ دفاع
- ۱۳ مهر ۱۳۸۷
- دانشجو
- فرید علاقمند
- استاد راهنما
- علی معینی
- چکیده
- سیستم های واکنشی، سیستم هایی هستند که تعامل پیوسته ای با محیط اطراف خویش داشته و به دلیل به کارگیری آنها در موارد حیاتی وضروری، اطمینان از کارکرد صحیح و ایمن آنها امری ضروری می باشد. از مهمترین روش های کسب اطمینان از کارکرد صحیح این سیستم ها، استفاده از روش های رسمی راستی آزمایی می باشد. روش های راستی آزمایی در حالت کلی به دو دسته الگوریتمی و استنتاجی تقسیم می شوند. در روش های راستی آزمایی مبتنی بر دیاگرام، از ترکیب هر دو روش، به منظور بهره گیری از مزایای هردو استفاده می شود. در این پایان نامه ابتدا به معرفی سیستم های واکنشی ترکیبی و پارامتریک، روش های راستی آزمایی آنها و چالش های پیش رو می پردازیم و برخی از الگوریتم های موجود برای راستی آزمایی آنها را ارائه می کنیم. سپس الگوریتمی مبتنی بر دیاگرام، جهت راستی آزمایی سیستم های واکنشی ترکیبی ارائه می کنیم. ایده اصلی الگوریتم، مدل سازی سیستم های ترکیبی با آتامای مربعی می باشد، چرا که تحلیل آتاماتای مربعی، تصمیم پذیر بوده و الگوریتم های متنوعی برای آن ارائه شده است. در الگوریتم پیشنهادی ابتدا برای توصیف رسمی خصوصیات مورد راستی آزمایی سیستم، از منطق زمانی خطی استفاده کرده و سپس سیستم واکنشی مورد نظر را با دیاگرام آتاماتای مربعی مدل می کنیم .در نهایت به تحلیل دیاگرام و آتاماتای حاصل می پردازیم. تحقیقات پیشین در زمینه راستی آزمایی سیستم های ترکیبی، عمدتا محدود به سیستم های خطی بوده و اکثر آنها با استفاده از روش های پیچیده ریاضیاتی، به تحلیل مستقیم معادلات دیفرانسیلی می پردازند. در حالیکه در این پایان نامه ابتدا سیستم مورد نظر را با آتاماتای مربعی مدل کرده و سپس به راستی آزمایی مدل حاصل می پردازیم. از مزایای روش فوق، قابل اعمال بودن آن برروی سیستم های خطی و غیر خطی، مبتنی بر دیاگرام بودن آن و بهره گیری از تحقیقات پیشین در زمینه تحلیل آتاماتای مربعی می باشد.
- Abstract
- Reactive systems are those systems that have an ongoing interaction with their environment and since they are used in critical applications, ensuring their safety is necessary. Formal analysis techniques can be used to verify their safety property. There are basically two approaches to verification of reactive systems: the algorithmic approach in one hand and the deductive approach on the other hand. Recently diagram based techniques have been proposed to combine some of the advantage of deductive and algorithmic verification approaches. In this thesis, first hybrid and parameterized systems are introduced and then challenges for their verification are explained. Finally a diagram-based algorithm for verification of hybrid systems is proposed. The main idea behind the algorithm is to modeling hybrid systems with rectangular automata, and then using previous studdings for verification of rectangular automata. We also use linear temporal logic (LTL) to specify the properties we are interested in. Previous researches and studding are mostly restricted to linear systems and analyze the differential equations directly. While this thesis deals with modeling with rectangular automata and analyzing the automata. The most important advantage of proposed algorithm is that can be applied to both linear and nonlinear systems.
