Runtime enforcement of regular timed properties by suppressing and delaying events

پیاده سازی زمان اجرا یک روش تایید / اعتبار سنجی است که با هدف اصلاح اعداد احتمالی نادرست یک سیستم مورد علاقه است. در این مقاله، ما در نظر سنجی پیاده سازی برای سیستم هایی که زمان فیزیکی بین اقدامات مهم است، در نظر گرفته شده است. اعدام ها به این ترتیب به صورت کلمات زمان بندی شده (به عنوان مثال، دنباله ای از اعمال با تاریخ) مدل می شوند. ما در نظر سنجی زمانبندی برای مشخصات زمان بندی شده به صورت اتوماتیک زمانبندی طراحی شده ایم. سازوکارهای اجرای ما توانایی هر دو را برای تأخیر در رویدادها برای محدود کردن زمان بندی محدودیت ها و سرکوب رویدادها دارند، در صورتی که هیچ تاخیری مناسب نیست، بنابراین احتمالا برای اعدام های طولانی تر امکان پذیر است. برای تضعیف طراحی و اثبات صحت آن، سازوکارهای اجرایی در سطوح مختلف شرح داده می شود: توابع اجرایی که رفتار ورودی-خروجی را با توجه به تغییرات کلمات زمان بندی شده مشخص می کند، محدودیت هایی که باید از طریق چنین توابع رضایت بخش باشند، نظارت های اجرایی که عملیات عملی را توصیف می کنند رفتار توابع اجرایی و الگوریتم های اجرایی اجرای پیاده سازی نظارت اجرائی را توصیف می کند. امکان سنجی اجرای نظارت بر خواص به موقع توسط نمونه سازی سنتز مانیتورهای اجرایی از اتوماتای ​​زمانبندی معتبر است.