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

Reactive Systems Verification

شماره درس: ۴۰۶۶۵ تعداد واحد: ۳
مقطع: کارشناسی ارشد نوع درس: نظری
پیش‌نیاز: – هم‌نیاز: –

اهداف درس

سیستم‌های واکنشی (reactive) سیستم‌هایی هستند که رفتار آن‌ها به گونه‌ای پیوسته و تنگاتنگ در ارتباط با محیط تعریف می‌شود. این گونه سیستم‌ها معمولاً در کاربردهای حساس به کار می‌آیند. نمونه‌هایی از این کاربردها عبارتند از: سیستم‌های عامل، شبکه‌های کامپیوتری سریع، سیستم‌های همراه بی‌سیم، سیستم‌های رایافیزیکی (CPS)، اینترنت اشیاء (IoT)، هوانوردی، سیستم‌های کنترل صنعتی، نیروگاه‌های اتمی و غیره. از خواص مهم این سیستم‌ها، همروندی (concurrency)، جنبه‌های بی‌درنگ (real-time)، و کارایی (performance)، اتکاپذیری (dependability) و امنیت بالا است. سه خاصیت اخیر معمولاً مستلزم درستی رفتار این گونه سیستم‌ها در شرایط مختلف است. از سویی دیگر، تعیین چنین درستی رفتاری به دلیل جنبه‌های همروندی و بی‌درنگی معمولاً بسیار پیچیده است. این درس درباره مفاهیم و روش‌های رسمی‌ای (formal methods) است که برای توصیف مشخصات (specification) و اعتبارسنجی (validation) سیستم‌های واکنشی به کار می‌آیند.

ریز مواد

  1. درستی‌یابی سیستم (۱ جلسه)
    • وارسی الگو، مشخصات وارسی الگو، نقاط قوت و ضعف.
  2. مدل‌های همروندی (۳ جلسه)
    • سیستم‌های گذار، مدل‌های متنی مبتنی بر متغیرهای مشترک، مسائل معنایی، روابط هم‌ارزی بین دستورات، مدل‌های متنی مبتنی بر ارسال پیام، مدل CSP، مدل CCS، شبکه‌های پتری، هم‌ارزی رفتاری، توازی همگام، NanoPromela، توازی همگام، مساله انفجار فضای حالت، تبعات ملزومات عدالت، عدالت ضعیف، عدالت قوی، دستورات هماهنگ‌سازی، دستورات ارتباطی، جنبه‌های معنایی عدالت، عدالت در شبکه‌های پتری، عدالت در سیستم‌های گذار.
  3. خواص زمان خطی (۴ جلسه)
    • بن بست، رفتار زمان خطی، خواص و تغییر ناپذیرهای ایمنی، خواص زندگی، انصاف.
  4. خواص منظم (۴ جلسه)
    • خودکارها در روی کلمات متناهی، وارسی الگوی خواص ایمنی منظم، خودکارها در روی کلمات نامتناهی، وارسی الگوی خواص ω منظم.
  5. منطق زمانی خطی (۶ جلسه)
    • نحو و معنا، هم‌ارزی فورمول‌های LTL، وارسی الگوی مبتنی بر خودکارهای LTL.
  6. منطق درخت محاسباتی (۶ جلسه)
    • نحو و معنا، قابلیت توصیف CTL نسبت به LTL، وارسی الگوی CTL، انصاف در CTL، وارسی الگوی نمادین CTL، CTL*.
  7. هم‌ارزی و تجرید (۳ جلسه)
    • شبیه‌سازی دوسویه، شبیه‌سازی دوسویه و هم‌ارزی CTL*، الگوریتم‌های پیمانه سازی شبیه‌سازی دو سویه، روابط شبیه‌سازی، شبیه‌سازی دوسویه و هم ارزی CTL* ∀
  8. کاهش ترتیب جزئی (۱ جلسه)
    • استقلال اعمال، رهیافت مجموعه‌ی زمان خطی Ample، رهیافت مجموعه‌ی زمان شاخه‌ای Ample.
  9. خودکارهای زمانی (۱ جلسه)
    • معنا، منطق درخت محاسباتی زمانی، وارسی الگوی TCTL.
  10. سیستم‌های احتمالی (۱ جلسه)
    • زنجیره‌های مارکوف، منطق درخت محاسباتی احتمالی، خواص زمان خطی، PCTL* و شبیه‌سازی دوسویه احتمالی، زنجیره‌های مارکوف و هزینه‌ها، فرایند‌های تصمیم‌گیری مارکوف.

ارزیابی

مراجع

  1. C. Baier and J.P. Katoen. Principles of Model Checking. MIT Press, 2008.
  2. E. Clarke, O. Grumberg, and D.A. Peled. Model Checking. 2nd edition, MIT Press, 2018.
  3. M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. 2nd edition. Cambridge University Press, 2004.
  4. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
  5. C. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
  6. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.