آقای بهرنگ مهرپرور دانشجوی کارشناسی ارشد جناب آقای دکتر محمد عبدالهی ازگمی روز سه شنبه31/3/90 ساعت 11 صبح در اتاق 304 واقع در طبقه سوم دانشکده کامپیوتر ازپروژه کارشناسی ارشد خود تحت عنوان ارائه فنونی برای بررسی مدل توصیف های سیستم های تصادفی گسسته - رخدادد و پیاده سازی آنها دفاع خواهد نمود.

  چکیده پایان نامه:

  توصیف SDES یک روش یکپارچه و انتزاعی برای توصیف سیستم ­ های تصادفی گسسته رخداد است. کلاس ‌ هایروشهای صوری گوناگونهمچون شبکه ­ های پتری و اتوماتاهای زمانی تصادفی،که برای مدل­سازی این گونه سیستم­ها بکار می­روند را می­توان به توصیف SDES تبدیل نمود.همچنین ابزار PDETool به عنوان یک چارچوب یکپارچه برای ارزیابی، شبیه­سازی و تحلیل مدل­های سطح بالا بر پایه توصیف SDES طراحی شده است.

  هدف از این پژوهش، افزودن فنون بررسی مدل به ابزار PDETool بوده است. برای این منظور، یک موتور بررسی کننده مدل به نام McGine ساخته و در چارچوب PDETool مجتمع شده است. چارچوب یکپارچه حاصل، یک محیط جامع برای مدل‌سازی، ارزیابی و درستی‌یابی سیستم‌های گسسته-رخداد فراهم آورده است. از سوی دیگر مفهوم نظری و روش بررسی مدل صورت‌بندی چند­گانه معرفی و در McGine پیاده‌سازی شده است. برای این منظور، روشی برای استخراج فرمول ­ های منطق درخت محاسباتیازمتغیر ‌ های SDES ارائه شده است. علاوه بر این فضای حالت عمومی و الگوریتم تولید آن و همچنین سازوکار کدبندی حالت­های SDES معرفی شده است. با بکار بردن روش ارائه شده برای کدبندی، امکان بررسی مدل نمادین مبتنی بر نمودار تصمیم دودویی فراهم آمده است. در پایان معماری بررسی کننده McGine به گونه­ای طراحی شده که می­تواند در چارجوب PDETool و یا به عنوان یک ابزار جداگانه مورد استفاده قرار گیرد. پس از آن روش ارائه شده و موتور تولید شده مورد ارزیابی قرار گرفته و نتایج در این پایان­نامه ارائه شده­اند.

  واژه‌های کلیدی: بررسی مدل، توصیف سیستم­های گسسته-رخداد( SDES ) ، منطق درخت محاسباتی ( CTL ) ، صورت‌بندی چند­گانه ، کدبندی حالت­ها.

  Abstract

 SDES description is a unified abstract formalism for modeling stochastic discrete-event systems. Various classes of formalisms such as stochastic Petri nets or stochastic timed automata, which are used for modeling these systems, can be translated into SDES descriptions. Moreover, PDETool, which is an integrated framework for model construction, evaluation and simulation of high-level models based on SDES description, has already been developed .

  The aim of this thesis has been to extend PDETool with model checking techniques. For this purpose, a model checking engine, called McGine, has been developed and integrated into PDETool framework. The resulting unified framework is an integrated environment for modeling, evaluation and verification of discrete-event systems. Furthermore, the theoretical concepts and methods of multi-formalism model checking is introduced and partially implemented in McGine. For this purpose, a new method for extracting computational tree logic (CTL) formulas from SDES variables is proposed. Moreover, the general state space and the corresponding state space generation algorithm are introduced. Also, an encoding mechanism for SDES states is proposed. By applying the proposed encoding method, binary decision diagram (BDD) based symbolic CTL model checking is achieved. Finally, the architecture of McGine is designed and implemented, which can be used through PDETool framework or as a stand-alone tool. The proposed methods and the developed engine are evaluated and the results are presented in this thesis.

  Keywords: Model checking, Stochastic Discrete-Event Systems (SDES), Computational tree logic (CTL), Multi-formalism, State encoding

ارائه­دهنده:

بهرنگ مهرپرور

  اساتید راهنما:

محمد عبدالهی ازگمی

  استاد ممتحن خارجی : دکتر رامتین خسروی

  استاد ممتحن داخلی :دکترمحمدرضا کنگاوری

زمان : سه شنبه31خرداد ماه 1390

  ساعت11 صبح

  مکان: دانشکده مهندسی کامپیوتر- طبقه سوم- اتاق 304

  از اساتید بزرگوار، دانشجویان گرامی و دیگر متخصصان و علاقه مندان به موضوع دفاعیه دعوت
می شود با حضور خود موجبات غنای علمی و ارتقای کیفی را فراهم سازند.

  دانشکده مهندسی کامپیوتر مدیریت تحصیلات تکمیلی