صفحه 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 نگاه كلي به
Rebeca زبانيلسنشیگرا مبنتيسر مدل۸601 بسولیمدلسازیسیستم
هایهلکنشییست
: RebecasLl.o
لستفاده از بكزبانش گرا
بسوليمدلسازي
آتسرجمه آنسه زبلنهاي0 016131 13) 1۷۲00161 1سنکه لمکان درستيی ابيرا با
Model chekinget_s فولهم ميسازد.
تاریخچه:
مدلهايشسيگرا بسولیسیستمهايهمروند از دهه ي هشتاد تا کنونسطرح شدم
صفحه 4:
نگاه Is به زبان Systems فيد تسسا
Rebeca
خلاصه اي از جزئیات :
5 مانند ۸60۲ داراي اشیاء فعال مستقل. تبادل ناهمگام پیام.
يبر پوياي پیکر بندي و بافر هاي نا محدود براي پيامهاي دريافتي است.اما
در این مدل ريسمانهاي متعدد همروند درون يك شيء فعال وجود ندارند.
ساده سازي .5 Rebeca :
نه منظور کاهش پيچيدگي فرآیند درستي يابيء از nae a بك
صفحه 5:
a Is oe زبان Systems فيد تسسا
Rebeca
: Rebec
از صهم تسرینشخصه هاولشیاء در لیرهدل ولکنشیبودنآنها لستبه همیرچلیلهر
یلا زلشیاء در لینمدل) 0 18013 نامیده ميشود و مدلارلئه شدمه
2 نامگناييشدملست
:Class
در مدلیبکار لمکانتعریفک لاو ردم) وجود دارد که باعظفزلیش ق لبلب
مجدد 1361156 ) در سطح مد[و همچنیرهنگام درستیب ابیمیشود.
: Message
ياتدر سيستم توسط تباد يبيام و جرلور وا لهايكا ركزار لمنجام مي
بيده بسه هر وباندر بلبافر نامحدود بسه نام صنوقپستوسه
خیرم ميشوند.
صفحه 6:
Verification of Reactive Systems
نگاه كلي به زبان 166602 REBECA
Method:
دريافتي داراي يك روال متناظر است که رسیدن پیغام به ابتداي صف موجب ely هر
فراخواني آن مي گردد و فراخواني هر روال موجب برداشته شدن پیغام مربوطه از
ابتداي صف مي شود.
Component:
یک موتلفه از تعدادی 1301266 تشکیل شده است که به صورت همزمان اجرا می شوند و با یکدیگر
ن ربك هاى ديك غیر حاضس در آن ملفه تعامل دارند.
موجود در یک ملفه ریک های داخلی و ریک های دیگر ریک های خارجی نامیده می
نين با توجه به فرستتده آنها به دو دسته داخلى و خارجى تقسيم مى شوند.
صفحه 7:
Verification of Reactive Systems
نگاه كلي به زبان 166602 REBECA
در مدل سازي يك مؤلفه. بيغامهاي خارجي محيط مؤلفه را شبيه سازي مي كنند. از
آنجابي كه محيط قابل بيش بيذ
شوند.
بيغامهاي داخلي در صندوق يستي مؤلفه مقصد كه مانند صف عمل مي كند. قرار مي
كيرند و توسط ربك مورد نظر سرويس داده مي شوند.
اجراي روالها به طور موازي با يكديكر و هر يك با يك رسمان اجرائي. ادامه مي يابد.
اين اجرا شامل برداشت بيغام از ابتداي صف و فراخواني روال متناظر آن است. هر
كاه ربك داراي پیغام منتظر در صف نباشد. در حالت بیکار باقي مي ماند.
صفحه 8:
Verification of Reactive Systems
نگاه كلي به زبان 166602 REBECA
Known Rebec:
هر ربك داراي فهرستي از ربك هاي آشنا است که فرستاده پیغام تنها به آنها امکان
دارد.متد
هاي ربك هاي آشنا که امکان صدا کردن آنها وجود دارد نیز مشخص می باشد.
1(
هر ربك داراي يك روال براي تنظیم مقادیر اولیه است. به هنگام شروع کار سیستم.
اين روال ها به صورت ضمني فراخواني مي شوند.
يابي کدهاي نوشته شده به زبان ربکا بك ابزار خودکار تولید شده است که
دن کد ربکا؛ بررسي نحو آن و آزمون مدل را در اختیار کاربر قرار مي
صفحه 9:
Verification of Reactive Systems
REBECA wl روشهاي درستي
خصوصیات مورد نظر آن به صورت توصیف ) نوشت.
بررسي و اثبات برآروده شدن خواص دلخواه توسط مدل. وظیفه تحلیل صوري است.
روش تحلیل مي تواند به دو صورت الگوريتميك ( وارسي الگو- 6۳6166 1۷]0061) و یا
استنتاجي باشد.
در وارسي الگو يك شبیه سازي کامل از مدل روي تمام حالتهاي ممکن انجام مي شود. این
اید به وسیله يك ابزار نرمافزاري انجام گیرد.
صفحه 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
علت رویکرد به درستي يابي تركيبي :
براي درستي بابي صوري سیستم هاي واقعي مشكلاتي وجود دارد.
در درستي يابي سیستم هاي بزرگ, قضیه هايي که بايستي اثبات شوند معمولا
در حدتوان خبرگان نیستند.
model cheking ,» هم هنگامي که سیستم ا گي بالايي
برخوردار باشد دچار مسئله ي قابل پیش بيني انفجار حالت مي شویم.
درستي يابي تركيبي براي جلو كيري از انفجار حالت و در نتيجه ايجاد امکان
زيه مدل به مؤلفه هاي تشكيل دهنده. درستي
اج خواص كل سيستم از خواص اجزاي تشكيل
اده مي شود. كه براي انجام آن راههاي كوناكوني وجود دارد.
صفحه 13:
Verification of Reactive Systems
درستي يابي تركيبي REBECA
براي انجام درستي يابي تركيبي در ساده ترین شکل سیستم را مرکب از دو پیمانه
۲و 0 در نظر مي گیریم که با محبط خود در ار تباط هستند.
> 0 م لو
"it «
این سیستم را با 0 || نمایش مي دهیم.
اگر توصیف خصوصیات ,40 را براي و و40 را براي ۵) داشته باشیم. مسئله درستي
بابي تركيبي. در حالت كلي به صورت قاعده ز خلاصه مي ذ
اینجا بايستي در نظر گرفت, نحوه تاثير كذاري رم ۲۲
یکدیگر است و همچنین خصوصیات ,0), اس ORG
ترکیب و ۵ تايستي به گونه اي باشد ۳ * | م جیهم بر
ل
صفحه 14:
Verification of Reactive Systems
REBECA تانق فرگتی asa
این است که
نکته اي که بيستي در اینجابه آن شاره
معمولا در درستي يابي تركيبي خواص ايمني مورد توجه قرار مي گيرند.
دلیل :
استدلال در مورد خواص پیشرفت در درستي يلبي تركيبي کار دشواري است. در اين
روش اگر خاصيتي که براي پیمانه ۳ بیان مي شود. در مورد تمامي دنباله هاي
محاسباتي ممکن ایجاد شده در اثر اجراي ۳ برقرار باشد ( خاصیت از نوع خواص ایم:
باشد) و 0۵ روي داده هاي تحت کنترل ظ تاثیر نگذارد. ترکیب P و © مي تواند
حداكثر توليد برخي از اين دنبلله هاي را غير ممكن سازد. اما بخشي از دنبلله ها كه
مانند خواص هميشكي ١ را حفظ خواهند كرد. اما اكر خواص مورد بررسي در
دنبلله ها برقرار باشند. نمي توان تضمين نمود كه در اثر اجراي تركيبي. اين
صفحه 15:
Verification of Reactive Systems
REBECA Ss pula ans
يكي از روشهايي که در درستي يابي تركيبي مورد استفاده قرار مي گیرد. کمینه سازي
تركيبي است.در روش کمینه سازي تركيبي يك نسخه کاهش يافته " ۵ از ۵ مشتق مي
شود که تنها رفتاري از 0 را مشخص مي کند که براي 8 قابل مشاهده است.
1 > +o و
2 >
و سم {
ن ساختن آن دسته از ارتباطات 0 که براي قابل مشاهده 2 1 0< 90
توانیم 0 pet aes pee ng
دارد. که براي اثبات خواص سیستم از قواعد رو برو pee
۸ 70
م در قاعده فوق کاهش الفباي 2 به الفباي ,۵ ۲۲|
هاي غير مشترك از فضاي حالت * ۵ است.
صفحه 16:
Verification of Reactive Systems
REBECA درستي يابي تركيبي
Rebeca
در ربکا بدون هیچ شرطي روي اشیاء واكنشي, مي توان درستي يابي تركيبي انجام داد و
این سسفله از فقاط قوث ربكا است«عدم تاثير اشياء:بر داده هاى مشترك سبب«مى شود كه
درستي يابي تركيبي بدون قيد و شرط بر روي آنها قابل اعمال باشد.
در ربكا براي انجام درستي يابي تركيبي مي توان مدل بسته سيستم را به دو قسمت
مؤلفه و محيط تجزيه كرد.
با انجام اين تجزيه. مشخص مي شود كه حالت و رفتار Rebec) te REDEC plas
هاي داخلي مؤلفه) بايستي به طور کامل مدل شود و کدام 116166 ها Rebec)
هاي محيط) به طور مجرد یا کمینه مدل گردند. در مورد ی و تنها
فرستادن پیفام به 161086 هاي داخلي مولفه از رفتار آن مدل مي گردد. مولفه
اور کیب با محیط خود. دوباره مدلي بسته را بوجود مي ۳ كه به آن مدل مؤلفه
صفحه 17:
Verification of Reactive Systems
درستي يابي تركيبي 1۵060۵ REBECA
در درستي يابي تركيبي ربکا کارهاي زیر قابل
انجام است:
مدلسازي محیط
تجرید محیط
تجرید صف از پيغامهاي خارجي
تجرید پارامترها؛ تغییر پوياي پيكربندي ایجاد پوياي ربك ها
تجزیه مدل و ترکیب مولفه ها
اثبات نظریه درستي يابي ربکا
با استة
اده از ژ چند تعریف و قضیه نظريه درستي يابي ربكا بات شده است كه در مرجع
يعني پایان نامه دکترا خانم دکتر سيرجاني تحت عنوان توصيف و درستي يابي
هاي همروند و واكنشي ذکر شده است که از ذکر آن صرف نظر شده
صفحه 18:
Verification of Reactive Systems
سیستم کنترل کننده خط آهن REBECA
سیستم کنترل کننده خط آهن با استفاده از ربکا نوشته شده است. این مثال به صورتهاي مختلف در
متون مربوط به درستي يابي سیستم هاي واكنشي مورد بحث قرار گرفته است و مي تواند نمونه خوبي
براي نمایش و توضیح روش درستي يابي و همچنین مقایسه و ارزيابي مدل پيشنهادي و شیوه درستي
يابي آن نسبت به شیوه هاي دیگر باشد.
در تعریف این مسئله در قسمتی از مسیر راه آهن دوطرفه. يك پل وجود دارد که در آن واحد فقط يك
قطار مي تواند از روي آن بگذرد. در دو طرف این پل. چراغ هايي وجود دارد که فقط به يكي از قطارهايي
كه از دو طرف به پل مي رسند اجازه عبور مي دهد.
هر قطار تنها در صورتي مي تواند از روي اين يل عبور کند که چراغ مربوط به ورود به پل از آن سمت
سبز باشد. اگر چراغ مربوط قرمز باشد. قطار باید تا سبز شدن آن صبر کند.
صفحه 19:
Verification of Reactive Systemda> سیستم کنترل كننده
REBECA
خصوصيات مطلوب در اين مسئله :
شرط ايصفي :هيج كاه نبايد دو قطار هم زمان اجازه عبور از روي پل را به دست
sags
شرط پیشرفت :درعین حال همه قطارها كه از دو طرف به سمت يل مى
آيند بايد در نهايت بتوانند اجازه عبور از روي يل را بدست اورند
G \{ traint.OnTheBridge & train2.OnTheBridge)
GF( train1.OnTheBridge | train2.OnTheBridge)
صفحه 20:
Verification of Reactive Systems ~
هن
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 Systems ~
سیم کنعرال کتنده:خط آهن 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 Systems ~
سیستم کنترل کننده خط آهن REBECA
مدل بسته سیستم
اين سيستم شامل دو كلاس يا رده می باشد:
يك رده كنترل كننده يل (001361:011©10) ©8131060) است كه از تصادف دو قطار جلو
كيري كرده و امنيت يل را تامين ميكند.
يك رده براي تعریف قطارها (Train)
هر قطار روي خط آهن در حال حرکت است تا هنگامي که ReachBridge ply )3
بافر برداشته شده و کارگزار مربوط به آن اجرا شود. در اینجا قسمتی از محاسبه ( حرکت
قطار روي خط آهن قبل از رسيدن به پل) به وسیله ناهمگامي پیامها مدل شده است. پس از
اجراي کارگزار اين پیام قطار به پل رسیده است و رسیدن خود را با پیام ۸1116 به
کنترل کننده اطلاع مي دهد. در اين هنگام چون پيامي در بافر قطار وجود ندارد به حالت
اقي مي ماند. ۱
ننده پس از دریافت پیام 28۳71۷6 وضعیت چراغ سوي دیگر پل را بررسي مي
قرمز بودن» چراغ مربوط به این قسمت را به سبز تغییر داده و با پیام
0 به درخواست کننده اجازه عبور مي دهد. در غیر اینصورت يك متغییر
23 را براي این قطار تنظیم میکند تا وضعیت قطار به عنوان
لبور ثبت شود.
صفحه 23:
Verification of Reactive Systems ~
یستم کنترل کننده خط آهن REBECA
مدل بسته سیستم
با در یافت پیام ۷01711۵37۳255 قطار منتظر از روي پل عبور مي کند وپس از عبور
Passed ol, را به خود مي فرستند. در اين جا نیز زمان عبور از روي يل به وسيله
ناهمكامي بيامهاء با زمان طي شده براي فراخواني کارگزار مربوط به پیام 328560 مدل
شده است. ۱
کارگزار پیام 325560 ترك پل را به کنترل کننده اعلام میکند و كنترل كننده هنكام
سرویس دادن به پیام ترك پل وجود قطار منتظر در سوي دیگر پل را بررسي مي کند تا در
صورت انتظار» اجازه عبور از پل را برایش صادر نماید.
در حال اجراي این مدل متشکل از تعریف در ربك از رده 112112 و يك کنترل
است که اجراي همروند انهاء اجراي سیستم را مدل مي کند.
صفحه 24:
3 ل کننده خط 7 ۷2:9 ويد ie
Train t2; Af (ieWaitinga) {
boolean isviaiting2;
boolean signal; 1
boolean sigaal2; ]مه
} Signal? - false; /* ved 7
egery initial { ie Uswaieingt) {
Signall = false; /* red */ signal = truer
Signal? = false; /* ved */ EL, YoutlayPase ()
Jotaivingl = faloer iniiaiting! = fale;
Ietiait ing? = false? 1
0 1
egery Arrive) { 1
TE (oondor == C1) { 1
LE [eignal2 -- false) {
eignall - fms; /* green ۸
)مرو
امه
ieviaitingl = crue:
1
1
else:
1 A
signal? - true; /+ green ۸
+2 YowlayPass (1
elee{
فوصت نطو = crue;
1
1
1 =
صفحه 25:
تزل كننده خط آ مدموا و ine
8 بسته سيستم
reactiveclasa Train(3) {
Knownobjecte [
BridgeCont roller controller;
| مد
۱
1
] (الممشغخصة مددومم
هدع - مجه نموه
self. Passed()
۱
magerv YouMayPaes() [
‘onTheBridge ~ trus;
self. Paseed() +
١
Passed() { موه
onTheBridge = false;
controller -Leave (}
pelE.ReachBridge ():
1
ReachBriags () { دوعق
cont voller .Aeriva() ;
1
2
heey A
Teas teaina (tnacont router! ور
Train train2 (theController) : 0):
BridgeController theController(traint,
(قصتوی ۰
1
صفحه 26:
Verification of Reactive Systems ~
REBECA سیستم کنترل کننده خط آهن
در مدل مؤلفه اين سيستم مدل به دو ملفه هرکدام شامل OBridgeControl os,
و 113112() تقسيم شده است. در اين مدل متغير هاي حالت ربك 1133122 از مدل
حذف شده اند. اين مدل شامل رده خارجي ۳211 261() است. این رده مرتباً پينامهاي
۶6 و 1,886( را به کنترل کننده ارسال مي کند.
یات ايمني و پیشرفت براي مدل مولفه ارائه شده به صورت زیر ا
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