آموزش بررسی مدل منطق زمانی (Temporal Logic Model Checking) - آخرین آپدیت

ویژگی‌های زمان خطی Linear Time Properties

• بن‌بست (Deadlock) Deadlock

• رفتار زمان خطی Linear Time Behavior

• ویژگی‌های زمان خطی Linear Time Properties

• مفاهیم پایه ویژگی‌های ناوردا Basic Concepts of Invariant Properties

• الگوریتم‌های بررسی ویژگی‌های ناوردا Algorithms for Checking Invariant Properties

• ویژگی‌های ایمنی (Safety Properties) Safety Properties

• برابری اثر و ویژگی‌های ایمنی Trace Equivalence and Safety Properties

• ویژگی‌های زنده بودن (Liveness Properties) Liveness Properties

• مثال بررسی ویژگی‌های زنده بودن Checking Liveness Properties - Illustration

• مقایسه ایمنی در برابر زنده بودن Safety Vs Liveness

• مفاهیم انصاف (Fairness) Concepts of Fairness

• محدودیت‌های انصاف Fairness Constraints

• ارضای منصفانه ویژگی‌های LT Fair Satisfaction of LT Properties

منطق زمان خطی Linear Time Logic

• منطق زمان خطی (LTL): نحو Linear Time Logic (LTL): Syntax

• معناشناسی LTL Semantics of LTL

• ارضای LTL در سیستم‌های انتقال Satisfaction of LTL on Transition Systems

• معناشناسی نقیض Semantics of Negation

• برابری فرمول‌های LTL Equivalence of LTL Formulas

• فرم نرمال مثبت Positive Normal Form

• انصاف در LTL Fairness in LTL

• نمای کلی بررسی مدل LTL Overview of LTL Model Checking

• اتوماتای بوچی غیرقطعی (NBA) Non-Deterministic Buchi Automata (NBA)

• اتوماتای بوچی تعمیم‌یافته (GNBA) Generalize NBA (GNBA)​

• تبدیل GNBA به NBA GNBA to NBA

• مفاهیم بررسی پایداری Persistency Checking - Concepts

• مثال بررسی پایداری Persistency Checking - Example

• بستار و مجموعه‌های ابتدایی Closure & Elementary Sets

• ترجمه فرمول‌های LTL به NBA Translating LTL Formulas to NBA

• آموزش نرم‌افزار SPIN A Tutorial on SPIN

• نمای کلی Promela Overview of Promela

• ساختار فرآیند Process Structure

• دستورات Promela - بخش اول Promela Statements - Part 1

• دستورات Promela - بخش دوم Promela Statements - Part 2

• دستورات Promela - بخش سوم Promela Statements - Part 3

• معناشناسی عملیاتی - بخش اول Operational Semantics - Part 1

• معناشناسی عملیاتی - بخش دوم Operational Semantics - Part 2

• مدل‌های ارتباطی Communication Models

• نمای کلی بررسی‌کننده مدل SPIN Overview of SPIN Model Checker

• مشخصات ویژگی‌ها Property Specifications

منطق درخت محاسباتی Computation Tree Logic

• مقدمه‌ای بر منطق درخت محاسباتی (CTL) Introduction to Computation Tree Logic

• نحو CTL CTL Syntax

• معناشناسی CTL CTL Semantics

• برابری و فرم‌های نرمال CTL CTL Equivalence and Normal Forms

• قدرت بیان CTL در مقابل LTL Expressiveness of CTL Vs LTL

• مقدمه‌ای بر بررسی مدل CTL Introduction to CTL Model Checking

• محاسبه مجموعه‌های ارضا در فرمول‌های CTL - بخش اول Computing the Satisfaction Sets of CTL Formulas - Part 1

• محاسبه مجموعه‌های ارضا در فرمول‌های CTL - بخش دوم Computing the Satisfaction Sets of CTL Formulas - Part 2

• انصاف در CTL Fairness in CTL

• بررسی مدل CTL با در نظر گرفتن انصاف CTL Model Checking with Fairness

• مثال‌های نقض و شاهدها Counterexamples and Witnesses

• تولید مثال‌های نقض و شاهدها Generation of Counterexamples and Witnesses

• مثال‌های نقض و شاهدها با انصاف Counterexamples and Witnesses with Fairness

بررسی مدل نمادین CTL Symbolic CTL Model Checking

• مقدمه‌ای بر بررسی مدل نمادین CTL Introduction to Symbolic CTL Model Checking

• کدگذاری نمادین سیستم‌های انتقال Symbolic Encoding of Transition Systems

• مثالی از کدگذاری نمادین سیستم‌های انتقال Symbolic Encoding of Transition Systems - An Example

• ترکیب نمادین سیستم‌های انتقال Symbolic Composition of Transition Systems

• محاسبه تصویر نمادین Symbolic Image Computation

• محاسبه پیش‌تصویر نمادین Symbolic Preimage Computation

• محاسبه نمادین برای عملگرهای Until وجودی و Always وجودی Symbolic Computation for Existential Until and Existential Always Operators

• مثالی از بررسی مدل نمادین Symbolic Model Checking - An Example

• نمای کلی نمایش توابع سوئیچینگ Overview of Switching Function Representations

• ساخت OBDDهای کاهش‌یافته Constructing Reduced OBDDs

• ملاحظات ROBDDها Considerations of ROBDDs

• مسئله ترتیب متغیرها Variable Ordering Problem

• عملیات بولی در OBDDها Boolean Operations in OBDDs

• نمای کلی NuSMV NuSMV Overview

• مدل‌سازی در NuSMV Modeling in NuSMV

• کاربردهای NuSMV Uses of NuSMV