چهارچوبی برای تشخیص خاتمه پذیری قوانین فعال با استفاده از وارسی مدل مبتنی بر BDD و SAT

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

کلیدواژه ها:

قوانین فعال ، پایگاه داده فعال ، خاتمه پذیری ، وارسی مدل