آموزش مقدمه‌ای بر مدل‌سازی برای تأیید رسمی (Formal Verification) - آخرین آپدیت

مقدمه‌ای بر مدل‌چکینگ Introduction to Model Checking

• مثال‌های انگیزشی Motivating Examples

• باگ‌های مهم پیشین و اثرات آن‌ها High Profile Previous Bugs and Their Impacts

• مروری بر تأیید عملکردی Overview of Functional Verification

• تکنیک‌های تأیید عملکردی Techniques for Functional Verification

• مروری بر تأیید رسمی و مدل‌چکینگ Overview of Formal Verification and Model Checking

• عناصر مدل‌چکینگ Elements of Model Checking

• چالش مدل‌چکینگ: انفجار فضای حالت Challenge to Model Checking: State Space Explosion

مدل‌سازی Modeling

• منطق گزاره‌ای Propositional Logic

• منطق مرتبه اول (Predicate Logic) Predicate Logic

• نظریه مجموعه‌ها Set Theory

• سیستم‌های انتقال: تعاریف Transition Systems: Definitions

• سیستم‌های قطعی در مقابل غیرقطعی Deterministic vs Non-Deterministic Systems

• اجراها Executions

• مدل‌سازی مدارهای ترتیبی Modeling Sequential Circuits

• گراف‌های برنامه: تعاریف Program Graphs: Definitions

• گراف‌های برنامه: مثال‌ها Program Graphs: Examples

• از گراف‌های برنامه تا سیستم‌های انتقال From Program Graphs to Transition Systems

مدل‌سازی ترکیب سیستم Modeling System Composition

• همزمانی و درهم‌تنیدگی (Interleaving) Concurrency and Interleaving

• همزمانی و درهم‌تنیدگی: مثال‌ها Concurrency and Interleaving: Examples

• گراف‌های برنامه درهم‌تنیده Interleaving Program Graphs

• کنش‌های حیاتی و اتمیک بودن Critical Actions and Atomicity

• الگوریتم عدم تعارض پترسون Peterson's Mutual Exclusion Algorithm

• همگام‌سازی و دست‌دادن (Handshaking) Synchronization and Handshaking

• مثال: تقاطع خط آهن Example: Railroad Crossing

• حاصل‌ضرب همگام بخش اول Synchronous Product - Part 1

• حاصل‌ضرب همگام بخش دوم Synchronous Product - Part 2

• مسئله انفجار فضای حالت The State Space Explosion Problem