عنوان پایان‌نامه
وارسی سیستم های واکنشی بلادرنگ با استفاده از منطق زمانی مبتنی بر دیاگرام
- رشته تحصیلی
- مهندسی کامپیوتر- آلگوریتم ها و محاسبات
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه پردیس یک فنی شماره ثبت: 1.;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 38028
- تاریخ دفاع
- ۰۴ تیر ۱۳۸۷
- دانشجو
- محمد حاتمی رشیدی
- استاد راهنما
- علی معینی
- چکیده
- سیستم واکنشی ، سیستمی است که تعاملی پیوسته با محیط اطراف خود دارد. کارکرد درست سیستم های واکنشی به علت کاربرد آن در موارد خاص و حساس ضروری و اجتناب ناپذیر است. سیستم های کنترل ترافیک هوایی ، رآکتورهای اتمی آستانه تحمل خطا در طراحی و ساخت آن ها بسیار کم و در حد صفر است. بنابراین روشهای رسمی راستی آزمایی واکنشی ، اهمیت ویژه ای یافته است. از میان سیستم های واکنشی، اخیراً سیستم های بلادرنگ مورد توجه خاص قرار گرفته اند ، و روشهای متعددی برای راستی آزمایی (وارسی) آن ها پیشنهاد شده است. از آن جمله میتوان به روشهای مبتنی بردیاگرام اشاره کرد. روش های مبتنی بر دیاگرام ،خصوصیات روش های الگوریتمی و روشهای استقرایی را دربرمی گیرد . استفاده از دیاگرام ، قدرت توصیف و انعطاف پذیری روش-های استقرایی را با اتوماسیونی که از روشهای الگوریتمی به دست می آید، ترکیب میکند و حاصل کار قابل قبول تر می باشد. دیاگرام های مسنداتی نه تنها برای سیستمهای گسسته بلکه برای انواع سیستمهای واکنشی ، مثل سیستم های بلادرنگ پیوسته و سیستم های پارامتری به کار می روند. به نظر می رسد که دیاگرامهای مسنداتی برای راستی آزمایی سیستمهای واکنشی کامل باشند . ابزارهایی برای به دست آوردن دیاگرام ها ، به صورت تقریباً اتوماتیک به وجود آمده است. در این پایان نامه ، نمونه ای از سیستم های واکنشی را توصیف و راستی آزمایی شده است. این سیستم ، از چند پردازش که هر کدام دارای یک بخش بحرانی هستند، تشکیل شده است. تعداد پردازشهای فرض شده دلخواه است. سیستم فوق را می توان مشابه سیستم زیر دانست : سیستمی که شامل چند پردازش و یک منبع مشترک است و منبع در یک زمان ، فقط باید توسط یکی از پردازش ها در اختیار گرفته شود. برای رعایت انحصار متقابل در وارد شدن به مرحله بحرانی پردازش از پروتکل فیشراستفاده می شود. در ابتدا سیستم با استفاده از منطق زمانی توصیف می شود و سپس راستی آزمایی آن با استفاده از دیاگرامهای مسنداتی و دیاگرامهای مسنداتی زمانی انجام خواهد شد. کارهای قبلی مربوط به این موضوع ، به صورت محدود و با قیدهایی که در صورت مسئله اعمال شده بود، انجام گرفته است. سعی کردیم که قیدهای مسئله را کمتر کنیم و مسئله را در حالت کلی-تری حل کنیم. در کارهای قبل این کار برای سیستمی تنها با دو پردازش انجام شده است. در حالیکه اینجا ، توصیف و راستی آزمایی این سیستم با تعداد پردازشهای فرض شده انجام شده است.
- Abstract
- Reactive systems are those systems that have reaction with environment. Because of their application in special cases, function of these systems is important and unavoidable. Air traffic control systems and nuclear reactors are samples of reactive systems that have low fault tolerance in design and production, so reactive formal methods have important function in verification. Among reactive systems, real time systems are in attendance. A lot of methodologies and approaches were proposed for verification of these systems, For example diagram based approach proposed by Lamport and other researchers .Diagrams integrate deductive and algorithmic verification techniques for the verification of finite and infinite-state systems, thus combining the expressive power and flexibility of deduction with the automation provided by algorithmic methods. Predicate diagrams can be used to verify not only discrete systems, but also some more complex classes of reactive systems such as real-time systems and parameterized systems. It seems that time predicate diagrams and predicate diagrams are complete .Some tools can be used for supporting the generation of diagrams semi-automatically. In this dissertation, an example of reactive systems is specified and verified. This system included some processes with having each process has a critical section. Number of processes is arbitrary. It is similar to this system: A systems included some processes and a common resource. Common resource is occupied by only one process. For satisfaction of mutual exclusion in entrance to critical section, we use Fischer’s protocol. Initially, systems were specified by temporal logic, then verified by predicate diagrams and timed predicate diagrams. Previous researches in this field include some limitation, so generality of discussion was decreased. It is attempt to decrease the limitation and condition of problem and solve it in general case. Previous works solve this problem only with two processes, but it generalized number of processes in this dissertation.
