وارسي ويژگي دسترس‌پذيري در سامانه‌هاي نرم‌افزاري پيچيده و هم‌روند با استفاده از الگوريتم‌هاي جستجوي هوشمند

روش وارسي مدل، روشي رسمي و مؤثر جهت تأييد سامانه‌هاي نرم‌افزاري است كه با توليد و بررسي همه حالت هايِ ممكنِ مدلي از سامانه نرم‌افزار به تحليل آن مي ‌پردازد. در سامانه‌هاي ايمني - بحراني، نمي توان ريسك بروز خطا را حتي در فرآيند تست پذيرفت و لذا لازم است فرآيند درستي‌يابي، قبل از پياده‌ سازي و در سطح مدل انجام شود. استفاده از اين روش به‌منظور بررسي خواصي مانند ايمني ايجاب مي‌ كند كه تمام حالت‌ هاي قابل دسترس (تمام فضاي حالت) توليد و سپس فضاي حالت سامانه مورد نظر به‌صورت دقيق بررسي شوند. چالش اساسي روش وارسي مدل در سامانه‌هاي بزرگ و پيچيده كه داراي فضاي حالت گسترده و نامحدود هستند، مشكل انفجار فضاي حالت (كمبود حافظه در توليد همه حالت‌هاي ممكن) است. سامانه‌هاي تبديل گراف، از پركاربردترين سامانه‌هاي مدل‌سازي رسمي و راه‌كاري مناسب به‌منظور مدل‌ سازي و وارسي سامانه‌هاي پيچيده هستند. در سامانه‌هايي كه تأييد ويژگي ايمني غيرممكن است، مي ‌توان با جستجويِ يك حالت قابل دسترسي كه در آن پيكربندي خاصي (به‌عنوان مثال خطا يا رفتار نامطلوب) رخ مي ‌دهد، ويژگي ايمني را رد كرد. مطالعات اخير حاكي از آن است كه اكتشاف جزئي و هوشمندانه بخشي از فضاي حالت مي‌ تواند راه حل مناسبي براي مشكل انفجار فضاي حالت باشد. هدف اين پژوهش، استفاده از الگوريتم جنگل تصادفي در وارسي مدل است كه مي‌تواند با گزينش تعداد محدودي مسير اميدبخش مشكل انفجار فضاي حالت را برطرف سازد. مسيري اميدبخش است كه احتمال رسيدن به يك جواب از طريق اين مسير، بيشتر از بقيه مسيرها باشد. در روش پيشنهادي، ابتدا مدل كوچكي از سامانه با استفاده از زبان رسمي سامانه توصيف گراف (GTS) ايجاد، سپس، از فضاي حالت مدل كوچك، مجموعه‌ آموزشي از مسيرهايي كه به هدف مي‌رسند ايجاد مي‌شود. پس‌ازآن، مجموعه آموزشي توليدشده در اختيار الگوريتم جنگل تصادفي قرار داده مي‌شود تا روابط منطقي موجود در آن شناسايي و كشف شوند. در مرحله بعد از دانش به‌دست‌آمده جهت پيمايش هوشمند و غير كامل فضايِ حالتِ مدلِ بزرگ استفاده مي‌شود. رويكرد پيشنهادي براي تأييد ويژگي دسترس‌پذيري و رد ويژگي ايمني در سامانه‌هاي بزرگ و پيچيده كه ايجاد تمام فضاي حالت سامانه ناممكن است، استفاده مي‌ شود. به منظور ارزيابي رويكرد پيشنهادي، اين رويكرد در ابزار GROOVEكه از ابزار متن‌باز براي طراحي و وارسي مدل براي سامانه‌هاي تبديل گراف است، اجراشده است. نتايج نشان مي‌دهند كه روش پيشنهادي ازنظر ميانگين زمان اجرا و طول شاهد توليدشده نسبت به روش‌هاي مورد مقايسه عملكرد بهتري دارد.