ارائه درس درستی يابی سيستم های واكنشی

صفحه 1:
Verification of Reactive Systems REBECA ‏به نام خدا‎ ‏سیستم‎ cul ‏ارائه درس درستي‎ : ‏موضوع‎ ‎Rebeca (Reactive Object Language) ارائه دهنده : محمد ابراهيمي اتير 1384 

صفحه 2:
Verification of Reactive Systems REBECA - نگاه كلي به زبان سس - روشهاي درستي يابي - درستي يابي تركيبي - کمینه سازي تركيبي - درستي يابي تركيبي ‎Rebeca‏ ثال (سیستم کنترل کننده خط آهن) گيري 

صفحه 3:
Verification of Reactive Systems نگاه كلي به ‎REBECA Rebeca yl‏ 2 وزبانيلسنش گرا مبنتيسر مدل۸001 بوليمدلسازي سيستمهاووالكنشييست مزليايه»1۵06 : لستفاده از بلزبان‌شسیگرا بولومدلسازي ترجمه آنسه زبانهای616170 1 1۷10001 1سنکه لمکان ديستيلبي را با کمك0 00102 1۷۲0061 ف رلهم‌مي‌سازد. 1 تاریخچه: مدل‌هاي‌شي‌گرا بسولي‌سیستم‌هاي‌همروند از دهه ي هشتاد تا کنون‌مطرح 

صفحه 4:
نگاه ‎Is‏ به زبان ‎Systems‏ فيد تسسا ‎Rebeca‏ خلاصه اي از جزئیات : 5 مانند ۸60۲ داراي اشیاء فعال مستقل. تبادل ناهمگام پیام. یر پوياي پیکر بندي و بافر هاي نا محدود براي پيامهاي دريافتي است.اما در این مدل ربسمانهاي متعدد همروند درون يك شيء فعال وجود ندارند. ساده سازي 59 ‎Rebeca‏ : یه منظور کاهش پيچيدگي فرآیند درستي يابيء از امکان ایجاد بو بك 

صفحه 5:
‎Verification of Reactive Systems ١ ۲ <€.‏ نكاه كلي 4 ‎REBECA . alia‏ »و۳8 از مهم ترين»_شخصه هايلشياء در لميرهدل ولكنشي ود وآنهالستبه همین ملیلهر ب از لشیاء در لینمدل6 6 ‎3٩613‏ ننامیده مي‌شود و مدلاراثه شدء 18619668 نامكناييوشدملست 7 ‎:Class ‏در مدلربکار لمکانت_عریفک ای ردم) وجود دارد که باعثفلیشقلبلیت لستفاده مجددد 1361156 ) در سطح مد[و همچنیرهنگام دیستیب لبیمی ‏شود. ‎ ‎ ‎: Messa ‏پاندر سیستم توسط تبادل‌پیام و (جولور وا لهايک ارگزار لنجام‎ ‎Ms 2‏ هد بههر يبئدر يكبافر نامحدود به نام صنشوقيستي غضخیره می‌شوند. 

صفحه 6:
Verification of Reactive Systems نگاه كلي به زبان 166602 ‎REBECA‏ Method: ‏هر پیام دريافتي داراي يك روال متناظر است که رسیدن پیغام به ابتداي صف موجب‎ ‏فراخواني آن مي گردد و فراخواني هر روال موجب برداشته شدن پیغام مربوطه از‎ ‏ابتداي صف مي شود.‎ Component: یک موئلنه از تعدادی 1301266 تشکیل شده است که به صورت همزمان اجبرا می شوند و با یکدیگر ین ریک های دیگ غیر حاضبس در آن مولفه تعامل دارند. موجود در یک مولفه ریک های داخلی و ربک های دیگر ریک های خارجی نامیده می نیز با توجه به فرستنده آنها به دو دسته داخلی و خارجی تفسیم می شوند. 

صفحه 7:
Verification of Reactive Systems نگاه كلي به زبان 166602 ‎REBECA‏ در مدل ساز: بيغامهاي خارجي محيط مؤلفه را شبيه سازي مي كنند. از آنجايي که محیط قابل بيش بيني نیست این پیغامها هميشه حاظر در نظر گرفته مي شوند. پيغامهاي داخلي در صندوق پستي موّلفه مقصد که مانند صف عمل مي کند. قرار مي گیرند و توسط ربك مورد نظر سرویس داده مي شوند. اجراي روالها به طور موازي با یکدیگر و هر يك با يك رسمان اجرائي. ادامه مي يابد. این اجرا شامل برداشت پیغام از ابتداي صف و فراخواني روال متناظر آن است. هر كاه ربك داراى ب م منتظر در صف نباشد. در حالت بیکار باقي می ماند. شود. اجراي متد يك عمل اتميك است که با رسیدن يك پیغام نتیجه آن يك گذار به شمار نمي آید. 

صفحه 8:
Verification of Reactive Systems نگاه كلي به زبان 166602 ‎REBECA‏ Known Rebec: هر ربك داراي فهرستي از ربك هاي آشنا است که فرستاده پیغام تنها به آنها امکان دارد.متد هاي ربك هاي آشنا که امکان صدا کردن آنها وجود دارد نیز مشخص مي باشد. ‘Initial Method ‏هر ربك داراي يك روال براي مقادير اولیه است. به هنگام شروع کار سیستم.‎ ‏اين روال ها به صورت ضمني فراخواني مي شوند.‎ يابي كدهاي نوشته شده به زبان ربكا يك ابزار خودكار توليد شده است ؛ كردن كد ربكا؛ بررسي نحو آن و آزمون مدل را در اختيار كاربر قرار 

صفحه 9:
Verification of Reactive Systems REBECA ‏روشهاي درستي يابي‎ براي درستي يابي يك مدل *. بايستي خصوصیات مورد نظر آن به صورت توصیف © نوشت. مدل ۳ رفتارهاي ممکن سیستم را مشخص مي کند و توصیف م) رفتار دلخواه سیستم است. بررسي و اثبات برآروده شدن خواص دلخواه توسط مدل, وظیفه تحلیل صوري است. روش تحلیل مي تواند به دو صورت الگوريتميك ( وارسي الگو- 1۷۲0061 0 )و يا استنتاجي باشد. الگو يك شبیه سازي کامل از مدل روي تمام حالتههاي ممکن انجام مي به وسیله يك ابزار نرمافزاري انجام گیرد. 

صفحه 10:
Verification of Reactive Systems REBECA wl ‏روشهاي درستي‎ بیان خصوصیات مورد نظر در درستي روشهاي بیان خصوصیات: منطق زماني روشهاي ميتني بر نظریه ماشین ها در ربکا به طور خاص از منطق زماني خطي استفاده شده است. ساختار منطق زماني ابر مجموعه اي از ساختار منطق گزاره ها است. بنا براین گزاره ق گزاره ها ( گزاره هايي در مورد مقادیر متغیر هاي يك حالت) و عملگرهاي ( مانند عملگرهاي نقیض ( -) و یا () ) در این منطق وجود دارند. ي. نیازمند روشي رياضي است. 

صفحه 11:
Verification of Reactive Systems REBECA ‏روشهاي درستي يابي‎ نحو یک فرمول زمانی در منطق زمانی به صورت باز گشتی و به شکل منام| 9 | مت | ۷۵و2۱ 02 دهنده عبارت منطق گزاره ما و ۵ نماینده عبارث حو با توجه به حالتی که عبارت پر روی آن بنا شده است حالت 8 عبارت منطق زمانی 6 را ارضا می‌کند (0 ۸۲۸ )اگر و فقط اگر: اگر -©ءو 7 یک گزاره باشد: ۸ بر روی مقادیر متغیرهای ۶ درست باشد. اگر ۵26,۷0 : 9 در 5 ارضا شود یا 9 در 8 ارضا شود. اكر ,© - © : ,©در 5 ارضا نشود اكر ,ملا -م ,9 در حالت بعد از 5 در ساختار مشاهداتی درست باشد اگر ومنا,<م: ,م تا برقرار شدن رم در حالت‌های مجود در ساختار مشاهداتی درست باشد. 

صفحه 12:
Verification of Reactive Systems درستي يابي تركيبي ‎REBECA‏ علت رویکرد به درستي يابي تركيبي : براي درستي بابي صوري سیستم هاي واقعي مشكلاتي وجود دارد. در درستی يابي سیستم هاي بزرگ, قضیه هايي که بايستي اثبات شوند معمولا در حدتوان خبرگان نیستند. در 0616060 ۳0061 هم هنگامي که سیستم از پيچيدگي بالايي برخوردار باشد دچار مسئله ي قابل پیش بيني انفجار حالت مي شویم. درستي يابي تركيبي براي جلو كيري از انفجار حالت و در نتیجه ایجاد امکان زيه مدل به مؤلفه هاي تشكيل دهنده. درستي اج خواص كل سيستم از خواص اجزاي تشكيل 

صفحه 13:
Verification of Reactive Systems درستي يابي تركيبي ‎REBECA‏ براي انجام درستي يابي تركيبي در ساده تربن شکل سیستم را مرکب از دو پیمانه و 0 در نظر مي گیریم که با محبط خود در ار تباط هستند. > 0 م لو ‎"it‏ « اين سيستم را با © || 8 نمايش مي دهيم. اگر توصیف خصوصیات ,40 را براي 8 و ۵۵ را براي 0 داشته باشیم. مسئله درستي يابي تركيبي, در حالت كلي به صورت قاعده زير خلاصه مي ذ اینجا بايستي در نظر گرفت. نحوه تاثیر گذاري ,0 ۲۲ یکدیگر است و همچنین خصوصیات ,0), )اس % ‎Or‏ ‏ترکیب و ۵ تايستي به گونه اي باشد ۳ * | م جیهم بر ل 

صفحه 14:
Verification of Reactive Systems REBECA ‏تانق فرگتی‎ asa نکته اي که بايستي در اینجا به آن اشاره شود این است که : معمولا در درستي يابي تركيبي خواص ايمني مورد توجه قرار مي گيرند. دلیل : استدلال در مورد خواص پیشرفت در درستي يلبي تركيبي کار دشواري است. در اين روش اگر خاصيتي که براي پیمانه ۳ بیان مي شود. در مورد تمامي دنباله هاي محاسباتي ممکن ایجاد شده در اثر اجراي ۳ برقرار باشد ( خاصیت از نوع خواص ایم: باشد) و 0۵ روي داده هاي تحت کنترل ظ تاثیر نگذارد. ترکیب ‎P‏ و © مي تواند حداكثر توليد برخي از اين دنبلله هاي را غير ممكن سازد. اما بخشي از دنبلله ها كه مي مانند خواص هميشكي 7 را حفظ خواهند كرد. اما اكر خواص مورد بررسي در دنبلله ها برقرار باشند. نمي توان تضمين نمود كه در اثر اجراي تركيبي. اين 

صفحه 15:
Verification of Reactive Systems REBECA Ss pula ans يكي از روشهايي که در درستي يابي تركيبي مورد استفاده قرار مي گیرد. کمینه سازي تركيبي است.در روش کمینه سازي تركيبي يك نسخه کاهش یافته " ۵ از ۵ مشتق مي شود که تنها رفتاري از 0 را مشخص مي کند که براي 8 قابل مشاهده است. و ‎+o‏ > 1 > 2 و اس { ن ساختن آن دسته از ارتباطات © كه براي ۴ قابل مشاهده ,لامع 0 توانیم 0 را پیمانه اي کاهش دهیم که تعداد حالتهاي rE Lp , a a Pre ‏خوامن سیستم از قوف رو برو‎ SUN ely a8 Ss ۱۵ ۲, ودر قاعده فوق كاهش القباي © به الفباي ‏ | رم 09 |2 هاي غير مشترك از فضاي حالت ” © است. 

صفحه 16:
Verification of Reactive Systems REBECA ‏درستي يابي تركيبي‎ Rebeca در ربكا بدون هیچ شرطي روي اشیاء واكنشي, مي توان درستي يابي تركيبي انجام داد و ‎alts yl‏ فقاط قوث ربكا است«عدم تاثير اشياء بر داذه هاى مشترك سبب«مى شود كه درستي يابي تركيبي بدون قيد و شرط بر روي أنها قابل اعمال باشد. در ربكا براي انجام درستي يابي تركيبي مي توان مدل بسته سيستم را به دو قسمت مؤلفه و محيط تجزيه كرد. با انجام اين تجزيه. مشخص مي شود كه حالت و رفتار ‎Rebec) te REDEC plas‏ هاي داخلي مؤلفه) بايستي به طور کامل مدل شود و کدام 116166 ها ‎Rebec)‏ ‏هاي محیط) به طور مجرد یا کمینه مدل گردند. در مورد ‎Rebec‏ هاي محیط تنها فرستادن پیفام به 161086 هاي داخلي مولفه از رفتار آن مدل مي كردد. مؤلفه ركيب با محیط خود. دوباره مدلي بسته را بوجود مي آورد که به آن مدل مؤلفه 

صفحه 17:
Verification of Reactive Systems REBECA ‏درستي يابي تركيبي‎ Rebeca ‏در درستي يابي تركيبي ربكا كارهاي زير قابل‎ ‏انجام است:‎ ‏مدلسازي محيط‎ ‏تجريد محيط‎ ‏تجريد صف از بيغامهاي خارجي‎ ‏ايجاد يوياي ربك ها‎ sa Se ‏تجرید پارامتر‎ 1 ‏تجزیه مدل و ترکیب مولفه ها‎ اثبات نظریه درستي يابي ربکا اه از چند تریف و قضيه نظريه درستي بي ریا ثبات شده است كه در مرجع يعني پایان نامه دکترا خانم دکتر سيرجاني تحت عنوان توصیف و درستي يابي 

صفحه 18:
Verification of Reactive Systems _ 5 a 3 REBECA ‏سیستم كنترل كننده خط‎ تم کنترل کننده خط آهن با استفاده از ربکا نوشته شده است. این مثال به صورتهاي مختلف در متون مربوط به درستي يابي سیستم هاي واكنشي مورد بحث قرار گرفته است و مي تواند نمونه خوبي براي نمایش و توضیح روش درستي يابي و همچنین مقایسه و ارزيابي مدل پيشنهادي و شیوه درستي يابي آن نسبت به شیوه هاي دیگر باشد. در تعريف اين مسئله در قسمتي از مسیر راه آهن دوطرفه. يك پل وجود دارد که در آن واحد فقط يك قطار مي تواند از روي آن بگذرد. در دو طرف این پل. چراغ هايي وجود دارد که فقط به يكي از قطارهايي که از دو طرف به پل مي رسند اجازه عبور مي دهد. هر قطار تتها در صورتي مي تواند از روي این پل عبور کند که چراغ مربوط به ورود به پل از آن سمت سبز باشد. آگر چراغ مربوط قرمز باشد. قطار باید تا سبز شدن آن ضبر کند. 

صفحه 19:
Verification of Reactive Systemda> ‏سیستم کنترل كننده‎ REBECA ‏آهن‎ با استفادهل3 و روت تیم ميديم ةيوم سيستم بررسي مي شود: مدل بسته سيستم مول مؤلفه خصوصيات مطلوب در اين مسئله : شرط ايصفي :هيج كاه نبايد دو قطار هم زمان اجازه عبور از روي پل را به دست آورند شرط پیشرفت :درعین حال همه قطارها كه از دو طرف به سمت يل مى آيند بايد در نهايت بتوانند اجازه عبور از روي يل را بدست اورند G \{ traint.OnTheBridge & train2.OnTheBridge) GF( train1.OnTheBridge | train2.OnTheBridge) 

صفحه 20:
Verification of Reactive Systemda> oruS ‏سیستم کنترل‎ REBECA یکدیگر بر روی پل است و در منطق زمانی خطی به شکل زیر تعریف می‌شود: ‎((Trainl OnTheBridge » Train2.On'TheBridge))‏ لكل ‏قاعده کمینه‌سازی و قضیه استفاده می‌ضود ‎ ‎ ‎cl theController ‏خاصيت ايمنى‎ ‎ ‏(ز مععيع-[2الممعتكسعلامتممععل م ممعم[ ا المميتك عل امشممععط )دح عهلامسممعهطا و ‏خاصیت ایمنی ‎theController|Train‏ می‌توان را چنین نوشت: ‎gtheController||frain1= (Train On heBridge=> (theController.Signal[l]=green 4 theController.Signal[2|-red_)) ‏اما با توجه به قاعده کمینه‌سازی می‌نویسيم: ‎green )‏ ۱ به این ترتیب فضای حالت خلاصه می‌شود ‏از آنجایی که 11۵101 و 112102 هر دو از یک رده تعریف ده‌اند. می‌توانیم نتیجه بگیریم: ‎otheController|/Frain2 = ( Train2.OnTheBridge= theController.Signal[2 green ) 

صفحه 21:
Verification of Reactive Systemda> oruS ‏سیستم کنترل‎ REBECA ‏آهن‎ مدل بسته ستلسیم با استفاده از فسیه و استراندی انجام درست قابى قر یبی چنین عمل می‌کنیم: ‎ptheController|(Trainl a ptheController|[Train2 4 @theController =‏ ( (A(theController.Signal[1]-green theController.Signal[2]-green ))) 0 (. (Trainl.OnTheBridge= theController.Signal[1 J=green)) ‏م‎ ) (Train2.OnTheBridge= theController.Signal[2|-green)) => (A(Trainl.OnTheBridge Train2.OnTheBridge)) ‏به ابن ترتيب حصوصیت ایمنی کل سیستم از ترکیب خصرصبات ایمنی مژلفه‌های آن نتیجه گیری‎ ‏می‌شود‎ ‏پر اساس نتایج بدست آمده از آزمون مدل . نمودار گذار برای درستی‌یابی سیستم به صورت کلی‎ ای ۱۶4 حالت است. در صورت درستی‌یابی ترکیبی با استرا اتژی بیان شده تنها 1۸ حالت وجود دارد و بقیه کار با استفاده از استنتاج انجام می‌گیرد. 

صفحه 22:
Verification of Reactive Systemda> oruiS ‏سیستم کنترل‎ REBECA ‏آهن‎ این سیستم شامل دو کلاس يا رده مي باشد: يك رده کنترل کننده پل (0۳1۳01161) ۳11006) است که از تصادف دو قطار جلو كيري كرده و امنيت يل را تامين ميكند. يك رده براي تعریف قطارها (112110). هر قطار روي خط آهن در حال حرکت است تا هنگامي که پیام 1162011771006 از بافر برداشته شده و کارگزار مربوط به آن اجرا شود. در اینجا قسمتی از محاسبه ( حرکت قطار روي خط آهن قبل از رسیدن به پل) به وسیله ناهمکامي پیامها مدل شده است. پس از اجراي کارگزار این پیام قطار به پل رسیده است و رسیدن خود را با پيام ۸۸11176 به ل كننده اطلاع مي دهد. در اين هنكام چون پيامي در بافر قطار وجود ندارد به حالت داده و با پیام 0 به درخواست کننده اجازه عبور می دهد. در غیر اینصورت يك نام ‎ISWaiting‏ را براي این قطار تنظیم میکند تا وضعیت قطار به اجازه عبور ثبت شود. 

صفحه 23:
Verification of Reactive Systemda> oruS ‏سیستم کنترل‎ REBECA ‏أشن‎ با در يافت پیام ۷011۷1837۳255 قطار منتظر از روي بل عبور مي كند ويس از عبور پیام ۳35560 را به خود مي فرستند. در اين جا نيز زمان عبور از روي يل به وسيله ناهمكامي ييامهاء با زمان طي شده براي فراخواني كاركزار مربوط به بيام 2855601 مدل شده است. ۱ کارگزار پیام 25560 ترك پل را به کنترل کننده اعلام میکند و کنترل کننده هنگام سرویس دادن به پیام ترك پل. وجود قطار منتظر در سوي دیگر پل را بررسي مي کند تا در صورت انتظار» اجازه عبور از پل را برایش صادر نماید. در حال اجراي این مدل متشکل از تعریف در ربك از رده 112112 و يك کنترل است که اجراي همروند انهاء اجراي سیستم را مدل مي کند. 

صفحه 24:
Verification of Reactive Systemda> ‏سیبستم کنترل کننده‎ megery Leavet) { Tt [ender signal - tee Lf (iswsiting2) { eignal2 ~ truss 2 () : isWaiting? = false; 1 ‏امه‎ ‎signal? = fale; Lf (iswaitingl) { signal = true; ‏جع‎ YoutlayPase (I: isWaiting! - falaa; [+ ved ‏يع‎ 1 1 REBECA reactiveclass BridgeController (5) { Imownebjects { ‘Tain tl; Train ¢2) } staterare { boolean ieWaitingl; boolean isviaiting2; boolean signal; Boolean signal2, ) egery initial { Signall = false; /* red */ Signal? = false; /* ved */ Jotaivingl = faloer Ietiait ing? = false? 0 egery Arrive) { 1 TE (oondor == C1) { 1 if (eignalZ =~ False! { signal = true; /* green ¢/ 21 ‏مد قود اليد‎ امه ‎ieviaitingl = crue:‏ 1 اعمه ‎Gf (signal == false) {‏ signal? - true; /+ green ۸ +2 YowlayPass (1 elee{ ‏فوصت نطو‎ = crue; 1 1 ۱ 

صفحه 25:
Verification of Reactive Systemda> oruS ‏سیستم کنترل‎ REBECA ‏آهن‎ مدل بسته سیستم { ‎reactiveclase Train(2)‏ Knownobjecte [ BridgeCont roller controller; 1 اعد سم و 1 نخان مدعوما ‎case‏ 0 مسحت ۱ 0[ ‎tao)‏ = ی 2 } ‎fegorr Feaeed. |‏ ‎Eatees‏ = ا ی ود ‎self Beseaiviase‏ } ‎msgsrv ReachBridge () {‏ ا 0 ۱ و 1 ‎met A‏ ور ‎Teas teaina (tnacont router!‏ ل ‎Tenin‏ ‏2 عم ا 1 ‎erainait or‏ 1 

صفحه 26:
Verification of Reactive Systemda> ori ‏سیم کنترل‎ REBECA ‏آهن‎ مدل مولفه در مدل مؤلفه اين سيستم مدل به دو ملفه هرکدام شامل ‎OBridgeControl os,‏ و 113112() تقسيم شده است. در اين مدل متغير هاي حالت ربك 1133122 از مدل حذف شده اند. اين مدل شامل رده خارجي ۲۵11 ]26() است. این رده مرتباً پينامهاي ۳۶6 )و 1,68۷6() را به کنترل کننده ارسال مي کند. یات ايمني و پیشرفت براي مدل مولفه ارائه شده به صورت زیر ا G \(theController.signal1 & theController.signal2) G F(theController.signal1 | theController.signal2) 

صفحه 27:
Verification of Reactive Systems یه گنوی ‎REBECA‏ بر اکتور در مدلسازی سیستم‌های همروند و توزیع شده مرفق پی صوری برای طراحی سیستم‌هایی با قابلیت اطمینان بالا رستی‌یابی صوری میستم‌های واقعی استفاده ست که مدل به صورت پیمانه‌ای طراحی شده باشد و پیمانه‌مای ی مدل کیسوله شده و با اتسال کم بافتتت :۱ کی برای پیمانه‌ما در رون مبتشن برستی‌یابی ترکیبی از آن بهره گرفت. یک ندل در ریک مجموعه‌ای غین تهی از ‎Sissel‏ iste gs نامحدود پیغام است. ی مجدد دهعت ساده کردن فرآیند درستی‌یابی وجود پرسیستم‌هاین انقنبیم: کرد. ابتدا حصویبانت ابن. مؤلقنها ‎ly‏ ترسط ستی‌یایی نموده و سپس استتتاج حصوصیت کل سیستم که حاصل ترکیب اين زیرسیسم‌هاست بدون هیچ فترطی زوی زیرسیسته‌ها امکانپذیراست, عمل, ترکیپ دو زیرسیستم 

صفحه 28:
Verification of Reactive Systems REBECA Ss ‏نتيجه كير‎ حل مشکل انفجار فضای حالت. از تجرید و "5 که اجرای فرستنده و گيرنده را مسدود نمی‌سازد. اجازه می‌دهد تا بدون ن استفاده شده است. تبادل ناهمگام پیام در بير خصوصيات سسعم (نْه جر من مواوم خاض) اناكذارساى درشت دائه استقاده كيم ومن تتيسيه مدل ساده‌تر شده و فضاى حالت كاهش مىيابد. نجريد از صف ييغامها در نوصيف خصوصيات سيستم نمونهى ديكرى از استفاده از ت ید است. علاوه پر تجرید. از تقارن موجود در سیستم و وجود مولفه‌های ‎yelp ob‏ سادهسازی عملیات درستی‌یایی سستم. اسفاده ‎ale‏