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

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

آتاماتای زماندار، توصیف، حساب رخداد، وارسی