ارائه راه حلی تخمینی برای مقابله با انفجار فضای حالت در وارسی سیستم های تبدیل گراف

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

Keywords:

الگوریتم ژنتیک , انفجار فضای حالت , سیستم های تبدیل گراف , وارسی مدل