عنوان پایان‌نامه
استفاده از روشهای هوشمند برای بهینه سازی درستی یابی صوری
- رشته تحصیلی
- مهندسی کامپیوتر- هوش مصنوعی - رباتیک
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 39915;کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 1455
- تاریخ دفاع
- ۱۰ دی ۱۳۸۷
- دانشجو
- راضیه بهجتی اردکانی
- چکیده
- پیچیدگی روز افزون سیستم¬های سخت¬افزاری و نرم¬افزاری امکان طراحی سیستم¬های درست با استفاده از تکنیک¬های غیرصوری را مشکل کرده است. روش¬های صوری روش¬هایی هستند که با تکیه بر مدل¬های ریاضی به تحلیل و بررسی طراحی سیستم¬ها می¬پردازند. وارسی مدل، یکی از روش¬های مطرح در درستی¬یابی است که درستی¬یابی را به صورت کاملاً خودکار انجام می¬دهد. این روش با وجود دقت بالایی که دارد با مشکل انفجار فضای حالت (افزایش نمایی فضای حالت با افزایش ابعاد مسئله) روبه¬رو است. برای غلبه بر این مشکل روش¬های مختلفی ارائه شده است که هر یک به نحوی به افزایش کارایی این روش¬ کمک می¬کند. ایده¬ی اصلی در این پژوهش، استفاده از روش¬های هوش مصنوعی برای بهینه¬سازی و نیز مدیریت مشکلات موجود در وارسی مدل است. برای این منظور به دنبال ارائه¬ی روشی هوشمند برای گسترش محدوده¬ی وارسی مدل به درستی¬یابی مدل¬های بزرگتر و پیچیده¬تر هستیم. طی سال-های اخیر روش¬های مختلفی مبتنی بر یادگیری ماشین برای بهینه¬سازی وارسی مدل و یا گسترش آن به مدل¬های بزرگتر و حتی نامتناهی ارائه شده است. در این پایان نامه چارچوبی مبتنی بر یادگیری تقویتی برای وارسی ویژگی¬های منطق زمانی خطی ارائه می¬دهیم. در چارچوب پیشنهادی، هدف بهینه¬سازی مصرف حافظه از طریق افزایش احتمال وقوع مسیرهای منجر به نقض ویژگی¬ها است. برای این منظور از یک عامل با قابلیت یادگیری تقویتی برای افزایش احتمال کشف اینگونه مسیرها در اجراهای اولیه استفاده شده است. در یادگیری تقویتی عامل از طریق تعامل با محیط و دریافت پاداش و جزا به یادگیری مفاهیم می¬پردازد. در چارچوب پیشنهادی با تکیه بر شرط انصاف تابع پاداشی ارائه شده است که به درستی عامل را به سمت یافتن مثال¬های نقض هدایت می¬کند. همچنین از آنجا که جستجوی عامل فضای حالت مدل را به طور کامل پوشش نمی¬دهد از روش¬های احتمالی در وارسی مدل به منظور ارائه¬ی تقریبی از میزان تطابق مدل با ویژگی منطق زمانی خطی داده شده بهره گرفته¬ایم. این تقریب در مواردی ارائه می¬شود که پس از تولید تعداد مشخصی مسیر اجرا از مدل هیچ مثال نقضی یافت نشود. در نهایت برای نمایش کارایی چارچوب پیشنهادی، نتایج حاصل از آن برای وارسی مدل تعدادی مثال نمونه ارائه و با نتایج حاصل از روش معمول وارسی مدل و نیز وارسی مدل تصادفی مقایسه شده است. کلمات کلیدی: درستی¬یابی صوری، وارسی مدل سیستم¬های نامتناهی، یادگیری ماشین، یادگیری تقویتی، وارسی مدل احتمالی
- Abstract
- Today’s increasing complexity of hardware and software designs has made it impossible to provide bug free systems. Formal methods are analytical means which use mathematical models of systems in order to discover bugs and invalid runs of systems. Model checking is a promising approach which is mainly used for the verification of concurrent and reactive systems. The main obstacle in model checking is state explosion, which is the problem of exponential growth of the size of the state space in the size of the model. Over the past two decades, researchers have developed a large number of techniques to overcome state explosion, including: partial-order reduction methods, symmetry reduction, and compositional verification. The main idea in this research is to use machine learning methods for the purpose of handling the problems in model checking. For this purpose we have proposed a learning-based method in order to expand the applicability of model checking to larger and more complicated models. We propose a bounded rational verification approach for on-the-fly model checking of LTL properties. We optimize memory usage by increasing the probability of finding faulty runs. Since in on-the-fly model checking we do not have complete knowledge about the model, we use a machine learning method based on interaction and reward receiving. Based on the concept of fairness we propose a heuristic for defining rewards. We also exploit the ideas of probabilistic model checking in order to find a measure of correctness of the system in the case where no violations are found after generating a certain number of runs of the system. The experimental results show that this approach easily outperforms classical model checking approaches. Key Words: Formal Verification, Model Checking Infinite Systems, Machine Learning, Reinforcement Learning, Probabilistic Model Checking
