با گسترش پیچیدگی سیستمهای نرمافزاری و افزایش نیاز به روشهای دقیق برای تحلیل، طراحی و اطمینان از صحت عملکرد آنها، استفاده از رویکردهای رسمی در مدلسازی رفتاری سیستمها اهمیت روزافزونی یافته است. یکی از رویکردهای برجسته در این زمینه، سیستمهای تبدیل گراف است که به دلیل ماهیت شهودی، بصری و فرمال خود، امکان مدلسازی دقیق تغییرات ساختاری و رفتاری سیستمهای پیچیده را فراهم میآورد. با وجود مزایای متعدد سیستم تبدیل گراف، یکی از موانع اصلی در استفاده عملی از آن، چالش تعریف بهینهی قوانین تبدیل گراف است. وجود قوانین زائد، ناسازگار یا فاقد شرط کافی میتواند منجر به تولید فضای حالت بسیار بزرگ (پدیدهی انفجار فضای حالت) شده و در نهایت باعث کندی یا توقف ابزارهای وارسی مدل شود. چنین مشکلی در کاربردهای واقعی، محدودیت جدی برای استفاده از سیستم تبدیل گراف ایجاد میکند. رساله حاضر با هدف حل این چالش، چارچوبی هوشمند و خودکار برای پالایش و بهینهسازی قوانین تبدیل گراف ارائه میدهد. این چارچوب مبتنی بر الگوریتم ژنتیک طراحی شده و در بستر ابزار رسمی GROOVE پیادهسازی گردیده است. در این رویکرد، هر کروموزوم نمایانگر یک زیرمجموعه از قوانین سیستم تبدیل گراف است و با استفاده از تابع برازندگی، که همزمان دو هدف کاهش فضای حالت و حفظ ویژگیهای رفتاری سیستم را دنبال میکند، مجموعهای بهینه از قوانین انتخاب میشود. از دیگر جنبههای نوآورانه این پژوهش، تحلیل ساختاری روابط میان قوانین از طریق گراف وابستگی است که با شناسایی همپوشانیها، تکرارها و ناسازگاریها در مجموعه قوانین، به پالایش مؤثر آنها کمک میکند. بهمنظور ارزیابی عملی چارچوب پیشنهادی، مجموعهای از مسائل کلاسیک و شناختهشده از جمله «مسئله خرید»، «مسئله فیلسوفان گرسنه» و «خوانندگان و نویسندگان» مورد تحلیل قرار گرفتهاند. نتایج حاصل از این آزمایشها نشان میدهد که فضای حالت مدلها بهطور چشمگیری کاهش یافته و در عین حال، دقت تحلیل رفتاری سیستم حفظ گردیده است. همچنین، مقایسه تجربی روش پیشنهادی با سایر روشهای موجود، از جمله روشهای مبتنی بر جستجوی کامل و الگوریتمهای فرااکتشافی دیگر، حاکی از برتری آن در کاهش زمان اجرا، مصرف حافظه و افزایش مقیاسپذیری است. این دستاوردها نشان میدهد که روش ارائهشده میتواند نقش مهمی در توسعه ابزارهای وارسی مدل و تحلیل سیستمهای پیچیده نرمافزاری ایفا کند.
