وارسی ویژگی دسترس پذیری در سیستم های تبدیل گراف با رویکرد کشف وابستگی شرطی بین قوانین

وارسی مدل [1] یکی از موثرترین تکنیک های صحت سنجی خودکار ویژگی های سیستم های سخت افزاری و نرم افزاری است. در حالت کلی، در این روش، مدلی از سیستم موردنظر تولید می شود و تمام حالات ممکن در گراف فضای حالت مورد کاوش قرار می گیرد تا بتواند خطاها و الگوهای نامطلوب را پیدا کند. در سیستم های بزرگ و پیچیده تولید تمام فضای حالت منجر به مشکل انفجار فضای حالت[2] می شود. تحقیقات اخیر نشان می دهند که کاوش در فضای حالت با استفاده از روش های هوشمندانه، می تواند ایده امیدوارکننده ای باشد. ازاین رو در این تحقیق ابتدا مدلی از سیستم موردنظر ایجاد می شود، سپس بخشی از فضای حالت مدل، تولیدشده و با استفاده از احتمالات شرطی، وابستگی بین قوانین موجود در فضای حالت کشف می شوند. پس از آن، با کمک وابستگی های کشف شده، بقیه فضای حالت مدل را به طور هوشمندانه مورد کاوش قرار می گیرد. در این مقاله روشی برای وارسی ویژگی دسترس پذیری [3] در سیستم های نرم افزاری پیچیده و بزرگ که به زبان رسمی تبدیل گراف [4] (GTS) مدل شده اند، ارایه می شود. روش پیشنهادی در GROOVE که یک مجموعه ابزار منبع باز برای طراحی و بررسی وارسی مدل سیستم های تبدیل گراف می باشد، پیاده سازی شده است. نتایج آزمایش های تجربی نشان می دهند که رویکرد پیشنهادی نسبت به روش های قبلی سریع تر بوده و مثال های نقض [5]/شاهد [6]کوتاه تری تولید می کند.