بخشی از پاورپوینت
اسلاید 1 :
به نام خدا
ارائه درس درستي يابي سيستم هاي واكنشي
موضوع : Rebeca (Reactive Object Language)
اسلاید 2 :
فهرست مطالب
- نگاه كلي به زبان Rebeca
- روشهاي درستي يابي
- درستي يابي تركيبي
- كمينه سازي تركيبي
- درستي يابي تركيبي Rebeca
- مثال (سيستم كنترل كننده خط آهن)
- نتيجه گيري
اسلاید 3 :
real applications
نگاه كلي به زبان Rebeca
Rebeca زباني است شيءگرا مبنتي بر مدل Actor براي مدلسازي سيستم هاي واكنشي است.
مزاياي Rebeca : استفاده از يك زبان شيءگرا براي مدلسازي ترجمه آن به زبانهاي Model cheking است كه امكان درستي يابي را با كمك Model cheking فراهم مي سازد.
تاريخچه:مدل هاي شي گرا براي سيستم هاي همروند از دهه ي هشتاد تا كنون مطرح شده اند
تفاوت عمده مدل هاي شيء گرا نسبت به ساير مدل ها : تاكيد بر روي درستي يابي بخصوص درستي يابي تركيبي است.
اسلاید 4 :
real applications
نگاه كلي به زبان Rebeca
خلاصه اي از جزئيات :Rebeca مانند Actor داراي اشياء فعال مستقل، تبادل ناهمگام پيام، تغيير پوياي پيكر بندي و بافر هاي نا محدود براي پيامهاي دريافتي است،اما در اين مدل ريسمانهاي متعدد همروند درون يك شيء فعال وجود ندارند.
ساده سازي در Rebeca :به منظور كاهش پيچيدگي فرآيند درستي يابي، از امكان ايجاد پوياي يك شيء فعال و تغيير هم بندي در زمان اجرا، در هنگام ارائه روشهاي درستي يابي صرف نظر شده است.
اسلاید 5 :
real applications
نگاه كلي به زبان Rebeca
Rebec : از مهم ترين مشخصه هاي اشياء در اين مدل، واكنشي بودن آنها است، به همين دليل هر يك از اشياء در اين مدل Rebec ناميده مي شود و مدل ارائه شده Rebeca نامگذاري شده است.
Class :در مدل ربكار امكان تعريف كلاس( رده) وجود دارد كه باعث افزايش قابليت استفاده مجدد( Reuse ) در سطح مدل و همچنين هنگام درستي يابي مي شود.
Message : اجراي عمليات در سيستم توسط تبادل پيام و اجراي روالهاي كارگزار انجام مي پذيرد. پيامهاي رسيده به هر ربك در يك بافر نامحدود به نام صندوق پستي به صورت صف ذخيره مي شوند.
اسلاید 6 :
real applications
:Method هر پيام دريافتي داراي يك روال متناظر است كه رسيدن پيغام به ابتداي صف موجب فراخواني آن مي گردد و فراخواني هر روال موجب برداشته شدن پيغام مربوطه از ابتداي صف مي شود.
:Component يك موئلفه از تعدادي Rebec تشكيل شده است كه به صورت همزمان اجرا مي شوند و با يكديگر و همچنين ربك هاي ديگر غير حاضر در آن مؤلفه تعامل دارند.
ربك هاي موجود در يك مؤلفه ربك هاي داخلي و ربك هاي ديگر ربك هاي خارجي ناميده مي شوند.پيغامها نيز با توجه به فرستنده آنها به دو دسته داخلي و خارجي تقسيم مي شوند.
اسلاید 7 :
real applications
در مدل سازي يك مؤلفه، پيغامهاي خارجي محيط مؤلفه را شبيه سازي مي كنند. از آنجايي كه محيط قابل پيش بيني نيست اين پيغامها هميشه حاظر در نظر گرفته مي شوند. پيغامهاي داخلي در صندوق پستي مؤلفه مقصد كه مانند صف عمل مي كند، قرار مي گيرند و توسط ربك مورد نظر سرويس داده مي شوند. اجراي روالها به طور موازي با يكديگر و هر يك با يك رسمان اجرائي، ادامه مي يابد. اين اجرا شامل برداشت پيغام از ابتداي صف و فراخواني روال متناظر آن است. هر گاه ربك داراي پيغام منتظر در صف نباشد، در حالت بيكار باقي مي ماند.
بخشي از محاسبات و عدم قطعيت موجود در سيستم به وسيله نا همگامي تبادل پيغامها مدل مي شود. اجراي متد يك عمل اتميك است كه با رسيدن يك پيغام حاصل مي شود و نتيجه آن يك گذار به شمار نمي آيد.
اسلاید 8 :
real applications
:Known Rebec هر ربك داراي فهرستي از ربك هاي آشنا است كه فرستاده پيغام تنها به آنها امكان دارد.متد هاي ربك هاي آشنا كه امكان صدا كردن آنها وجود دارد نيز مشخص مي باشد.
Initial Method:هر ربك داراي يك روال براي تنظيم مقادير اوليه است. به هنگام شروع كار سيستم، اين روال ها به صورت ضمني فراخواني مي شوند.
Tools :براي درستي يابي كدهاي نوشته شده به زبان ربكا يك ابزار خودكار توليد شده است كه امكان وارد كردن كد ربكا؛ بررسي نحو آن و آزمون مدل را در اختيار كاربر قرار مي دهد.
اسلاید 9 :
real applications
براي درستي يابي يك مدل P، بايستي خصوصيات مورد نظر آن به صورت توصيف φ نوشت. مدل P رفتارهاي ممكن سيستم را مشخص مي كند و توصيف φ رفتار دلخواه سيستم است.
بررسي و اثبات برآروده شدن خواص دلخواه توسط مدل، وظيفه تحليل صوري است.
روش تحليل مي تواند به دو صورت الگوريتميك ( وارسي الگو- Model cheking) و يا استنتاجي باشد
در وارسي الگو يك شبيه سازي كامل از مدل روي تمام حالتهاي ممكن انجام مي شود. اين تحليل بايد به وسيله يك ابزار نرمافزاري انجام گيرد
در روش استنتاجي، مسئله تحليل به صورت يك قضيه در يك سيستم اثبات رياضي مطرح مي شود و طراحي سعي دارد از يك اثبات كننده خودكار قضيه، اثبات مورد نظر را انجام دهد.
اسلاید 10 :
real applications
بيان خصوصيات مورد نظر در درستي يابي، نيازمند روشي رياضي است. روشهاي بيان خصوصيات: منطق زماني روشهاي ميتني بر نظريه ماشين ها در ربكا به طور خاص از منطق زماني خطي استفاده شده است. ساختار منطق زماني ابر مجموعه اي از ساختار منطق گزاره ها است، بنا براين گزاره هاي منطق گزاره ها ( گزاره هايي در مورد مقادير متغير هاي يك حالت) و عملگرهاي اين منطق ( مانند عملگرهاي نقيض ( ~) و يا (v) ) در اين منطق وجود دارند.
اسلاید 11 :
real applications
روشهاي درستي يابي
اسلاید 12 :
علت رويكرد به درستي يابي تركيبي :براي درستي يابي صوري سيستم هاي واقعي مشكلاتي وجود دارد. در درستي يابي سيستم هاي بزرگ، قضيه هايي كه بايستي اثبات شوند معمولا در حدتوان خبرگان نيستند. در model cheking هم هنگامي كه سيستم از پيچيدگي بالايي برخوردار باشد دچار مسئله ي قابل پيش بيني انفجار حالت مي شويم.
درستي يابي تركيبي براي جلو گيري از انفجار حالت و در نتيجه ايجاد امكان درستي يابي صوري سيستم هاي واقعي به كار مي رود. در اين نوع درستي يابي از تجزيه مدل به مؤلفه هاي تشكيل دهنده، درستي يابي هر يك از اجزاء و استنتاج خواص كل سيستم از خواص اجزاي تشكيل دهنده آن استفاده مي شود. كه براي انجام آن راههاي گوناگوني وجود دارد.
اسلاید 13 :
براي انجام درستي يابي تركيبي در ساده ترين شكل سيستم را مركب از دو پيمانه P و Q در نظر مي گيريم كه با محيط خود در ارتباط هستند.
درستي يابي تركيبي
اين سيستم را با P║Q نمايش مي دهيم.اگر توصيف خصوصيات φp را براي P و φQ را براي Q داشته باشيم، مسئله درستي يابي تركيبي، در حالت كلي به صورت قاعده زير خلاصه مي شود.آنچه كه در اينجا بايستي در نظر گرفت، نحوه تاثير گذاري P وQ بر يكديگر است و همچنين خصوصيات φpو φQاستبه بيان ديگر، تركيب P و Q نبايستي به گونه اي باشد كه هر يك از دو خاصيت فوق در P║Q از بين برود.
اسلاید 14 :
درستي يابي تركيبي
نكته اي كه بايستي در اينجا به آن اشاره شود اين است كه :
معمولا در درستي يابي تركيبي خواص ايمني مورد توجه قرار مي گيرند.
دليل :
استدلال در مورد خواص پيشرفت در درستي يابي تركيبي كار دشواري است. در اين روش اگر خاصيتي كه براي پيمانه P بيان مي شود، در مورد تمامي دنباله هاي محاسباتي ممكن ايجاد شده در اثر اجراي P برقرار باشد ( خاصيت از نوع خواص ايمني باشد) و Q روي داده هاي تحت كنترل P تاثير نگذارد، تركيب P و Q مي تواند حداكثر توليد برخي از اين دنباله هاي را غير ممكن سازد. اما بخشي از دنباله ها كه باقي مي مانند خواص هميشگي P را حفظ خواهند كرد. اما اگر خواص مورد بررسي در برخي دنباله ها برقرار باشند، نمي توان تضمين نمود كه در اثر اجراي تركيبي، اين خواص برجا بمانند.
اسلاید 15 :
كمينه سازي تركيبي
يكي از روشهايي كه در درستي يابي تركيبي مورد استفاده قرار مي گيرد، كمينه سازي تركيبي است.در روش كمينه سازي تركيبي يك نسخه كاهش يافته ׳ Q از Q مشتق مي شود كه تنها رفتاري از Q را مشخص مي كند كه براي P قابل مشاهده است.
با پنهان ساختن آن دسته از ارتباطات Q كه براي P قابل مشاهده نيست، مي توانيم Q را پيمانه اي كاهش دهيم كه تعداد حالتهاي بسيار كمتري دارد. كه براي اثبات خواص سيستم از قواعد رو برو استفاده مي شود. مقصود از عملگرP ↓Σ در قاعده فوق كاهش الفباي Q به الفباي P و حذف متغيرهاي غير مشترك از فضاي حالت ׳ Q است.
اسلاید 16 :
درستي يابي تركيبي Rebeca
در ربكا بدون هيچ شرطي روي اشياء واكنشي، مي توان درستي يابي تركيبي انجام داد و اين مسئله از نقاط قوت ربكا است. عدم تاثير اشياء بر داده هاي مشترك سبب مي شود كه درستي يابي تركيبي بدون قيد و شرط بر روي آنها قابل اعمال باشد.
در ربكا براي انجام درستي يابي تركيبي مي توان مدل بسته سيستم را به دو قسمت مؤلفه و محيط تجزيه كرد. با انجام اين تجزيه، مشخص مي شود كه حالت و رفتار كدام Rebec ها (Rebec هاي داخلي مؤلفه) بايستي به طور كامل مدل شود و كدام Rebec ها (Rebec هاي محيط) به طور مجرد يا كمينه مدل گردند. در مورد Rebec هاي محيط تنها عمليات فرستادن پيغام به Rebec هاي داخلي مؤلفه از رفتار آن مدل مي گردد. مؤلفه پس از تركيب با محيط خود، دوباره مدلي بسته را بوجود مي آورد كه به آن مدل مؤلفه مي گوئيم
اسلاید 17 :
در درستي يابي تركيبي ربكا كارهاي زير قابل انجام است:
مدلسازي محيط
تجريد محيط
تجريد صف از پيغامهاي خارجي
تجريد پارامترها؛ تغيير پوياي پيكربندي، ايجاد پوياي ربك ها تجزيه مدل و تركيب مولفه ها
اثبات نظريه درستي يابي ربكا
با استفاده از چند تعريف و قضيه نظريه درستي يابي ربكا اثبات شده است كه در مرجع اين ارائه يعني پايان نامه دكترا خانم دكتر سيرجاني تحت عنوان توصيف و درستي يابي صوري سيستم هاي همروند و واكنشي ذكر شده است كه از ذكر آن صرف نظر شده است.
اسلاید 18 :
سيستم كنترل كننده خط آهن با استفاده از ربكا نوشته شده است. اين مثال به صورتهاي مختلف در متون مربوط به درستي يابي سيستم هاي واكنشي مورد بحث قرار گرفته است و مي تواند نمونه خوبي براي نمايش و توضيح روش درستي يابي و همچنين مقايسه و ارزيابي مدل پيشنهادي و شيوه درستي يابي آن نسبت به شيوه هاي ديگر باشد.
در تعريف اين مسئله در قسمتي از مسير راه آهن دوطرفه، يك پل وجود دارد كه در آن واحد فقط يك قطار مي تواند از روي آن بگذرد. در دو طرف اين پل، چراغ هايي وجود دارد كه فقط به يكي از قطارهايي كه از دو طرف به پل مي رسند اجازه عبور مي دهد. هر قطار تنها در صورتي مي تواند از روي اين پل عبور كند كه چراغ مربوط به ورود به پل از آن سمت سبز باشد. اگر چراغ مربوط قرمز باشد، قطار بايد تا سبز شدن ان صبر كند.
سيستم كنترل كننده خط آهن
اسلاید 19 :
سيستم كنترل كننده خط آهن مدل بسته سيستم
با استفاده از دو روش درستي يابي اين سيستم بررسي مي شود:مدل بسته سيستم / مول مؤلفه
خصوصيات مطلوب در اين مسئله :شرط ايمني:هيچ گاه نبايد دو قطار هم زمان اجازه عبور از روي پل را به دست آورند
شرط پيشرفت :درعين حال همه قطارها كه از دو طرف به سمت پل مي آيند بايد در نهايت بتوانند اجازه عبور از روي پل را بدست اورند
اسلاید 20 :
سيستم كنترل كننده خط آهن
مدل بسته سيستم
