عبدالرسول پیمانی - دانشگاه آزاد اسلامی واحد اراک، گروه کامپیوتر،اراک، ایران
رزا یوسفیان - آموزشکده فنی حرفه ای سما، دانشگاه آزاد اسلامی واحد خمینی شهر، اصفهان، ایران

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

وارسی مدل، سیستمهای تبدیل گراف، سیستمهای تبدیل گراف لایه ای