اسلاید دوم

اسلاید دوم:

شرط لازم برای روش بررسی مدل ارائه یک مدل از سیستم است. 

• ابتدا سیستم های گذار را معرفی می کنیم، که یک کلاس استاندارد از مدل ها برای ارائه سیستم های سخت افزاری و نرم افزاری است. 
• جنبه های مختلف مدلسازی سیستم های همگام را توضیح می دهیم.
• در انتها در مورد مسأله انفجار فضای حالت در بررسی مدل توضیح می دهیم. 

سیستم های گذار

• سیستم های گذار (TSs) رفتار سیستم را مدل می کنند. 
• TSs گراف های جهت داری هستند که گره ها و یالها به ترتیب نمایانگر حالت ها و گذارها هستند. 
• یک حالت سیستم اطلاعاتی راجع به سیستم در یک لحظه خاص از رفتار آن را توصیف می کند:
• رنگ فعلی چراغ راهنمایی
• مقادیر فعلی تمام متغیرهای برنامه + شمارنده برنامه
• مقادیر فعلی رجیسترها با مقادیر بیت های ورودی
• گذارها مشخص می کند که چگونه یک سیستم از یک حالت به حالت دیگر انتقال پیدا می کند. 
• سوییچ از یک رنگ به رنگ دیگر (برای چراغ راهنمایی)
• اجرای یک دستور برنامه
• تغییر رجیسترها و بیت های خروجی برای یک ورودی جدید
• در ادامه ما به صورت فرمال یک سیستم گذار را تعریف می کنیم.

• یک سیستم گذار TS یک چندتایی (S,Act,→,I,AP,L)  است. 
• S مجوعه ای از حالت هاست. 
• Act مجموعه ای از عمل هاست. 
• →⊆ S×Act×S یک رابطه ی گذار است. 
•  I⊆ S مجموعه ای از حالات اولیه است. 
• AP مجموعه ای از گزاره های اتمی است.
• و 􀂄 L: S → 2^AP یک تابع برچسب گذاری است.
• TS محدود است اگر S, Act و AP محدود باشند.