درستی‌یابی سیستم‌ها

با درس «مدل‌سازی و درستی‌یابی صوری» جایگزین شد.

مقطع: تحصیلات تکمیلی گرایش: الگوریتم‌ها و محاسبات
نوع درس: نظری تعداد واحد: ۳
پیش‌نیاز: – هم‌نیاز: –

هدف کلی

هدف از این درس مروری بر روش‌های صوری توصیف سیستم‌ها و درستی‌یابی ویژگی‌های آن‌هاست. تاکید بر سیستم‌های واکنشی است و منظور از روش‌های توصیف روش‌هایی است که با هدف درستی‌یابی ارائه می‌شوند. از میان روش‌های درستی‌یابی تاکید اصلی بر روش وارسی الگوی (Model Checking) ویژگی‌های توصیف شده در منطق‌های زمانی (Temporal Logics) است.

سرفصل‌ها

  1. درستی‌یابی سیستم
  2. مدل‌های همروندی
  3. خواص زمان خطی
  4. خواص منظم
  5. منطق زمانی خطی
  6. منطق درخت محاسباتی
  7. هم‌ارزی و تجرید
  8. کاهش ترتیب جزئی
  9. خودکارهای زمانی
  10. سیستم‌های احتمالی

ارزیابی پیشنهادی

منابع پیشنهادی

  1. C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press, 2008.
  2. K. Schneider. Verification of Reactive Systems. Springer, 2004.
  3. E. Clarke, O. Grumberg, and D. A. Peled. Model Checking. 2nd Edition, MIT Press, 2018.
  4. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
  5. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.