پاورپوینت درس درستي يابي سيستم هاي واكنشي (pptx) 46 اسلاید

دسته بندی : پاورپوینت

نوع فایل : PowerPoint (.pptx) ( قابل ویرایش و آماده پرینت )

تعداد اسلاید: 46 اسلاید

قسمتی از متن PowerPoint (.pptx) :

به نام خداارائه درس درستي يابي سيستم هاي واكنشيموضوع : Rebeca (Reactive Object Language)  مقدمه real applications Rebeca formal verification يكي از ملزومات درستي يابي رسمي براي اطمينان از درستي سيستم ها داشتن يك روش كارآمد و مناسب براي مدل سازي سيستم هاي همروند و توزيع شده است.Rebeca يك زبان actor-base براي مدلسازي اين سيستم ها است. در واقع Rebeca تلاش ميكند همانند پلي ارتباطي ميان درستي يابي رسمي و application هاي واقعي عمل نمايد. as a reference model Concurrent Cmputation Rebeca platform for developing object-based concurrent systems Rebeca مي تواند بر پايه يك مفسر قابل استفاده براي مدل actor به عنوان مدل مرجع براي محاسبات هم روند، استفاده شود، همچنين Rebeca مي تواند عملا پايگاهي براي توسعه سيستم هاي هم روند شي گرا باشد. Rebeca مشابه مدل actor مي باشد كه درآن: active object ها مستقل. message passing ها غير هم زمان بافر ها نا محدود. تغيير topology و توليد active object ها به صورت dynamic است تعريف class به syntax اضافه شده و class ها عملا شبيه الگوهايي براي states، behaviorو active object interfase هستند. component ها به عنوان active object هايي كه به صورت غير هم زمان اجرا مي شوند تصور شده اند. در rebeca نقش active object هاي داخلي و خارجي متفاوت با مدل actor واقعي است. Objectها واكنشي و self-contaend هستند كه به آنها rebec اتلاق مي شود. Rebeca و يا (Reactive Object Language) حاصل تحقيقات و پايان نامه خانم دكتر مرجان سيرجاني از اساتيد فعلي دانشكده فني و مهندسي دانشگاه تهران و دانشجوي آقاي دكتر موقر در دانشگاه صنعتي شريف مي باشد. همچنين تحقيقات صورت گرفته براي تكامل Rebeca حاصل تلاش گروهي از دانشجويان دانشگاه صنعتي شريف و دانشگاه تهران مي باشد.Rebeca يك مدل نسبتا جديد و در حال تكامل است اين مدل براي اولين بار در سال 2002 با ارائه مقاله اي تحت عنوانSimulation in Rebeca در كنفرانس بين الملليParallel and Distributed Processing Techniques and Applications(PDPTA’02) مطرح شد و در اوريل همان سال در سمينار Automated Verification of Critical Systems (AVoCS'02) در دانشگاهBirmingham ارائه شد. مقالات Rebeca در كنفرانسها و سمينارهاي بين المللي ارائه شده و تعدادي از آنها منتشر شده است . 2003 M. Sirjani, A. Movaghar, H. Iravanchi, M.M. Jaghoori, A. Shali Model Checking in Rebeca in the Proceedings of The 2003 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'03), CSREA Press, June 2003.   M. Sirjani, A. Movaghar, H. Iravanchi, M.M. Jaghoori, A. Shali. Model Checking Rebeca by SMV in the Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS'03), University of Southampton, April 2003. 2002 M. Sirjani and A. Movaghar, Simulation in Rebeca in Proceedings of The 2002 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'02), CSREA Press, June 2002. Also presented on Automated Verification of Critical Systems (AVoCS'02), University of Birmingham, April 2002. 2001 M. Sirjani, A. Movaghar, and M.R. Mousavi, Compositional Verification of an Actor-Based Model for Reactive Systems in Proceedings of Workshop on Automated Verification of Critical Systems (AVoCS'01), Oxford University, April 2001.   rebec : در Rebeca مدل سازي توسط reactive objects صورت مي گيرد . واژه rebec نيز از حروف re و bec كه در recatve object وجود دارد گرفته شده است. در rebeca به object ها rebec تلاق ميشود. هر rebec معرف يك active calss بوده و يك thread منحصر به فرد دارد. Message : پيامها در واقع عاملي براي انجام محاسبات تلقي مي شوند و تمامي محاسبات با ارسال پيام صورت گرفته و توسط احضار متد مربوط به پيام اجرا مي شوند. Method : هر پيام يك تابع نگهدارنده (method-handler) دارد كه متد ( method ) ناميده مي شود. پيامها با احضار اين متد ها ارسال و دريافت مي شوند. Inbox : هر rebec براي پيامهاي خود يك بافر نامحدود دارد كه به آن صف يا inbox اتلاق ميشود. وقتي كه يك پيام به ابتداي صف يك rebec رسيده باشد متد مربوطه احضار شده و پيام از صف حذف ميشود. تعاريف Class : هر Class الگويي براي حالات ( State )، رفتار (( behavior و رابطهايي براي recatve object مي باشد. Activeclass : هر activeclass شامل knownobject ها، متغيرهاي حالت(state variabels) و تعدادي message server است. تعاريف knownobject : Knownobject ها در واقعrebec هايي هستند كه مي توان به آنها پيام ارسال كرد و هر پيام شامل callee id ، message id وpassed parameters به سوي callee مي باشد. Rebeca model : برنامه هاي Rebeca شامل تعاريف (re)activeclass ها و يك بدنه اصلي مي باشد ودر بدنه اصلي rebec ها بوسيله activeclass ها معرفي مي شوند. ‍‍Close model : در Rebeca ، model از مجموعة محدودي rebec تشكيل شده كه به صورت موازي اجرا مي شوند. اگر تمامي درخواستهاي احضار متد در داخل model و به rebec هاي داخل مدل آدرس دهي شده ويا از rebec هاي داخل model سرچشمه گرفته باشد ، به چنين مدلي close model اتلاق مي شود . برعكس اين حالت open model ويا Component اتلاق مي شود. تعاريف Syntax Notation :