-
شماره ركورد
9962
-
شماره راهنما(اين فيلد مربوط به كارشناس ميباشد لطفا آن را خالي بگذاريد)
9962
-
پديد آورنده
زينب حمزئي
-
عنوان
يك بررسي‌كننده مدل نمادين براي سيستم‌هاي زماني مبتني بر گراف كلاس حالت و منطق درخت محاسباتي
-
مقطع تحصيلي
كارشناسي ارشد
-
رشته تحصيلي
مهندسي كامپيوتر - گرايش نرم‌افزار
-
سال تحصيل
بهمن ماه 1390
-
تاريخ دفاع
بهمن ماه 1390
-
استاد راهنما
دكتر محمد عبدالهي ازگمي
-
چكيده
چكيده
سيستم‌هاي بي‌درنگ، سيستم‌هاي سخت‌افزاري يا نرم‌افزاري با محدوديت‌هاي زماني هستند و تاْمين نيازمندي‌هاي عملكردي و غيرعملكردي، درستي طراحي اين سيستم‌ها را تضمين مي‌كند. با توجه به عدم كفايت روش آزمون، درستي‌يابي صوري و به خصوص راه‌كار وارسي‌مدل خودكار، رهيافتي مطمئن براي اثبات درستي يا عدم درستي به شمار مي‌رود.
يك صورت‌بندي مناسب براي وارسي‌مدل سيستم‌هاي بي‌درنگ، مي‌تواند بسط‌هاي اتوماتاي زمانمند، شبكه‌هاي پتري زمانمند يا بر مبناي شيء باشد. بيشتر مسائل تحليل اتوماتاي زمانمند، تصميم‌پذير و برخي از تحليل‌هاي شبكه‌هاي پتري زمانمند، تصميم‌ناپذير است. البته شبكه‌هاي پتري زمانمند، به دليل توانايي بالا، براي توصيف همروندي در سيستم‌هاي پيچيده مناسب هستند.
در سيستم‌هاي هيبريد، مؤلفه‌ي گسسته و پيوسته همزمان وجود دارند و زمان نيز يكي از عوامل پيوسته است. بنابراين سيستم‌هاي بي‌درنگ، زيرمجموعهاي از سيستم‌هاي هيبريد هستند. اتوماتاي هيبريد، به عنوان صورت‌بندي رايج اين سيستم‌ها، مي‌تواند صورت‌بندي مياني، براي توصيف سيستم‌هاي بي‌درنگ نيز به شمار آيد. زيرا از يك سو، اتوماتاي زمانمند زيرمجموعهاي از آن بوده و از سوي ديگر روش‌هايي براي تبديل بسط‌هاي شبكه‌هاي پتري زمانمند به اتوماتاي هيبريد ارائه شده است.
به طور كلي، روش‌هاي شمارشي و توليد تمام فضاي حالت نامتناهي، براي سيستم‌هايي با مؤلفه پيوسته، ناكارآمد بوده و از وارسي‌مدل نمادين، استفاده مي‌شود. توليد گراف كلاس حالت، كه در آن حالات نامتناهي، در قالب تعدادي متناهي از كلاس‌هاي حالت، افراز مي‌شوند، راه‌حل مناسبي است كه كلاس‌هاي حالت در برخي از آنها درشت‌دانه و در برخي ريزدانه‌تر هستند و بررسي همه ويژگي‌هاي مورد نياز در آنها ممكن نيست.
در اين پايان‌نامه، ابزاري معرفي مي‌شود كه صورت‌بندي مدل‌هاي ورودي آن اتوماتاي هيبريد خطي است. بنابراين حوزه سيستم‌هاي مورد بررسي در اين ابزار، علاوه بر سيستم‌هاي بي‌درنگ، شامل سيستم‌هاي هيبريد خطي نيز مي‌شود. وارسي‌مدل براي نيازمندي‌هاي زماني انجام مي‌شود. كلاس حالت مورد استفاده در اين ابزار يك چندوجهي بوده و تمامي مراحل توليد گراف كلاس حالت بر اساس محاسبات چندوجهي است. در اين ابزار، بر خلاف برخي از ابزارهاي موجود، الگوريتم‌هاي تحليل، به مسائل دسترس‌پذيري محدود نمي‌شود و تحليل‌هاي زماني، بر روي مسيرهاي اجرا نيز ممكن است. هسته اصلي ابزار، پس از توليد فضاي حالت نمادين و افراز آن به زيرمجموعه‌هاي مناسب، وارسي‌مدل براي زيرمجموعهاي از منطق زماني TCTL مدل را وارسي مي‌كند.
واژه‌هاي كليدي: وارسي‌مدل نمادين، سيستم‌هاي هيبريد، منطق زماني، چندوجهي، گراف كلاس حالت.
-
لينک به اين مدرک :
