سید مرتضی بابامیر - استادیار گروه مهندسی دانشگاه کاشان
مهدی برهانی دهکردی - دانشجوی کارشناسی ارشد دانشگاه آزاد اسلامی واحد اراک
امیر اسماعیلی - دانشجوی کارشناسی ارشد دانشگاه آزاد اسلامی واحد اراک

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

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