عین الله پیرا - استادیار، دانشکده فناوری اطلاعات و مهندسی کامپیوتر، دانشگاه شهید مدنی آذربایجان

تایید درستی سیستم های نرم افزاری، خصوصاً از نوع بحرانی-ایمنی، یکی از مراحل مهم و چالش برانگیز در طراحی چنین سیستم هایی است چرا که وجود یک خطا حتی از نوع خیلی کوچک می تواند صدمات جبران ناپذیری وارد کند. برای کاهش زمان و هزینه تولید چنین سیستم هایی، درستی آنها قبل از پیاده سازی و معمولاً روی مدلی از آن انجام میشود . وارسی مدل یک روش مبتنی بر ریاضیبرای تحلیل خودکار سیستم های نرم افزاری است که با پیمایش تمام حالت های ممکنِ مدل، درستی مدل را در تک تک این حالت ها بررسی می کند. در صورت پیچیده و بزرگ بودن یک مدل، وارسی مدل با مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالت های ممکن) مواجه می شود. در این مقاله، از الگوریتم جستجوی عمقی تکرارشونده A* ) IDA* ) استفاده کرده تا این مشکل را تا حدودی حل کنیم. روند این الگوریتم به این صورت است که ابتدا یک جستجوی او ل- عمق ( DFS) تا عمق یک انجام داده سپس مسیرهایی که هزینه آنها از یک مقدار آستانه بیشتر است را کنار گذاشته و جستجوی اول -عمق دیگری تا عمق دو انجام می دهد و این مراحل را تا موقعی ادامه می دهد که به حالت هدف برسد. برای ارزیابی کارایی الگوریتم IDA* ، آن را در ابزار GROOVE – از ابزارهای وارسی مدل مبتنی بر زبان تبدیل گراف - پیاده سازی کرده و نتایج آن را با نتایج الگوریتم A* مقایسه می کنیم

جستجوی عمقی تکرار شونده، سیستم های نرم افزاری بحرانی-ایمنی، وارسی مدل، تبدیل گراف