خانم زینب حمزئی دانشجوی کارشناسی ارشد جناب آقای دکتر محمد عبداله ازگمی روز یکشنبه30/11/90 ساعت 16:15 در اتاق دفاعیه واقع در طبقه سوم دانشکده کامپیوتر از پروژه کارشناسی ارشد خود تحت عنوان یک بررسی کننده مدل نمادین سیستم های بی درنگ مبتنی برکلاس حالت و منطق درخت محاسباتی دفاع خواهند نمود.

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

  سیستم‌های بی‌درنگ، سیستم‌های سخت‌افزاری یا نرم‌افزاری با محدودیت‌های زمانی هستند و تاْمین نیازمندی‌های کارکردی و غیرکارکردی، درستی طراحی این سیستم‌ها را تضمین می‌کند. با توجه به عدم کفایت روش آزمون، درستی‌یابی صوری و به خصوص راه‌کار وارسی‌مدل خودکار، رهیافتی مطمئن برای اثبات درستی یا عدم درستی به شمار می‌رود.

  یک صورت‌بندی مناسب برای وارسی‌مدل سیستم‌های بی‌درنگ، می‌تواند بسط‌های اتوماتای زمانمند، شبکه‌های پتری زمانمند و یا بر مبنای شیء باشد. بیشتر مسائل تحلیل اتوماتای زمانمند، تصمیم‌پذیر و برخی از تحلیل‌های شبکه‌های پتری زمانمند، تصمیم‌ناپذیر است. البته شبکه‌های پتری زمانمند، به دلیل توانایی بالا، برای توصیف همروندی در سیستم‌های پیچیده مناسب هستند. به بیان دیگر، نسبت اتوماتا به شبکه‌های پتری، مانند زبان اسمبلی به زبان‌های سطح بالای برنامه‌نویسی است.

  در سیستم‌های هیبرید، دو مؤلفه گسسته و پیوسته همزمان وجود دارند و زمان نیز یکی از عوامل پیوسته است. بنابراین سیستم‌های بی‌درنگ، زیر مجموعه‌ای از سیستم‌های هیبرید هستند. اتوماتای هیبرید، صورت‌بندی رایج این رده از سیستم‌ها است. می‌توان اتوماتای هیبرید را به عنوان صورت‌بندی میانی، برای توصیف سیستم‌های بی‌درنگ نیز به شمار آورد. زیرا از یک سو، اتوماتای زمانمند زیر مجموعه‌ا‌ی از آن بوده و از سوی دیگر روش‌هایی برای تبدیل بسط‌های شبکه‌های پتری زمانمند به اتوماتای هیبرید ارائه شده است.

  به طور کلی، روش‌های شمارشی و تولید تمام فضای حالت نامتناهی، برای سیستم‌هایی با مؤلفه پیوسته، ناکارآمد بوده و از وارسی‌مدل نمادین، استفاده می‌شوند. تولید گراف کلاس حالت، که در آن حالات نامتناهی، در قالب تعدادی متناهی از کلاس‌های حالت، افراز می‌شوند، راه‌حل مناسبی است که کلاس‌های حالت در برخی از آنها درشت‌دانه و در برخی ریزدانه‌تر هستند و بررسی همه ویژگی‌های مورد نیاز در آنها ممکن نیست.

  در این پایان‌نامه، ابزاری معرفی می‌شود که صورت‌بندی مدل‌های ورودی آن اتوماتای هیبرید خطی است. وارسی‌مدل برای نیازمندی‌های زمانی انجام می‌شود. کلاس حالت مورد استفاده در این ابزار یک چندوجهی بوده و تمامی مراحل تولید گراف کلاس حالت بر اساس محاسبات چندوجهی است. در این ابزار، بر خلاف برخی از ابزارهای موجود، الگوریتم‌های تحلیل، به مسائل دسترس‌پذیری محدود نمی‌شود و تحلیل‌های زمانی، بر روی مسیرهای اجرا نیز ممکن است. هسته‌ اصلی ابزار، پس از تولید فضای حالت نمادین و افراز آن به زیر مجموعه‌های مناسب، وارسی‌مدل برای زیر مجموعه‌ای از منطق زمانی TCTL مدل را وارسی‌ می‌کند.

  واژه‌های کلیدی: وارسی‌مدل نمادین، سیستم‌های هیبرید، منطق زمانی ، چندوجهی، گراف کلاس حالت، منطق درخت محاسباتی زمانمند( TCTL ).

Abstract:

In recent years, the problem of modeling and verification of real-time systems has become very important. Obviously, correctness is of vital importance in safety-critical real-time systems, which needs software and mathematical tools that support the design and development of these systems. Using formal methods for modeling and analysis of systems, by well-known formalisms like automata, Petri nets and so on is imperative.

  A hybrid system is a wide class of systems, where discrete and continuous phenomena can be encountered. It requires a mathematical formalism that supports both discrete and continuous aspects of such systems. Real-time systems are special case of hybrid systems. The only one continuous variable is clock whose rate of change with time is always one.

  Hybrid automata are generalized finite state machine for modeling hybrid systems. These automata model the continuous activities of analogue variables, as well as discrete events.

  In this thesis, a symbolic model checking tool is provided for linear hybrid automata. The proposed tool is based on the symbolic model checker HyTech. HyTech already supports model checking of all kinds of temporal properties that can be expressed as a reachability problem.

  The main algorithm consists of three parts (1) getting XML input language of modeled linear hybrid automata, (2) the TCTL temporal logic that models timed requirements, and (3) generating state space of input hybrid automata and model checking against temporal requirements that is more than reachability analysis. State space computation algorithm is based on polyhedral computation, which is an important approach toward abstraction and static analysis of dynamic behavior of sophisticated and parallel systems.

  Keywords: Real-time systems, model checking, state class graph, polyhedron, timed computational tree logic (TCTL).

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

 زینب حمزئی

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

  دکتر محمد عبدالهی ازگمی

  استاد ممتحن داخلی : دکتر سعید پارسا

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

  زمان : یکشنبه 29 بهمن ماه

  ساعت 16:15

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

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

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