بخشی از پاورپوینت
اسلاید 1 :
به نام خدا
ارائه درس درستي يابي سيستم هاي واكنشي
موضوع : Rebeca (Reactive Object Language)
اسلاید 2 :
مقدمه
real applications
Rebeca
formal verification
يكي از ملزومات درستي يابي رسمي براي اطمينان از درستي سيستم ها داشتن يك روش كارآمد و مناسب براي مدل سازي سيستم هاي همروند و توزيع شده است.Rebeca يك زبان actor-base براي مدلسازي اين سيستم ها است. در واقع Rebeca تلاش ميكند همانند پلي ارتباطي ميان درستي يابي رسمي و application هاي واقعي عمل نمايد.
اسلاید 3 :
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 اتلاق مي شود.
اسلاید 4 :
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 ارائه شد.
اسلاید 5 :
مقالات 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.
اسلاید 6 :
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 رسيده باشد متد مربوطه احضار شده و پيام از صف حذف ميشود.
تعاريف
اسلاید 7 :
Class : هر Class الگويي براي حالات ( State )، رفتار (( behavior و رابطهايي براي recatve object مي باشد.
Activeclass : هر activeclass شامل knownobject ها، متغيرهاي حالت(state variabels) و تعدادي message server است.
تعاريف
اسلاید 8 :
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 اتلاق مي شود.
تعاريف
اسلاید 9 :
Syntax
Notation :
اسلاید 10 :
كد Rebeca شامل مجموعه اي ازتعاريف activeclass كه از يك بلاك اصلي تبعيت مي كنند مي باشد . هر rebec توسط activeclass هايش معرفي مي شود. اجباراً تمامي rebec ها بايستي ابتدا تعريف شوند.
Syntax
اسلاید 11 :
Syntax
Notation :recativeclasses
اسلاید 12 :
Syntax
Notation :knownobject
Knownobject هاي يك activeclass ، rebec هايي هستند كه هر نمونه activeclass مي تواند به آنها پيام ارسال كند. Synatx تعريف شده براي هر knownobject به صورت زير است:
هنگام تعريف rebec ها تعيين Knownobject ها در بلاك اصلي الزامي است.
اسلاید 13 :
Syntax
Notation :statevars
Notation :body
Notation :metod
تعريف متد :
هر پيام يك message-handler وابسته دارد كه متد ( method ) ناميده مي شود. هر پيام به سبب احضار يك متد خواهد رسيد. Syntax تعريف شده براي متد ها به شكل زير است:
اسلاید 14 :
پيامها ممكن است پارامترهايي از type هايي كه در heder متد مشخص شده است داشته باشد. بدنة msgsrv شامل برخي جملات rebec مي باشد.
اسلاید 15 :
هر activeclass شامل چند knownobject ، بيان متغير هاي حالت و مجموعه اي از سرويس دهنده هاي پيام يا متد مي باشد. هنگام معرفي rebecها تمامي activeclass ها بايستي يك سرويس دهنده پيام مشخص اوليه براي سرويس دادن به پيامهاي اوليه كه در صف پيامهاي rebec قرار دارند داشته باشند.
اسلاید 16 :
Syntax
Notation :parametrs
Notation :var
تمامي متغير ها قبل از استفاده بايستي تعريف شوند. متغير ها بايستي با يك حرف و يا يك زير خط شروع شوند همچنين ممكن است با هر تركيبي از حروف ، اعداد و زير خط تعريف شوند. Rebeca نسبت به كوچك و بزرگ بودن حروف حساس است.
اسلاید 17 :
Syntax
Notation :Statement
عبارات ( Expressions )
عبارات شامل عملگر هاي رياضي، منطقي و مقايسه اي مطابق جدول زير هستند:
Statement ها در Rebeca از اعمال پايه كه شامل ارسال و دريافت، تعاريف نوع داده، عبارات، عبارات مركب و كنترل ها مي باشند، ساخته شده است. دستورات توسط semicolon ها ( ; ) از هم تفكيك مي شوند و پايان هر خط لزوماً پايان دستورات نيست.
اسلاید 18 :
Syntax
Notation :mir (method invocation request)
اسلاید 19 :
اجراي يك دستورِ ارسال پيام شامل نام پيام با پارامتر هاي واقعي Par1 و . به يك knownobject است. از آنجايي كه message passing در rebeca به صورت غير هم زمان رخ مي دهد ، ممكن است پيام ها بعد از اينكه caller اقدامات خود را با محاسبات مربوط به خود انجام داد، در يك صف نا محدود callee ذخيره شود. وقتي كه اين پيام توسط callee خوانده شد متد متناظر احضار شده و اجرا مي شود.
همانطور كه در بالا ديديم دو نوع دستور ارسال وجود دارد؛ اولي پيام به knownobject ارسال مي شود و دومي پيام توسط caller به خودش ارسال مي شود، callee نيز ممكن است يك knownobject و يا خودِ caller باشد. در نوع دوم caller ، پيامها را در صف خودش قرار داده و با دستور بعدي كار خود را ادامه داد كه اين دو نوع ارسال پيامتفاوتي معنايي با هم ندارند.
دستورات ارسال و دريافت (Send and Receive statements ) :
Syntax ، دستورات ارسال و دريافت به صورت زير است:
اسلاید 20 :
Syntax
Notation :create
Notation :model
Notation : rebec
وقتي كه rebec ها از active class هاي متناضر معرفي مي شوند لزوما بايستي knownobject ها در بلاك اصلي تعريف شوند. Syntax معرفي rebec ها به صورت زير است:
