تولید قوانین راستی آزمای سیستم‌های رخدادگرا با استفاده از حساب رخداد

وارسی مدل، ابزار کاربردی جهت اشکال‌زدایی خودکار سیستم‌های واکنشی پیچیده مانند کنترل کننده‌های جاسازی شده و پروتوکل‌های شبکه می‌باشد. در وارسی مدل، سطح بالایی از توصیفات سیستم با نیازمندی‌های درست منطقی مقایسه می‌شود تا ناسازگاری‌های آن کشف شود. تکنیک‌های سنتی (قدیمی) وارسی مدل جهت مدل سازی صریح زمان قابل پذیرش نمی‌باشند و برای استدلال سیستم‌های بلادرنگ مناسب نمی‌باشند بنابراین آتاماتای زماندار جهت توصیف رفتار سیتم‌های بلادرنگ معرفی شد از آنجایی که آتاماتای زماندار در زمره زبان‌های ویژوال جهت توصیف رفتار سیستم‌های بلادرنگ قرار دارد در این نوع زبان‌ها بعضی از قیود سیستم قابل توصیف نمی‌باشند برای توصیف این قیود مجبور به استفاده از زبان‌های متنی هستیم؛ما در این مقاله جهت توصیف قیودی که توسط آتاماتای زماندار قابل توصیف نیستند از حساب رخداد که در زمره زبان‌های متنی قرار دارد استفاده می‌کنیم و همچنین نحوی شبیه سازی آتاماتای زماندار به حساب رخداد را نشان می‌دهیم.

کلمات کلیدی: آتاماتای زماندار Timed Automata،توصیف رسمی، حساب رخداد Event Calculus، وارسی نرم‌افزار، نرم‌افزار حساس به ایمنی

دانلود مقاله