برنامههای واکنشی کـه وظیفـه کنتـرل محـیط یـا دسـتگاه پیرامون خود را به عهده دارند، در زمره برنامه های حساس به ایمنـی قرار دارند به این معنی که احتمال خطا در آنها باید بسیار پایین باشد تا قابل اعتماد باشند. رویکردهای آزمون ایستا و پویا که از شیوههـای رایج برای اجتناب یـا کـشف خطـا در نـرمافـزار اسـت، در آزمـون برنامه های حساس به ایمنی با موانعی مواجـه هـستند. یـک راه حـل برای مقابله با این موانع، پایش و وارسی حین اجرای برنامه است. از طرف دیگر پاسخ برنامه واکنشی به محیط، باید متناسـب بـا سـرعت مورد نیاز محیط باشد به این معنی که پس از صدور محرک یا تقاضـا از طرف محیط، برنامـه واکنـشی فقـط فرصـت دارد قبـل از صـدور
محرک یا تقاضای بعدی پاسخ بدهد. در این مقاله، ابتدا یک مـدل دو لایه برای پایش و وارسـی حـین اجـرای سیـستم واکنـشی پیـشنهاد میکنیم، سپس برای نشاندادن عملیبودن آن، دو ویژگی از نیازهای پروتکل ارتباطی CBCASTرا به صورت دنباله اظهارات منطـقهـای زمانی FILو بیان کرده و در نهایـت اتوماتـای حاصـل از آن را میسازیم
