توصیف و وارسی نرم افزار های زمانی با ماشین حالت و منطق زمانی

راستیآزمایی نرمافزارهای زمانواقعی با دو مسئله مواجه است: ( 1) چگونه قوانین راستیآزمایی تولید کنیم و ( 2) چگونه آنها را برای راستیآزمایی توصیف مسئله به کار ببریم. ما در این مقاله روشی را ارائه میدهیم تا به وسیله آن به حل این دو مسئله برای سیستمهایی که با ماشین حالت زماندار توصیف میشوند، بپردازیم. در قدم اول، گزارههای منطقی زمان واقعی را از توصیف مسئله به دست میآوریم. در قدم دوم، قیود ایمنی را از گراف حالات ماشین حالت زماندار توصیف مسئله به دست میآوریم و در قدم سوم این قیود را به گزارههای منطقی زمان واقعی تبدیل میکنیم. این گزارهها که قیود ایمنی را نشان میدهند برای راستیآزمایی گزارههای حاصل از توصیف که در قدم اول به دست آمدهاند، به کار گرفته میشوند. برای نشاندادن عملیبودن روشمان، مسئله سیستم زمانواقعی تقاطع جاده و راهآهن را مطرح میکنیم و روشمان را برای آن به کار میبریم

کلیدواژه ها:

راستی آزمایی ، ماشین زماندار ، منطق زمان واقعی ، گراف حالات