ABS Kobra Ahmadi (Persion)

هدف از اين پايان­نامه، معرفي يك چهارچوب رياضي جهت استدلال در مورد خواص سيستم­هاي تحمل­پذير خطا مي­باشد. در همين راستا يك منطق عملي تكليف (DPL ) و يك اصل­گذاري براي آن معرفي مي­گردد. اين منطق خواص مفيدي مثل سلامت، تماميت، فشردگي و تصميم­پذيري دارد. اگر چه منطق معرفي شده، ارزشمند و مهم است ولي از آنجا كه منطق­هاي زماني در مشخص كردن سيستم­هاي محاسبه نقش مهمي دارند، اين منطق توسط عملگر­هاي زماني (CTL) توسيع داده مي­شود.   در سيستم­هاي تحمل­پذير خطا، بعد از يك نقض بايد اعمالي اجرا شود تا آن نقض را جبران كند كه در منطق تكليف استدلال   CTD ناميده مي­شود. رويكرد ما در اين پايان­نامه براي مواجهه با چنين جملاتي، استفاده از چندين نسخه­ي مجوز مي­باشد كه به اين ترتيب توسيع سودمند ديگري از DPL حاصل مي­شود. در اين پايان­نامه همچنين با طرح سناريوهايي از ساختارهاي ارائه شده مانند شام فيلسوفان و سيستم قطار، چگونگي كاربرد آن­ها را براي مشخص كردن سيستم­هاي محاسبه در عمل نيز نشان مي­دهيم.

-