بخشی از مقاله
بکارگیری داده کاوی در تشخیص به نبست در سیستم های تبدیل گراف
چکیده
وارسی مدل یک روش خودکار و راهکاری مناسب برای بررسی درستی یک سیستم نرمافزاری میباشد. خطاها در سیستمهای نرمافزاری، بهعلت هزینهِ پایین تصحیح آنها در مراحل تحلیل و طراحی نسبت به هزینه تصحیح آنها در مراحل تست و نگهداشت، باید قبل از پیاده-سازی و در سطح مدل مشخص و رفع شوند. سیستمهای تبدیل گراف از پرکاربردترین سیستمهای مدلسازی رسمی و راهکاری مناسب به منظور مدلسازی و وارسی مدل میباشند . مشکل مهم وارسی مدل این است که در اکثر سیستمهای واقعی و پیچیده با مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالتهای ممکن) مواجه میشود، بنابراین باید دنبال روشهایی باشیم که فضای حالت سیستم را بطور هوشمندانه و غیرکامل پیمایش میکنند. یکی از این روشها، استفاده از روشهای فرامکاشفهای میباشد. در این پژوهش، یک روش فرامکاشفهای مبتنی بر دادهکاوی ارائه میکنیم. محدودیت روش ارائه شده ایناست که فقط برای سیستمی جواب میدهد که مدل-های ساخته شده از آن با اندازههای مختلف، برپایهکی سبکِ معماری باشدن. سبکِمعمارییک، نوع اَبَرمدل جهت تعیین مجموعهای از اجزاء و ارتباطات میان آنها برای مشخص کردن سیستم بر مبنای آن سبک میباشد. روش ارائه شده را در فرمالیسم "سیستم تبدیل گراف" و ابزار – GROOVE از ابزارهای مدلسازی سیستم تبدیل گراف - پیاده سازی میکنیم. مقایسه نتایج پیادهسازی این روش با نتایج روشهای قبلی، نشان میدهند که زمان اجرای روش پیشنهادی در این پژوهش، نسبت به روشهای قبلی، بطور چشمگیری بهبود یافته است.
واژههای کلیدی
دادهکاوی، سبک معماری، سیستم تبدیل گراف، وارسی مدل، انفجار فضای حالت
-1 مقدمه
یکی از اهداف مهمِ تایید سیستمهای نرم افزاری1، اطمینان از بدون خطا ساخته شدن سیستمهای نرم افزاری موردنظر میباشد، بخصوص سیستم-های بحرانی- امنیتی که حتی خطای کوچک نیز موجب خسارتهای زیاد مالی و جانی میشود. خطاها در سیستمهای نرمافزاری، باید قبل از پیاده-سازی و در سطح مدل مشخص و رفع شوند. یک روش معمول برای بررسی صحت مدل، استفاده از روشهای رسمی از جمله وارسی مدل2 می باشد. در این روش، سیستم موردنظر بههمراه ویژگی که باید در سیستم نرم افزاری برقرار باشد براساس تئوری ریاضی مدل شده و به وارسیکننده مدل3 تحویل داده میشوند، وارسیکننده مدل تشخیص میدهد که آیا
ویژگی موردنظر در سیستم وجود دارد یا خیر؟ بطور کلی، وارسیکننده مدل از روی مدل سیستم مورد نظر، کلیه حالاتی که سیستم میتواند در آن قرار گیرد را ساخته و ویژگی موردنظر را در تکتک حالات قابل حصول سیستم بررسی میکند. به کلیه این حالات، فضای حالت 4 سیستم گفته میشود که از وضعیتها و گذارهای میان وضعیتها تشکیل شده است.[1]
مشکل اصلی که عملیات وارسی مدل با آن روبرو میشود انفجار فضای حالت5 (کمبود حافظه در تولید همه حالتهای ممکن) میباشد. راهحل-های مختلفی از جمله، وارسی مدل نمادین [2]، کاهش ترتیب جزئی [3] ، تکنیک تقارن [4] ، وارسی سناریو محور [5] و روش های دیگر [6-7]برای حل این مشکل ارائه شده است. البته این روشها نیز فضای حالت را بطور کامل پیمایش میکنند و بنابراین از مشکل انفجار فضای حالت رنج
میبرند. بنابراین باید دنبال روشهایی باشیم که فضای حالت سیستم را بطور غیرکامل و هوشمندانه پیمایش میکنند. در این پژوهش، یک روش فرامکاشفهای با استفاده از تکنیک دادهکاوی6 ارائه میکنیم. در روش پیشنهادی ابتدا مدل با اندازه کوچکی از سیستم در صورت موجود، وارسی میشود به اینصورت که فضای حالت آن با استفاده از استراتژی "جستجوی اول سطح" بطور کامل پیمایش شده و حالت بنبست (حالتی که گذار خروجی ندارد) در آن تشخیص داده میشود، سپس با داشتن فضای حالت تولید شده و دانستن حالت بنبست و با توجه به اینکه حالت ابتدایی مشخص است، تمام مسیرها که از حالت ابتدایی شروع میشوند و به حالت بنبست ختم میشوند را در نظر گرفته و تمام برچسب گذارها (که همان قوانین سیستم تبدیل گراف میباشند) در این مسیرها را بدون در نظر گرفتن خود حالتها استخراج میکنیم و با استفاده از تکنیکهای داده-کاوی، الگوهای تکراری در این مسیرها را پیدا میکنیم. برای تشخیص بن-بست در مدل با اندازه واقعی، از الگوهای تکراری بدست آمده استفاده کرده و فضای حالت آن را بطور هوشمندانه پیمایش میکنیم.
گرافها و نمودارها یک ابزار خیلی مفید و قابلفهم برای توصیف و مدلسازی سیستمهای نرمافزاری ارائه میکنند. سیستمهای تبدیل گراف7 (GTS) یک مبانی رسمی برای تبدیل گرافها و نمودارها به توصیف رسمی فراهم می کنند.[8] همچنین با این فرمالیسم میتوان رفتارهای پویای سیستم و چگونگی تغییرات آن را مدل کرد.
روش پیشنهادی در این پژوهش را در فرمالیسم GTS و ابزار GROOVE پیاده سازی میکنیم که این ابزار جهت تولید فضای حالت فرمالیسمهای GTS بکار میرود.[9] این روش برای سیستمی جواب می-دهد که مدلهای آن با اندازههای مختلف، برپایه یک سبکِ معماری باشند.
سبک معماری، یک نوع اَبَرمدل جهت تعیین مجموعهای از اجزاء و ارتباطات میان آنها برای مشخص نمودن سیستم بر مبنای آن سبک می-باشداین. اجزاء عموماً بهصورت مولفهها و اتصالدهندههای آنها میباشند که ارتباطات میان آنها بر اساس قیدها و محدودیتهایی است که مشخص میکند چگونه این مولفهها و اتصالدهندهها میتوانند باهم ترکیب شوند. در واقع، در این نوع سیستمها، گراف میزبان مستقل از قوانین تبدیل گراف هستند و گراف نوع و قوانین ثابت هستند. بعبارت دیگرمشترکاتِ، مدل با اندازههای مختلف از یک سیستم را بصورت استاندارد در میآورند که به آن سبک معماری گفته میشود .[10]
ادامه مطالب در این مقاله به صورت زیر سازماندهی شدهاند. در بخش 2، خلاصه ای از کارهای انجام شده در این زمینه را ارائه میکنیم. در بخش 3، پیشزمینه لازم، از جمله مطالبی درباره تکنیکهای دادهکاوی و فرمالیسم سیستم تبدیل گراف ارائه میکنیم. در بخش 4 به توضیح کامل روش ارائه شده میپردازیم. در بخش 5، روش پیشنهادی را روی چندین مساله شناخته شده اجرا کرده و نتایج حاصله را با نتایج اجرای روشهای
قبلی مقایسه میکنیم ونهایتاً، در بخش 6، نتیجهگیری و کارهای آینده را ذکر میکنیم.
-2 کارهای قبلی
برای رفع مشکل انفجار فضای حالت در وارسی مدل، راهحلهای کلاسیک از جمله روشهای مبتنی بر کاهش اندازه فضای حالت مدل ارائه شدهاند-[1 .9] از روش های مبتنی بر کاهش اندازه فضای حالت میتوان به موارد زیر اشاره کرد: وارسی مدل نمادین، کاهش ترتیب جزئی، تکنیک تقارن و وارسی سناریو محور. همچنین روشهای تجرید مدل هم وجود دارند که با کاهش اندازهی مدل به کاهش اندازهی فضای حالت میپردازند.[11-13]
در سالهای اخیر، از روشهای هوشمندانه به منظور مدیریت مشکل انفجار فضای حالتاستفاده شده است، از جملهِ الگوریتمهای ارائه شده؛ استفاده از الگوریتمهای ژنتیک [14,15] و پرندگان [16] برای پیدا کردن خطا (حالتهای بنبست) در سیستمهای تبدیل گراف، بکارگیری تکنیک دادهکاوی برای تحلیل اتوماتیک خطا [17-18] و بکارگیری الگوریتم کلونی
مورچهها در بررسی و کاوش فضای حالت مدلهای بزرگ میباشند.[19] بیشتر کارهایی که از تکنیک دادهکاوی استفاده کردهاند برای تحلیل
اتوماتیک خطا بکار میروند بعنوان نمونه، در [17] یک روش تحلیل اتوماتیک خطا (بنبست) بر مبنای دادهکاوی ارائه شده است. این روش، از الگوریتمی مشابه TF-IDF(Term Frequency-Inverse Document Frequency) استفاده میکند که منظور از TF، تعداد تکرار یک عبارت در یک مجموعه داده و IDF نیز رتبه و میزان اهمیت آن را نسبت به عبارت-های دیگر مشخص میکند، بهاینصورتکه همه گذارهای موجود در مسیرهای منجر به حالتهای خطا را رتبه بندی کرده و میزان اهمیت هر کدام از آنها را مشخص میکند. این روش در مدلهای شبکههای پتری زماندار پیاده سازی شده است. همچنین در [18] نیز از مثالهای نقض (مسیرهای منجر به حالت خطا) تولید شده توسط مدل چکر SPIN استفاده شده و با استفاده از تکنیکهای دادهکاوی و الگوریتم Sequential Pattern Mining، الگوهای ترتیبی که منجر به این خطاها میشوند را استخراج کرده و آنها را برای تصحیح مدل به مدلساز تحویل میدهند.
-3 پیشزمینه
– 1-3 دادهکاوی
دادهکاوی فرایندی است که با به خدمت گرفتن روشهای هوشمند، در میان دادهها به دنبال الگوهای خاص میگردد و در واقع، مرحلهای از فرایند کشف دانش میباشد.[20] دادهکاوی شامل مجموعهای از تکنیکهایی است که در دیگر حوزههای علمی مانند پایگاه دادهها، آمار، یادگیری ماشین، شبکههای عصبی و تشخیص الگو میتوان آن را یافت. تکنیکهای متنوعی در دادهکاوی وجود دارند که الگوهای مختلفی را تولید میکنند. روشهای کشف قوانین انجمنی و الگوهای تکراری8، طبقهبندی دادهها9و
خوشهبندی10 از عمدهترین راهکارهایی محسوب میشوند که به تولید الگوهای خاص خود میپردازند. از مهمترین الگوریتمهای کشف قوانین انجمنی و الگوهای تکراری می توان به الگوریتمهای Apriori و FP-Growth اشاره کرد.
الگوریتم Apriori جزو اولین الگوریتمهایی است که جهت یافتن الگوهای تکراری از آن استفاده میشود. نام آن برگرفته از شیوهای است که از آن استفاده میکند یعنی از دانش مرحله قبلی استفاده میکند. این الگوریتم یک الگوریتم جستجوی سطحی است که با پایان کاوش در سطح (مرحلهی (k به مرحله بعدی یعنی k+1 میرود. این عمل تا محقق شدن شرط یا شروط پایانی تکرار میشود. در مرحله kام، مجموعه اقلام kتایی تولید خواهند شد. پس از محاسبه مقدار درصد پشتیبان (درصد تکرار هر قلم داده در همه مسیرها) برای هر کدام و مقایسه آن با minsup (حداقل مقدار درصد پشتیبان) الگوهای تکراری k تایی شناسایی میشوند. در مرحلهی بعد، الگوریتم با کمک الگوهای تکراری k تایی، مجموعه اقلام (k+1) تایی کاندید که بالقوه میتوانند تکراری باشند را تولید میکند. به همین ترتیب با توجه به مقدار minsup برخی حذف شده و مجموعه اقلام تکراری (k+1) تایی تشکیل خواهند شد. این عمل تا یافتن آخرین مجموعه اقلام تکراری ادامه پیدا میکند.[21]
الگوریتم FP-Growth بدون نیاز به تولید مجموعه اقلام کاندید و با کمک ساختمان داده درخت، الگوهای تکراری را شناسایی میکند. این الگوریتم که استراتژی تقسیم و غلبه را دنبال میکند ابتدا مجموعه دادهها را به یک درخت مرسوم به FP-Tree تبدیل میکند و پس از آن بصورت مستقیم به استخراج الگوهای تکراری از این درخت میپردازد .[22]
- 2-3 سیستم تبدیل گراف
یک سیستم تبدیل گراف صفت دار11 به صـورت یـک سـهتـایی زیـر مشخص میشود: AGT(TG,HG,R) کـه در آن TG گـراف نـوع12، HG گراف میزبان13 و R مجموعه قوانین میباشد. گراف نوع یک تاپل بصـورت TG = (TGN, TGE, src, trg) می باشد که در آن، TGN مجموعـهای از گرههای نوع و TGE مجموعهای از یالهای نوع و src و trg دو تابع بصورت src, trg : TGE → TGN هستند. این توابع هر یال را به ترتیب به یـک گره مبدا و گره مقصد اختصاص میدهند. گـراف میزبـانHG بـر روی TG شامل یک همریختی گراف از HG به TG می باشد که هر یال و گره را بـه یک نوع در گراف نوع نگاشت می کند. یک قانون تبدیل گـراف p: L → R از یک نام p و یک جفت گراف نمونه بر روی گراف نوع TG تشـکیل مـی-شود. سمت چپ L نشان دهندهی پیش شرایط14 قانون و سمت راسـت R
نشان دهندهی پس شرایط15 قانون میباشند. سمت چـپ و راسـت قـانون باید با گراف نوع همریخت باشند. همچنین هر قـانون گـراف ممکـن اسـت شامل یک )NACشرایط کاربرد منفی(16 باشد که مشخصکننده ایناسـت که اگر این شرایط در گراف میزبان برقرار نبود آنگاه این قانون میتواند روی گراف میزبان اعمال شود.[8]
-4 روش پیشنهادی
در روش پیشنهادی، ابتدا مدل با اندازه کوچکی از سیستم در صورت موجود وارسی میشود به اینصورت که، فضای حالت آن با استفاده از استراتژی bfs(breadth first search) بطور کامل پیمایش شده و حالت بنبست در آن تشخیص داده میشود. با داشتن فضای حالت تولید شده و دانستن حالت بنبست و با توجه به اینکه حالت ابتدایی مشخص است، تمام مسیرها که از حالت ابتدایی شروع میشوند و به حالت بنبست ختم می-شوند را در نظر گرفته و تمام برچسب گذارها (که همان قوانین سیستم تبدیل گراف میباشند) را بدون در نظر گرفتن خود حالتها استخراج می-کنیم، سپس این مسیرها را به عنوان ورودی به الگوریتم جدید FindFreqPatt (مشابه الگوریتم (Apriori جهت کشف الگوهای تکراری میدهیم. این الگوریتم نیز، فقره داده با بزرگترین مقدار درصد پشتیبان را بر میگرداند. در واقع، این فقره داده دنبالهای از قوانین سیستم تبدیل گراف میباشد، توضیحات بیشتر در بخش 1-4 ذکر خواهند شد. حال برای تشخیص بنبست در مدل با اندازه واقعی، از خروجی الگوریتم FindFreqPatt استفاده کرده و فضای حالت آن را بطور هوشمندانه پیمایش میکنیم تا موقعی که به یک حالت بن بست برسیم، در بخش 2-4 بیشتر به این موضوع خواهیم پرداخت.
– 1-4 الگوریتم FindFreqPatt
این الگوریتم جهت کشف الگوهای تکراری بکار میرود و عملکرد آن تقریبا مشابه الگوریتم Apriori میباشد. ورودیهای این الگوریتم عبارتند از: -1 مجموعه D شامل برچسب گذارهای تمام مسیرها که از حالت ابتدایی شروع شده و به حالت بنبست ختم میشوند. -2 مجموعه C1 شامل تمام فقره دادههای ابتدایی میباشد. هر فقره داده شامل قانون گراف و درصد تکرار آن (support) در مجموعه D می باشد . منظور از درصد تکرار یک قانون، تعداد تکرار آن در مسیرهای موجود در مجموعه D است. -3 پارامتر minsup مشخص کننده حداقل مقدار درصد پشتیبان است و نشان دهنده حداقل درصد تکرار هر فقره داده در مجموعه D میباشد. انتخاب مقدار مناسب برای پارامتر minsup مهم است. انتخاب مقادیر کوچک برای این پارامتر باعث میشود علاوه بر اینکه تعداد مراحل تکرار الگوریتم افزایش یابد طول الگوی تکراری تولید شده نیز افزایش یابد. افزایش طول الگوی تکراری تولید شده به معنی این است که تعداد قوانین تبدیل گراف
موجود در الگوی تکراری که برای پیمایش هوشمندانه مدل با اندازه واقعی نیاز است افزایش یافته و این منجر به افزایش زمان اجرا خواهد شد. بالعکس، با انتخاب مقادیر بزرگ، امکان دارد که بعضی قوانینِ لازم جهت وارسی مدل در مدل با اندازه واقعی در الگوی تکراری حاصل از اجرای الگوریتم موجود نباشند و این باعث خطا در فرایند وارسی مدل بشود. تنها متغیر الگوریتم عبارت است از: مجموعه Ck+1 که این مجموعه برابر Ck × C1 (حاصلضرب کارتزین) میباشد و فقرههای داده انتخاب شده برای مرحلهِ بعد را نگه میدارد. خروجی الگوریتم نیز، فقره داده با بزرگترین
مقدار درصد پشتیبان میباشد (الگوی تکراری).شکل 1 الگوریتم FindFreqPatt را نشان میدهد.
The FindFreqPatt Algorithm : Pseudo code
intput: D , C1 , minsup
output : the item with maximum support. for ( k=1 ; Ck != ; k++) do begin
Ck+1= C k × C1
for each path t in D do
increment the count of all items in C k+1 that are contained in t remove all items in Ck+1 that their support are less than minsup
end for
return the item with maximum support in Ck-1.
شکل:1 الگوریتم FindFreqPatt
بعنوان مثال: فرض کنیم مجموعه قوانین سیستم تبدیل گراف برابرR={r1,r2,r3,r4} و مجموعه تمام مسیرها برابر D={r1r2r3r1r2r3, r1r2r1r2, r3r1r2, r1r3r2, r1r2r4} ، مجموعه C1 برابر C1={r1: 5/5=100% ,r2:5/5=100% , r3:3/5=60%, r4:1/5=20% } باشند. اگر مقدار minsup برابر 90% باشد آنگاه فقره داده برگشتی (الگوی تکراری) توسط الگوریتم برابر r1 یا r2 خواهد شد که قابل قبول نیستند. اگر مقدار minsup برابر 20% باشد آنگاه فقره داده برگشتی (الگوی تکراری) توسط الگوریتم برابر r1r2r3r1r2r3 خواهد شد که اگرچه میتواند قابل قبول باشد ولی این خروجی بعد از تکرار الگوریتم به تعداد 6 بار تولید شده و طول آن نیز بزرگ میباشد. اگر مقدار minsup برابر 50% باشد آنگاه فقره داده برگشتی (الگوی تکراری) توسط الگوریتم برابر r1r2 خواهد شد که این خروجی بعد از تکرار الگوریتم به تعداد 2 بار تولید شده و طول آن نیز نسبت به قبلی بهتر است.
- 2-4 پیمایش هوشمندانه مدل با اندازه واقعی
فرض کنیم خروجی الگوریتم FindFreqPatt بصورت الگوی riri+1…rj باشد و حالت ابتدایی متناظر با گراف میزبان مدل برابر s0 باشد. برای پیمایش هوشمندانه فضای حالت مدل با اندازه واقعی، ابتدا قانون ri را در صورت امکان روی حالت s0 اعمال کرده و به حالت s1 رفته، سپس قانون ri+1 را در صورت امکان روی حالت s1 اعمال کرده و به حالت s2 میرویم و در نهایت، قانون rj را روی حالت مرحله قبلی اعمال کرده و مثلا به حالت sk میرسیم، اگر تا این مرحله به حالت بن بست نرسیده باشیم این روند را دوباره از اول تکرار میکنیم یعنی قانون ri را در صورت امکان روی حالت sk اعمال می کنیم و ... .
