وارسي ويژگي دسترس‌پذيري در سامانه هاي تبديل گراف با رويكرد كشف وابستگي‌ شرطي بين قوانين

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