آقای حسن مطلبی پاقلعه دانشجوی دکترای جناب آقای دکتر محمد عبدالهی ازگمی روز یکشنبه مورخ 21/07/92 ساعت 16:30 در اتاق دفاعیه واقع در طبقه دوم دانشکده مهندسی کامپیوتر از رساله دکترای خود تحت عنوان ارائه و تحلیل زمانی یک صورت بندی برای مدل سازی سیستم های هیبرید دفاع خواهند نمود .

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

  در سال‌های اخیر مدل‌سازی ودرستی‌یابی سیستم‌های هیبرید موضوع پژوهش‌هایمتعددی بوده است. معمولاً در این زمینه از مدل‌های هیبرید مبتنی بر اتوماتا استفاده می‌شود. دلیل این امر، قدرت توصیف نظری و تحلیل‌پذیریبالای این صورت‌بندی‌ها در مقایسه با بسط‌هایهیبرید شبکه‌های پتری است. اما، به دلیل سطح پایین بودن و محدودیت‌های تعامل مدل‌های مبتنی بر اتوماتا، این صورت‌بندی‌ها برایتوصیف سیستم‌هایهیبرید پیچیده مناسب نیستند.

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

  در این رساله دو دسته صورت ‌بندی برای مدل‌سازی و درستی‌یابی سیستم‌های هیبرید پیشنهاد شده است: صورت‌بندی‌های مبتنی بر شبکه‌های پتری و صورت‌بندی‌های مبتنی بر شبکه‌های فعالیت. بسط‌های پیشنهادیبه منظور پر کردن فاصله بین اتوماتای هیبرید و شبکه‌های پتری هیبرید و نیز شبکه‌های فعالیت پیشنهاد شده‌اند. صورت‌بندی‌های هیبرید حاصله دارای قدرت توصیف و تحلیل‌پذیری معادل با اتوماتای هیبرید هستند.

  برای مدل‌سازی و تحلیل سیستم‌های هیبرید چندنرخی، شبکه‌های پتری هیبرید چندتکین (MSHPN) پیشنهاد شده‌ است. به منظور فراهم کردن امکان مدل‌سازی پارامتری سیستم‌هایهیبرید و تحلیل مستقیم مدل‌های پارامتری بدون نیاز به مقداردهی پارامترها، شبکه‌های پتری هیبرید چندتکین پارامتری
(P-MSHPN) پیشنهاد شده است. همچنین برای تحلیل محافظه‌کارانه و به‌دست آوردن نتایج قابل اتکا در حضور خطاهای اندازه‌گیری، محاسبات غیردقیق ونوسان زمان‌سنج‌ها، شبکه‌های پتری هیبرید بازه‌ای (IHPN) پیشنهاد شده است. نهایتاً، برای توصیف و تحلیل سیستم‌هایزمانی و هیبریدی که توصیف آنها با استفاده از شبکه‌های پتری زمانی و هیبرید، دشوار یا ناممکن است (به دلیل پیچیده بودن قواعد فعال‌سازی گذرها و اثر شلیک آنها)، شبکه‌های فعالیت زمانی (TAN) و شبکه‌های فعالیت هیبرید (HAN) پیشنهاد شده‌اند.برایحل مسأله چالش‌بر‌انگیز رفع برخورد بین گذرهای زمانی و محاسبه سرعت اجرای گذرهای زمانی در حضور برخوردها، گزاره‌های منتسب به گذرها و سطوح مختلف اولویت،هم در MSHPN ‌ و هم HAN ، از محاسبات چندوجهی و تکنیک‌های برنامه‌ریزی خطیبه‌کار گرفتهشده‌اند.

  برای محاسبه فضای حالت نمادین MSHPN ، روش افراز مبتنی بر سرعت معرفی شده است که در آن فضای متغیرهای پیوسته سیستم به یک مجموعه متناهی از چندوجهی‌های نه لزوماً بسته افراز می‌شود، طوری که بردار سرعت در هر چندوجهییک مقدار ثابت مشخص داشته باشد. الگوریتم‌ محاسبه فضای حالت نمادین، رفتار سیستم را در قالب یک گراف کلاس حالت به‌دست می‌آورد. برای تحلیل مدل پارامتری
P-MSHPN ، بسط پارامتری الگوریتم‌ها و ساختمان داده‌های مربوط به مدل غیرپارامتری ارائه شده است. در این روش لازم است صرفاً یکبار فضای حالت پارامتری مدل در قالب یک گراف کلاس حالت پارامتری محاسبه شود. وقتی این گراف کلاس حالت پارامتری به‌دست آمد،یا می‌توان از آن برای وارسی مدل پارامتری استفاده کرد یاآن‌که با مقداردهی پارامترها ی آن،یک گراف کلاس حالت غیرپارامتری به‌دست آورد. به علاوه، برای رفع برخورد و محاسبه سرعت و فضای حالت مدل‌های IHPN ، برنامه‌ریزی خطی بازه‌ای و ریاضیات بازه‌ای به‌کار گرفته شده‌اند.

  با ارائه مثال‌های تشریحی در کاربردهای مختلف نشان داده شده که صورت‌بندی‌های پیشنهادی قابلیت توصیف سیستم‌هایی را دارند که توصیف آنها با صورت‌بندی‌های پیشین عملی نیست.

  واژه‌های کلیدی: سیستم‌های هیبرید، شبکه پتری هیبرید، اتوماتای هیبرید، شبکه‌های پتری هیبرید چندتکین، شبکه‌های پتری هیبرید بازه‌ای، شبکه‌های پتری هیبرید چندتکین پارامتری، شبکه‌های فعالیت زمانی، شبکه‌های فعالیت هیبرید، افراز مبتنی بر سرعت.

 : Abstract

  In recent years, modeling and verification of hybrid systems has been the topic of several researches. Generally, automaton-based hybrid formalisms are used in this area. The reason is high expressive power and analyzability of these formalisms comparing to the hybrid extensions of Petri nets. However, due to low-level of description and the limitations in interactions of automaton-based models, these formalisms are not well-suited for describing complicated hybrid systems.

  There is also a body of work on proposing high-level modeling formalisms, which are suitable for complicated hybrid systems. Different timed and hybrid extensions of Petri nets are examples of these models. However, since some modeling capabilities of the automaton-based models do not exists in these formalisms, the Petri net-based models does not have enough expressive power. That is, there are systems that describing them using the automaton-based models is possible, but using Petri net-based models is difficult or even impossible .

  In this dissertation, two categories of models are proposed for modeling and analysis of hybrid systems: Petri net-based models and activity network -based models. The proposed extensions are aimed to bridge the gap between hybrid automata (HA) and hybrid Petri nets (HPNs) and also activity networks. The resulting hybrid formalisms have the same expressive power and analyzability as the hybrid automata. Multisingular hybrid Petri nets (MSHPNs) are proposed for modeling and analysis of multi-rate hybrid systems. In order to perform parametric analysis on hybrid systems parametric multisingular hybrid Petri nets (P-MSHPNs) is proposed, which allow direct analysis of parametric models without the need for instantiating them to obtain non-parametric models. In order for conservative analysis of hybrid systems in presence of inexact data and drifting clocks, interval hybrid Petri nets (IHPNs) are proposed . Finally, for modeling and analysis of timed and hybrid systems with complicated behaviors, where the usage of timed and hybrid Petri nets is difficult or impossible (due to the complexity of describing enabling and firing rules of transitions), two activity network-based models, i.e., timed activity networks (TANs) and hybrid activity networks (HANs), are also proposed.

  In order to address the challenging issue of conflict resolution between timed transitions and speed computation in presence of conflicts and execution predicates of transitions and different priority levels for MSHPNs and HANs, the polyhedral computations and linear programming techniques are employed.

  For symbolic state space computation of MSHPNS, the speed-based partitioning technique is introduced, which partitions the space of all valuation for real variables into a finite set of not necessarily closed convex polyhedra, such that the speed vector in each polyhedron is a specified constant vector. The speed-based partitioning technique, obtains the symbolic state space as a state class graph.

  Some illustrative examples of the proposed formalisms are used to demonstrate the expressive power of these models.

  Keywords: Hybrid systems, multisingular hybrid Petri nets (MSHPNs), parametric multisingular hybrid Petri nets (P-MSHPNs), interval hybrid Petri nets (IHPNs), timed activity networks (TANs), hybrid activity networks (HANs), speed-based partitioning.

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

  حسن مطلبی پاقلعه

  hmotallebi@iust.ac.ir

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

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

  هیات داوران:

  دکتر سعید پارسا-دکتر محمدرضا جاهد مطلق - دکتر محسن شریفی

  دکتر فاطمه قاسمی اصفهانی - دکتر مهران سلیمان فلاح

  زمان : یکشنبه 21 مهرماه 1392

  ساعت 16:30

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

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

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