10037

10037

طراحي يك مولد فضاي حالت نمادين براي توصيف‌هاي سيستم‌هاي تصادفي گسسته-رخداد و پياده‌سازي آن در چارچوب PDETool

كارشناسي ارشد

مهندسي كامپيوتر– گرايش نرم¬افزار

خردادماه 1390

خردادماه 1390

دكتر محمد عبدالهي ازگمي

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