شماره ركورد
10037
شماره راهنما(اين فيلد مربوط به كارشناس ميباشد لطفا آن را خالي بگذاريد)
10037
پديد آورنده
رضا فتحي
عنوان
طراحي يك مولد فضاي حالت نمادين براي توصيفهاي سيستمهاي تصادفي گسسته-رخداد و پيادهسازي آن در چارچوب PDETool
مقطع تحصيلي
كارشناسي ارشد
رشته تحصيلي
مهندسي كامپيوتر– گرايش نرم¬افزار
سال تحصيل
خردادماه 1390
تاريخ دفاع
خردادماه 1390
استاد راهنما
دكتر محمد عبدالهي ازگمي
چكيده
چكيده
بررسي مدل يكي از مهمترين روشهاي درستييابي سيستمهاست. يكي از مشكلات بررسي مدل¬، توليد فضاي حالت است. معمولاً به دليل بزرگ بودن فضاي حالت، مشكل انفجار حالت پيش ميآيد.اين مشكل به اين دليل بوجود ميآيد كه اندازه فضاي حالت با تعداد متغيرهاي مدل رشد نمايي دارد. از راهكارهاي غلبه بر اين مشكل، نگهداري فضاي حالت به صورت ضمني به جاي نگهداري صريح آنهاست. در اين روش به جاي نگهداري صريحِ فضاي حالتِ مدل، فضاي حالت به صورت نمادين، مثلاً به كمك نمودارهاي تصميم نگهداري ميشود. نگهداري فضاي حالت به صورت نمادين، هزينه ذخيره و پردازش فضاي حالت را به مرتبه ذخيرهسازي و پردازش گراف¬ها كاهش ميدهد و نسبت به روشهاي سنتي ذخيره فضاي حالت مثل روشهاي ليستي، آرايهاي، جدول درهمسازي، بردار بيتي و غيره، توانايي ذخيره، مديريت و پردازشِ فضاي حالتِ به مراتب بزرگتري را دارد.
ابزارهاي متعددي براي بررسي مدل وجود دارد كه با مدلهاي صوري متفاوتي كار نموده و فنون مديريت فضاي حالت و بررسي مدل مختلفي را فراهم ميكنند. ابزار مدلسازي PDETool با هدف فراهم سازي يك چارچوب يكپارچه براي مدلسازي و تحليل سيستمها طراحي شده است. در اين ابزار از توصيف سيستمهاي تصادفي گسسته رخداد (SDES) به عنوان صورتبندي رابط استفاده مي¬گردد، كه انواع مدلهاي صوري به آن تبديل ميشوند. اين ابزار فنون مختلف شبيهسازي، حل مدل و بررسي مدل را در قالب يك چارچوب واحد فراهم مي¬سازد. ورودي اين فنون، مدلهاي مياني SDES است. در روشهاي حل مدل تحليلي و نيز در بررسي مدل، انتخاب مناسب مولد فضاي حالت بسيار كليدي خواهد بود.
در اين پايان¬نامهفني براي توليد فضاي حالت نمادين از توصيف SDES ارائه شده است. در اين روش، با استفاده از توليد فضاي حالتنمادين به كمك گراف تصميم¬گيري دودويي مرتب كاهش¬يافته (ROBDD)، فضاي حالت بسيار بزرگتري را مي¬توان توليد و مديريت كرد.در نتيجه با استفاده از اين روش، ميتوان تحملپذيري بالاتري را در مقابل مشكل انفجار حالت ايجاد كرد. جزئيات فن پيشنهادي، طراحي و نتايج پيادهسازي آن در PDETool و نيز نتايج ارزيابي اين فن در اين پاياننامه ارائه شده است.
واژههاي كليدي:توليد فضاي حالت نمادين، گراف تصميم دودويي مرتب كاهشيافته(ROBDD)، انفجار فضاي حالت، توصيف SDES، سيستمهاي تصادفي گسسته رخداد