جابر کریم پور - دانشگاه تبریز
ساناز خبرت - دانشگاه آزاد اسلامی زنجان

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

توسعه مبتنی برمولفه خودکارتعامل مولفه تحلیل صوری، وارسی بررسی درستی زبانهای مبتنی برخودکارها، ابزار CoIn & DiVinE