درستی یابی سیستم های واکنشی

درستی یابی سیستم های واکنشی

اسلاید 1: به نام خدا ارائه درس درستي يابي سيستم هاي واكنشي موضوع : Rebeca (Reactive Object Language) ارائه دهنده : محمد ابراهيمي mebrahimi76@gmail.com تير 1384

اسلاید 2: فهرست مطالب - نگاه كلي به زبان Rebeca - روشهاي درستي يابي - درستي يابي تركيبي - كمينه سازي تركيبي - درستي يابي تركيبي Rebeca - مثال (سيستم كنترل كننده خط آهن) - نتيجه گيري

اسلاید 3: real applications نگاه كلي به زبان RebecaRebeca زباني است شيءگرا مبنتي بر مدل Actor براي مدلسازي سيستم هاي واكنشي است. مزاياي Rebeca : استفاده از يك زبان شيءگرا براي مدلسازي ترجمه آن به زبانهاي Model cheking است كه امكان درستي يابي را با كمك Model cheking فراهم مي سازد. تاريخچه: مدل هاي شي گرا براي سيستم هاي همروند از دهه ي هشتاد تا كنون مطرح شده اند تفاوت عمده مدل هاي شيء گرا نسبت به ساير مدل ها : تاكيد بر روي درستي يابي بخصوص درستي يابي تركيبي است.

اسلاید 4: real applications نگاه كلي به زبان Rebeca خلاصه اي از جزئيات : Rebeca مانند Actor داراي اشياء فعال مستقل، تبادل ناهمگام پيام، تغيير پوياي پيكر بندي و بافر هاي نا محدود براي پيامهاي دريافتي است،اما در اين مدل ريسمانهاي متعدد همروند درون يك شيء فعال وجود ندارند. ساده سازي در Rebeca : به منظور كاهش پيچيدگي فرآيند درستي يابي، از امكان ايجاد پوياي يك شيء فعال و تغيير هم بندي در زمان اجرا، در هنگام ارائه روشهاي درستي يابي صرف نظر شده است.

اسلاید 5: real applications نگاه كلي به زبان RebecaRebec : از مهم ترين مشخصه هاي اشياء در اين مدل، واكنشي بودن آنها است، به همين دليل هر يك از اشياء در اين مدل Rebec ناميده مي شود و مدل ارائه شده Rebeca نامگذاري شده است. ‍Class : در مدل ربكار امكان تعريف كلاس( رده) وجود دارد كه باعث افزايش قابليت استفاده مجدد( Reuse ) در سطح مدل و همچنين هنگام درستي يابي مي شود. Message : اجراي عمليات در سيستم توسط تبادل پيام و اجراي روالهاي كارگزار انجام مي پذيرد. پيامهاي رسيده به هر ربك در يك بافر نامحدود به نام صندوق پستي به صورت صف ذخيره مي شوند.

اسلاید 6: real applications :Method هر پيام دريافتي داراي يك روال متناظر است كه رسيدن پيغام به ابتداي صف موجب فراخواني آن مي گردد و فراخواني هر روال موجب برداشته شدن پيغام مربوطه از ابتداي صف مي شود. :Component يك موئلفه از تعدادي Rebec تشكيل شده است كه به صورت همزمان اجرا مي شوند و با يكديگر و همچنين ربك هاي ديگر غير حاضر در آن مؤلفه تعامل دارند. ربك هاي موجود در يك مؤلفه ربك هاي داخلي و ربك هاي ديگر ربك هاي خارجي ناميده مي شوند.پيغامها نيز با توجه به فرستنده آنها به دو دسته داخلي و خارجي تقسيم مي شوند. نگاه كلي به زبان Rebeca

اسلاید 7: real applications در مدل سازي يك مؤلفه، پيغامهاي خارجي محيط مؤلفه را شبيه سازي مي كنند. از آنجايي كه محيط قابل پيش بيني نيست اين پيغامها هميشه حاظر در نظر گرفته مي شوند. پيغامهاي داخلي در صندوق پستي مؤلفه مقصد كه مانند صف عمل مي كند، قرار مي گيرند و توسط ربك مورد نظر سرويس داده مي شوند. اجراي روالها به طور موازي با يكديگر و هر يك با يك رسمان اجرائي، ادامه مي يابد. اين اجرا شامل برداشت پيغام از ابتداي صف و فراخواني روال متناظر آن است. هر گاه ربك داراي پيغام منتظر در صف نباشد، در حالت بيكار باقي مي ماند. بخشي از محاسبات و عدم قطعيت موجود در سيستم به وسيله نا همگامي تبادل پيغامها مدل مي شود. اجراي متد يك عمل اتميك است كه با رسيدن يك پيغام حاصل مي شود و نتيجه آن يك گذار به شمار نمي آيد. نگاه كلي به زبان Rebeca

اسلاید 8: real applications :Known Rebec هر ربك داراي فهرستي از ربك هاي آشنا است كه فرستاده پيغام تنها به آنها امكان دارد.متد هاي ربك هاي آشنا كه امكان صدا كردن آنها وجود دارد نيز مشخص مي باشد. Initial Method: هر ربك داراي يك روال براي تنظيم مقادير اوليه است. به هنگام شروع كار سيستم، اين روال ها به صورت ضمني فراخواني مي شوند. Tools : براي درستي يابي كدهاي نوشته شده به زبان ربكا يك ابزار خودكار توليد شده است كه امكان وارد كردن كد ربكا؛ بررسي نحو آن و آزمون مدل را در اختيار كاربر قرار مي دهد.نگاه كلي به زبان Rebeca

اسلاید 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: در درستي يابي تركيبي ربكا كارهاي زير قابل انجام است: مدلسازي محيط تجريد محيط تجريد صف از پيغامهاي خارجي تجريد پارامترها؛ تغيير پوياي پيكربندي، ايجاد پوياي ربك ها تجزيه مدل و تركيب مولفه ها اثبات نظريه درستي يابي ربكا با استفاده از چند تعريف و قضيه نظريه درستي يابي ربكا اثبات شده است كه در مرجع اين ارائه يعني پايان نامه دكترا خانم دكتر سيرجاني تحت عنوان توصيف و درستي يابي صوري سيستم هاي همروند و واكنشي ذكر شده است كه از ذكر آن صرف نظر شده است.درستي يابي تركيبي Rebeca

اسلاید 18: سيستم كنترل كننده خط آهن با استفاده از ربكا نوشته شده است. اين مثال به صورتهاي مختلف در متون مربوط به درستي يابي سيستم هاي واكنشي مورد بحث قرار گرفته است و مي تواند نمونه خوبي براي نمايش و توضيح روش درستي يابي و همچنين مقايسه و ارزيابي مدل پيشنهادي و شيوه درستي يابي آن نسبت به شيوه هاي ديگر باشد. در تعريف اين مسئله در قسمتي از مسير راه آهن دوطرفه، يك پل وجود دارد كه در آن واحد فقط يك قطار مي تواند از روي آن بگذرد. در دو طرف اين پل، چراغ هايي وجود دارد كه فقط به يكي از قطارهايي كه از دو طرف به پل مي رسند اجازه عبور مي دهد. هر قطار تنها در صورتي مي تواند از روي اين پل عبور كند كه چراغ مربوط به ورود به پل از آن سمت سبز باشد. اگر چراغ مربوط قرمز باشد، قطار بايد تا سبز شدن ان صبر كند. سيستم كنترل كننده خط آهن

اسلاید 19: سيستم كنترل كننده خط آهن مدل بسته سيستمبا استفاده از دو روش درستي يابي اين سيستم بررسي مي شود: مدل بسته سيستم مول مؤلفه خصوصيات مطلوب در اين مسئله : شرط ايمني:هيچ گاه نبايد دو قطار هم زمان اجازه عبور از روي پل را به دست آورند شرط پيشرفت :درعين حال همه قطارها كه از دو طرف به سمت پل مي آيند بايد در نهايت بتوانند اجازه عبور از روي پل را بدست اورند

اسلاید 20: سيستم كنترل كننده خط آهن مدل بسته سيستم

اسلاید 21: سيستم كنترل كننده خط آهن مدل بسته سيستم

اسلاید 22: اين سيستم شامل دو كلاس يا رده مي باشد: يك رده كنترل كننده پل (Bridge Controller) است كه از تصادف دو قطار جلو گيري كرده و امنيت پل را تامين ميكند. يك رده براي تعريف قطارها (Train). هر قطار روي خط آهن در حال حركت است تا هنگامي كه پيام ReachBridge از بافر برداشته شده و كارگزار مربوط به آن اجرا شود. در اينجا قسمتي از محاسبه ( حركت قطار روي خط آهن قبل از رسيدن به پل) به وسيله ناهمگامي پيامها مدل شده است. پس از اجراي كارگزار اين پيام، قطار به پل رسيده است و رسيدن خود را با پيام Arrive به كنترل كننده اطلاع مي دهد. در اين هنگام چون پيامي در بافر قطار وجود ندارد به حالت انتظار باقي مي ماند. كنترل كننده پس از دريافت پيام Arrive، وضعيت چراغ سوي ديگر پل را بررسي مي كند و در صورت قرمز بودن، چراغ مربوط به اين قسمت را به سبز تغيير داده و با پيام Youmay pass به درخواست كننده اجازه عبور مي دهد. در غير اينصورت يك متغيير داخلي به نام IsWaiting را براي اين قطار تنظيم ميكند تا وضعيت قطار به عنوان منتظر اجازه عبور ثبت شود.سيستم كنترل كننده خط آهن مدل بسته سيستم

اسلاید 23: با در يافت پيام YouMayPass قطار منتظر از روي پل عبور مي كند وپس از عبور پيام Passed را به خود مي فرستند. در اين جا نيز زمان عبور از روي پل به وسيله ناهمگامي پيامها، با زمان طي شده براي فراخواني كارگزار مربوط به پيام Passed مدل شده است. كارگزار پيام Passed، ترك پل را به كنترل كننده اعلام ميكند و كنترل كننده هنگام سرويس دادن به پيام ترك پل، وجود قطار منتظر در سوي ديگر پل را بررسي مي كند تا در صورت انتظار، اجازه عبور از پل را برايش صادر نمايد. سيستم در حال اجراي اين مدل متشكل از تعريف در ربك از رده Train و يك كنترل كننده پل است كه اجراي همروند انها، اجراي سيستم را مدل مي كند.سيستم كنترل كننده خط آهن مدل بسته سيستم

اسلاید 24: سيستم كنترل كننده خط آهن مدل بسته سيستم

اسلاید 25: سيستم كنترل كننده خط آهن مدل بسته سيستم

اسلاید 26: در مدل مؤلفه اين سيستم مدل به دو مؤلفه هركدام شامل رده BridgeControl() و Train() تقسيم شده است. در اين مدل متغير هاي حالت ربك Train2 از مدل حذف شده اند. اين مدل شامل رده خارجي XTrain() است. اين رده مرتباً پيغامهاي Arrive() و Leave() را به كنترل كننده ارسال مي كند. خصوصيات ايمني و پيشرفت براي مدل مؤلفه ارائه شده به صورت زير است: سيستم كنترل كننده خط آهن مدل مولفه

اسلاید 27: نتيجه گيري

اسلاید 28: نتيجه گيري