پایان نامه : درست یابی صوری سیستم های شیء بنیاد توسط جبر پردازه ای
مباحثی که در این پایان نامه مطرح شده عبارتند از:
چكيده :
الگوي مبتني بر شيء يکي از رايج ترين رويکردها به برنامه سازي و مدل سازي است. باوجود اينکه پيشرفت هاي بسياري در اين زمينه انجام شده است، اما به نظر مي رسد که هنوز اين الگو نظريات پخته و جاافتاده اي براي استدلال صوري نداشته باشد. در اين پايان نامه تلاش مي کنيم که پايه اي براي استدلال صوري در زمينه ي زبان هاي مبتني بر شيء بنا کنيم. براي تحليل صوري، از شيوه ي تحليل جبرپردازه اي استفاده مي کنيم، که رويکردي قدرتمند براي مدل سازي سيستم هاي همروند است. با فراهم کردن نگاشتي از زبان هاي مبتني بر شيء به جبرپردازه اي، مي توانيم از توانمندي هاي جبرپردازه اي در کاربردهاي صنعتي نيز استفاده کنيم. در نگاشت ارائه شده به طور خاص بر جبرپردازه اي mCRL2 تمرکز مي کنيم، که يک شکل از جبرهاي پردازه اي است که از انواع داده اي به خوبي پشتيباني مي کند. توانايي هاي mCRL2 در کارهاي بسياري پيش از اين به اثبات رسيده بودند، و علاوه براين مجموعه ابزارهاي نيرومندي براي تحليل و درستي يابي مدل هاي mCRL2 وجود دارند. براي عملي کردن ايده هاي خود از دو زبان مبتني بر شيء استفاده مي کنيم. اولي زبان ربکاست، که زباني مبتني بر مدل بازيگر است که براي مدل سازي سيستم هاي همروند و توزيع شده به کار مي رود. زبان دوم زبان SystemC است که در صنعت کاربرد بسيار دارد. اين زبان در طراحي هاي در سطح سيستم کاربرد دارد. برتري هاي رويکرد ما در مقايسه با نگاشت هاي انجام شده ي پيشين در زمينه ي تبديل زبان هاي مبتني بر شيء به جبرپردازه اي، استفاده ي بسيار از انواع داده اي موجود در mCRL2 است. توانايي انواع داده اي موجود در mCRL2 تاحدي بود که عمومًا نيازي به تعريف مجدد انواع داد هاي احساس نشد. هر دو نگاشت در قالب يک ابزار کامپايلر پياده سازي شده و تعدادي مطالعه ي موردي در هر دو مورد انجام شده اند. نتايج نگاشت ربکا نشان مي دهد که کاهش ترتيب جزئي پويا اندازه ي فضاي حالت را نسبت به روش هاي پيشين (که ايستا بودند) بيشتر کاهش مي دهد، حال آنکه از لحاظ زماني ُکندتر است. همچنين توانستيم که يک اشکال در پياده سازي انجام شده ي قبلي براي روش هاي ايستاي کاهش ترتيب جزئي بيابيم، که توسط خوشه سازي قابل حل شدن است. در نگاشت SystemC نيز يک اشکال مخفي در پياده سازي ريزپردازنده ي mini MIPS پيدا شد، که تا قبل از آن يافته نشده بود.
فهرست
مقدمه:
۱ دست آوردهاي پايان نامه
۲ زبان مبتني بر شيء
۳ ساختار پايان نامه
٢ کارهاي مشابه:
۱ زبان هاي تبديل شده به mCRL
٣ پيش زمينه ها:
۱ سيستم هاي گذار: مبتني بر حالت و مبتني بر کنش
۱ کنش هاي پنهان راکد
۲ منطق هاي زماني
۳ ه مارزي رفتارها
۱ دوشبيه سازي
۱ دوشبيه سازي قوي .
۲ دوشبيه سازي ضعيف .
۳ دوشبيه سازي انشعابي .
۲ ه مارزي ُلکَنتي .
۳ جم عبندي
۴ جبرپردازه اي 2 mCRL
۱ مقدمه اي بر جبرپردازه اي
ُ خرد زبان نمايش مشترک
فلسفه ي ايجاد .
۲ انواع داده اي مجرد
۳ مقدمه اي بر
۱ ترکيب گزينشي و متوالي
۲ پردازه هاي موازي
۳ ب نبست و بسته بندي
۴ اعلان پردازه ها .
۵ عبارات شرطي
۶ جم عزني بر روي يک نوع داده اي .
۷ تغيير نام
۸ پنهان سازي کنش ها
. نسبت به mCRL ۳ توسعه هاي CRL
۱ انواع داده اي جديد در mCRL
۲ چندکنش ها .
۵ نگاشت ربکا (سرير):
۱ زبان ربکا -۵
۲ طرح نگاشت
۳ پياده سازي و مطالعات موردي
۴ بررسي کاهش فضاي حالت
۵ خلاصه ي فصل .
۶ نگاشت SystemC
۱ مقدمه .
۲ زبان SystemC
۳ انواع داده اي هسته
پردازه هاي هسته
۵ از پردازه هاي SystemC به پردازه هاي2 mCRL
۶ وراسي کد
۷ مطالعه ي کاربردي
۸ خلاصه فصل
۷ الگوريتم هاي کاهش:
۱ سرآغازي بر روش هاي کاهش فضاي حالت .
۲ خطي سازي
۳ کاهش ترتيب جزئي
-اولويت دهي
۲ کاهش ترتيب جزئي در ساختارهاي کريپکه
۱ روش پياده سازي
۳ کافي بودن کاهش ترتيب جزئي
۴ مخروط ها و کانون ها
۸ نتيجه گيري و کارهاي آينده:
۹ ضميمه:
فهرست منابع
فرهنگ واژگان (انگليسي به فارسي)
فرهنگ واژگان (فارسي به انگليسي)
***************************************************************************************
در صورت تمایل
به دریافت فایل فوق در مدت 10 دقیقه ، لطفاً اینجا کلیک
کنید
***************************************************************************************
مشاوره ؛نگارش پایان نامه ؛ مقاله + شبیه سازی
در تمام مقاطع دانشگاهی پذیرفته می شود
در صورت
تمایل می توانید عنوان و جزئیات پروژه خود را در قسمت نظرات این پست
اعلام فرمایید. ضمنا می توانید اطلاعات درخواستی خود را به ایمیل یا تلگرام
نمایید
ایمیل :
com.dr@yahoo.com
درباره :
درست یابی صوری ,
|