مدل‌سازی و درستی‌یابی صوری

Formal Modeling and Verification

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

هدف کلی

هدف این درس آشنایی دانشجویان با روش‌های توصیف صوری و وارسی مدل سیستم‌های همروند و واکنشی است. توصیف سیستم‌ها توسط زبان‌های مدل‌سازی سطح بالا انجام می‌شود که به نوبه خود به سیستم‌های گذار تبدیل می‌شوند. وارسی مدل مبتنی بر منطق‌های زمانی شناخته‌شده انجام می‌شود.

سرفصل‌ها

  1. مقدمه‌ای بر درستی‌یابی
  2. سیستم‌های گذار و گراف برنامه‌ها
  3. مدل‌سازی سطح بالا: پروملا، شبکه‌های پتری، و مدل اکتور
  4. خاصیت‌های خطی
  5. انصاف
  6. خاصیت‌های منظم
  7. منطق زمانی خطی
  8. منطق درخت محاسبه
  9. خودکاره‌های زمانی و هیبرید
  10. وارسی مدل احتمالاتی
  11. یادگیری مدل
  12. هم ارزی و تجرید (اختیاری؛ بنا به تشخیص استاد درس)
  13. کاهش ترتیب جزئی (اختیاری؛ بنا به تشخیص استاد درس)

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

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

  1. C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press, 2008.
  2. S. Kundu, S. Lerner, and R. Gupta. High-Level Verification: Methods and Tools for Verification of System-Level Designs. Springer-Verlag, 2014.
  3. M. Ben-Ari. Principles of the Spin Model Checker. Springer-Verlag, 2008.
  4. M. Huisman and A. Wijs. Concise Guide to Software Verification: From Model Checking to Annotation Checking. Springer International, 2023.
  5. E.M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith. Model Checking. MIT Press, 2018.
  6. C. Baier and J. P. Katoen. Principles of Model Checking. MIT Press, 2008.