رقم المقالة : 14000219273356 زيارة : 4752 الصفحة: 73 - 79

نوع المخطوط: المحکّمة

یک هیوریستیک جدید برای تشخیص بن بست در تحلیل ایمنی سیستم های نرم افزاری

الموضوعات :

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

تاريخ الإرسال : 27 الأحد , رمضان, 1442 تاريخ التأكيد : 12 السبت , جمادى الثانية, 1443 تاريخ الإصدار : 21 الإثنين , ذو القعدة, 1443

الکلمات المفتاحية: تحلیل ایمنیوارسی مدلبن&#172, بست هیوریستیک الگوریتم&#172, های تکاملی,

ملخص المقالة :

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

المصادر:

[1] C. Baier and J. P. Katoen, Principles of Model Checking, MIT Press, 2008.
[2] J. C. Bicarregui and B. M. Matthews, "Proof and refutation in formal software development," in Proc. 3rd Irish Workshop on Formal Methods, pp. 1-15, Galway, Ireland, 1-2 Jul. 1399.
[3] R. Behjati, M. Sirjani, and M. Nili Ahmadabadi, "Bounded rational search for on-the-fly model checking of LTL properties," In: F. Arbab and M. Sirjani, (eds) Fundamentals of Software Engineering. FSEN 2009. Lecture Notes in Computer Science, vol 5961. Springer, Berlin, Heidelberg. pp. 292-307, 2009.
[4] S. Edelkamp, A. L. Lafuente, and S. Leue, "Protocol verification with heuristic search: first results," in Proc. AAAI Sym. on Model-Based Validation of Intelligence, pp. 75-83, Menlo Park, CA, USA, 9 Oct. 2000.
[5] A. Groce and W. Visser, "Heuristics for model checking Java programs," International J. on Software Tools for Technology Transfer, vol. 6, no. 4, pp. 260-276, 2004.
[6] E. Pira, V. Rafe, and A. Nikanjam, "Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm," J. of Systems and Software, vol. 131, pp. 181-200, Sept. 2017.
[7] R. Yousefian, V. Rafe, and M. Rahmani, "A heuristic solution for model checking graph transformation systems," Applied Soft Computing, vol. 24, pp. 169-180, Nov. 2014.
[8] E. Alba, F. Chicano, M. Ferreira, and J. Gomez-Pulido, "Finding deadlocks in large concurrent java programs using genetic algorithms," in Proc. of the 10th Annual Conf. on Genetic and Evolutionary Computation, pp. 1735-1742, Atlanta, GA, USA, 12-16 Jul. 2008.
[9] E. Alba and F. Chicano, "Finding safety errors with ACO," in Proc. of the 9th Annual Conf. on Genetic and Evolutionary Computation, pp. 1066-1073, London, England, 7-11 Jul. 2008.
[10] F. Chicano, M. Ferreira, and E. Alba, "Comparing metaheuristic algorithms for error detection in java programs," in Proc. Int. Symp. on Search Based Software Engineering, pp. 82-96, Szeged, Hungary, 10-12 Sept. 2011.
[11] V. Rafe, M. Moradi, R. Yousefian, and A. Nikanjam, "A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations," Applied Soft Computing, vol. 33, pp. 136-149, Aug. 2015.
[12] M. Ferreira, F. Chicano, E. Alba, and J. Gomez-Pulido, "Detecting protocol errors using particle swarm optimization with java pathfinder," in Proc. of the High Performance Computing & Simulation Conf., pp. 319-325, Nicosia, Cyprus, 3-6 Jun. 2008.
[13] H. Kastenberg and A. Rensink, "Model checking dynamic states in GROOVE," in Proc. Int. SPIN Workshop on Model Checking of Software, pp. 299-305, Vienna, Austria, 30 Mar.-1 Apr. 2006.
[14] G. Rozenberg, Handbook of Graph Grammars and Computing by Graph Transformation, World Scientific, 1997.
[15] P. E. Hart, N. J. Nilsson, and B. Raphael, "A formal basis for the heuristic determination of minimum cost paths," IEEE Trans. on Systems Science and Cybernetics, vol. 4, no. 2, pp. 100-107, Jul. 1968.
[16] R. L. Haupt and S. E. Haupt, Practical Genetic Algorithms, John Wiley & Sons, 2004.
[17] J. Kennedy and R. Eberhart, "Particle swarm optimization," in Proc. IEEE Int Conf. on Neural Networks, , vol. 4, pp. 1942-1948, Perth, Australia, 27 Nov.-1 Dec. 1995.
[18] P. Larranaga and J. A. Lozano, Estimation of Distribution Algorithms: A New Tool for Evolutionary Computation, Springer Science & Business Media, 2001.
[19] J. Pearl, Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference, Morgan Kaufmann, 1988.
[20] A. Schmidt, "Model checking of visual modeling languages," in Proc. Conf. of PhD Students in Computer Science, p. 102, 2004.
[21] J. F. Groote and J. V. D. Pol, "A bounded retransmission protocol for large data packets," in Proc. Int. Conf. on Algebraic Methodology and Software Technology, pp. 536-550, Munich, Germany, 1-5 Jul. 1996.
[22] E. Pira, V. Rafe, and A. Nikanjam, "Searching for violation of safety and liveness properties using knowledge discovery in complex systems specified through graph transformations," Information and Software Technology, vol. 97, pp. 110-134, May 2018.

نص كامل:

معرفي يک روش جديد خوشه‌يابي خودکار

مقاله پژوهشی

یک هیوریستیک جدید برای تشخیص بن‌بست
در تحلیل ایمنی سیستم‌های نرم‌افزاری

عین‌الله پیرا

چكیده: تحلیل ایمنی سیستم‌های نرم‌افزاری، خصوصاً از نوع بحرانی- ایمنی، باید به طور دقیق انجام شود زیرا وجود حتی یک خطای کوچک در چنین سیستم‌هایی ممکن است نتایج فاجعه‌باری داشته باشد. ضمناً چنین تحلیلی باید قبل از پیاده‌سازی یعنی در مرحله طراحی و در سطح مدل انجام شود. وارسی مدل، یک روش دقیق و مبتنی بر ریاضی است که ایمنی سیستم‌های نرم‌افزاری را با دریافت مدلی از آن و بررسی تمام حالت‌های قابل دسترس مدل انجام می‌دهد. با توجه به پیچیدگی بعضی سیستم‌ها و مدل‌های آن، وارسی مدل ممکن است با مشکل انفجار فضای حالت مواجه شود، یعنی نتواند تمام حالت‌های قابل دسترس را پیمایش کند. یک راه حل برای حل مشکل انفجار فضای حالت در چنین سیستم‌هایی این است که به جای تأیید ایمنی، وارسی مدل سعی می‌کند آنها را با یافتن خطاهایی از جمله بن‌بست (در صورت موجود) رد کند. اگرچه قبلاً هیوریستیکی برای یافتن بن‌بست در فضای حالت مدل ارائه شده و آن را در چندین الگوریتم جستجوی مکاشفه‌ای ساده و تکاملی به کار برده‌اند ولی سرعت تشخیص آن پایین بوده است. این مقاله، یک هیوریستیک جدید برای یافتن بن‌بست در فضای حالت مدل ارائه می‌کند و سرعت تشخیص آن با به کار بردن در الگوریتم‌های جستجوی مکاشفه‌ای ساده از جمله عمقی تکرارشونده A* و جستجوی پرتو و الگوریتم‌های تکاملی مختلف از جمله ژنتیک، بهینه‌سازی ازدحام ذرات و بهینه‌سازی بیزی با روش قبلی مقایسه می‌شود. مقایسه نتایج تجربی تأیید می‌کنند که هیوریستیک جدید می‌تواند حالت بن‌بست را در زمان کمتری نسبت به هیوریستیک قبلی پیدا کند.

کلیدواژه: الگوریتم‌های تکاملی، بن‌بست، تحلیل ایمنی، وارسی مدل، هیوریستیک.

1- مقدمه

سیستم‌های نرم‌افزاری مدرن شامل زیرسیستم‌هایی می‌باشند که در بعضی شرایط مجبور هستند به منابع سیستم به طور هم‌روند و مشترک دسترسی پیدا کنند و این ممکن است باعث ایجاد حالت بن‌بست² شود. کشف و رفع حالت‌های خطا (برای مثال بن‌بست) یا به عبارت کلی‌تر، تحلیل ایمنی سیستم‌های نرم‌افزاری، خصوصاً از نوع بحرانی- ایمنی³، باید به طور دقیق و قبل از پیاده‌سازی یعنی در مرحله طراحی و در سطح مدل انجام شود. مجموعه‌ای از روش‌های رسمی⁴ مبتنی بر تحلیل‌های دقیق ریاضی وجود دارند که صحت مدل را با توجه به ویژگی‌های مورد انتظار بررسی می‌کنند. وارسی مدل⁵ یک روش رسمی است که مدلی از سیستم به همراه ویژگی‌های توصیف‌شده در قالب فرمول‌های منطق زمانی⁶ را دریافت کرده و درستی/ نادرستی ویژگی‌ها را با کاوش همه حالت‌های قابل دسترسِ (فضای حالت) مدل بررسی می‌کند [1]. با توجه به پیچیدگی بعضی سیستم‌ها و مدل‌های آن، وارسی مدل ممکن است با مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالت‌های ممکن) مواجه شود. یک راه حل برای حل مشکل انفجار فضای حالت در چنین سیستم‌هایی این است که وارسی مدل سعی می‌کند آنها را با یافتن خطاهایی از جمله بن‌بست (در صورت موجود) رد کند. به این مفهوم که به جای اثبات عدم وجود خطا، دنبال خطا می‌گردد. لازم به ذکر است که اگر وارسی مدل در چنین حالتی نتواند خطایی پیدا را کند، نمی‌توان ادعا کرد که سیستم بدون خطا است زیرا فقط قسمتی از فضای حالت پیمایش شده است [2]. البته می‌توان با روش‌های احتمالی از جمله مونت‌کارلو تخمین معناداری را از میزان صحت سیستم ارائه کرد [3].

فضای حالت مدل معمولاً با یک گراف نمایش داده می‌شود که در آن، رئوس و یال‌ها به ترتیب مجموعه حالت‌ها و گذارهای مابین آنها را نشان می‌دهند. در فضای حالت مدل، بن‌بست، حالتی را نشان می‌دهد که هیچ گذار خروجی ندارد که به چنین حالتی، حالت نهایی نیز می‌گویند. به عبارت دیگر، چنین گرهی در گراف معادل، یال خروجی ندارد. بعد از عمل وارسی، وارسی‌گر یک مثال نقض⁷ تولید می‌کند. یک مثال نقض نشان‌دهنده مسیری از حالت‌ها (گره‌ها) و گذارهای (یال‌های) مابین آنها است به طوری که این مسیر از حالت (گره) ابتدایی شروع شده و به یک حالت (گره) بن‌بست ختم می‌شود. یافتن چنین مسیری نیز ممکن است باعث بروز مشکل انفجار فضای حالت شود. در [4] هیوریستیکی برای یافتن بن‌بست در فضای حالت مدل ارائه شده است. این هیوریستیک مسیری را دریافت کرده و مجموع تعداد گذارهای خروجی گره‌های موجود در مسیر مورد نظر را برمی‌گرداند. واضح است که هرچه مقدار هیوریستیک برای مسیری کمتر باشد، احتمال به بن‌بست رسیدن آن بالا خواهد بود. برای تست این هیوریستیک، آن را در الگوریتم‌های جستجوی عمقی ⁸(DFS) و ردیفی ⁹(BFS) [5]، جستجوی مکاشفه‌ای ساده از جمله A* [5]، عمقی تکرارشونده A* (IDA*) و جستجوی پرتو ¹⁰(BS)

شکل 1: جزئیات مدل طراحی‌شده برای مسأله غذاخوری فیلسوفان با 2 فیلسوف [6].

[6] و الگوریتم‌های تکاملی مختلف از جمله ژنتیک ¹¹(GA) [4]، [7] و [8]، بهینه‌سازی کلونی مورچگان ¹²(ACO) [9]، شبیه‌سازی ذوب فلزات ¹³(SA) [10]، بهینه‌سازی ازدحام ذرات ¹⁴(PSO) [11] و [12] و بهینه‌سازی بیزی ¹⁵(BOA) [6] به کار برده‌اند. اگرچه این الگوریتم‌ها می‌توانند حالت بن‌بست را با موفقیت تشخیص دهند ولی سرعت تشخیص می‌تواند بهبود پیدا کند.

در این مقاله، یک هیوریستیک جدید برای یافتن بن‌بست در فضای حالت مدل ارائه می‌کنیم. این هیوریستیک به هر مسیری که تعداد گذارهای خروجی گره‌های موجود در آن تقریباً نزولی باشد، عدد کمتری
را اختصاص می‌دهد. در واقع به جای مجموع تعداد گذارهای خروجی گره‌های موجود، مجموع حاصل‌ضرب اختلاف تعداد گذارهای گره‌های پشت سر هم و در موقعیت گره یعنی را به عنوان مقدار برازندگی برای آن مسیر در نظر می‌گیرد. هرچه این مقدار برای مسیری کمتر باشد (یعنی تعداد گذارهای خروجی گره‌های موجود در آن تقریباً نزولی باشد)، احتمال رسیدن آن مسیر به بن‌بست بیشتر خواهد بود. برای تست هیوریستیک جدید، آن را در الگوریتم‌های مختلف استفاده کرده و این الگوریتم‌ها را در ابزار GROOVE [13] پیاده‌سازی می‌کنیم. سپس با اجرای این الگوریتم‌ها روی چندین مسأله شناخته‌شده، سرعت تشخیص آن را با هیوریستیک قبلی مقایسه می‌کنیم. قابل ذکر است که ابزار GROOVE، مدل‌های توصیف‌شده با زبان رسمی تبدیل گراف [14] را می‌پذیرد و در نتیجه مسایل در نظر گرفته شده نیز باید با این زبان رسمی توصیف شوند.

2- پیش‌زمینه

2-1 زبان رسمی تبدیل گراف

این زبان از گراف‌ها و تبدیلات مابین آنها جهت مدل‌سازی حالت‌ها و رفتارهای یک سیستم بهره می‌برد [14]. مدل‌هایی که با این زبان توصیف می‌شوند دارای سه جزء گراف نوع ، گراف میزبان و مجموعه قوانین تبدیل است. گراف شامل مجموعه‌ای از نوع‌های گره¹⁶ و مجموعه‌ای از نوع‌های یال¹⁷ است و گره‌ها و یال‌های مجاز را نشان می‌دهد که می‌توانند در طی تبدیلات گراف وجود داشته باشند. گراف حالت اولیه (آغازین) سیستم را نشان می‌دهد و بدیهی است که گره‌ها و یال‌های آن باید جزء نوع‌های گره و نوع‌های یال موجود در گراف باشند. مجموعه قوانین تبدیلی را نشان می‌دهد که حالات مختلف سیستم را می‌توانند تولید کنند. هر قانون تبدیل به صورت سه‌تایی تعریف می‌شود که در آن، گراف شرایطی را مشخص می‌کند که باید گراف مربوط به حالت فعلی داشته باشد تا این قانون بتواند روی این حالت اِعمال شود. گراف نیز شرایطی را تعیین می‌کند که باید گراف مربوط به حالت حاصل بعد از اِعمال قانون داشته باشد. گراف نیز محدودیت‌هایی را مشخص می‌کند که نباید در گراف مربوط به حالت فعلی باشند تا این قانون بتواند اِعمال شود. شکل 1 جزئیات مدل طراحی‌شده برای مسأله غذاخوری فیلسوفان با 2 فیلسوف را نشان می‌دهد [6]. قسمت‌های a و b در این شکل به ترتیب گراف‌های نوع و میزبان را نشان می‌دهند. مطابق این گراف نوع، هر فیلسوف می‌تواند در حالت‌های مختلف فکرکردن (thinking)، گرسنه‌بودن (hungry)، فقط چنگال چپ را در دست داشتن (hasLeft)، هر دو چنگال را در دست داشتن و خوردن (eating) و فقط چنگال راست در دست داشتن (hasRight) باشد. گراف میزبان نیز نشان می‌دهد فیلسوفان در ابتدا در حالت فکرکردن هستند. قسمت c قانون get-left را نشان می‌دهد. در گراف مربوط به این قانون، گراف‌های ، و را با هم ادغام کرده و از کدگذاری رنگی برای تشخیص هر کدام از اجزای آن استفاده می‌کنیم. اجزای مشترک بین گراف‌های و به صورت نازک سیاه‌رنگ هستند. اجزای مختص گراف به صورت گره‌ها با دو لبه و یال‌های نقطه‌چین آبی‌رنگ مشخص گردیده‌اند در حالی که اجزای مختص گراف
با رنگ سبز مشخص شده‌اند. در نهایت گره‌ها با دو لبه و یال‌های نقطه‌چین قرمزرنگ متعلق به گراف هستند. برای اِعمال قانون روی حالت (که در واقع به صورت یک گراف است)، ابتدا رخدادهای گراف در حالت پیدا شده و یکی از آنها که شامل گراف نیست با گراف جایگزین شده و حالت جدیدی را تولید می‌کند. برای تولید فضای حالت یک مدل، همه قوانین باید به طور مکرر روی حالت‌های تولیدشده اِعمال شوند.

2-2 وارسی مدل

وارسی مدل یک روش رسمی مبتنی بر تحلیل دقیق ریاضی است که درستی/ نادرستی مدل را با توجه به ویژگی‌های توصیف‌شده در قالب فرمول‌های منطق زمانی بررسی می‌کند. ایمنی یکی از ویژگی‌های مهم سیستم است که می‌تواند از طریق وارسی مدل و با بررسی تمام حالت‌های

(الف) (ب)

شکل 2: (الف) تأیید و (ب) انکار ویژگی ایمنی .

قابل دسترس سیستم تأیید شود. شکل 2- الف مثالی از تأیید ایمنی ویژگی را در فضای حالت یک مدل نشان می‌دهد که مطابق این شکل، ویژگی باید در تمام حالت‌ها ارضا شود. با توجه به این که تعداد حالت‌های قابل دسترس در سیستم‌های بزرگ باعث وقوع مشکل انفجار فضای حالت می‌شوند، بنابراین وارسی مدل سعی می‌کند به جای تأیید ویژگی ایمنی ، آن را انکار کند [1]. انکار ویژگی ایمنی می‌تواند با یافتن حالتی در فضای حالت و نقض ویژگی محقق شود. به عبارت دیگر، حالتی در فضای حالت یافت بشود که در آن ویژگی ارضا گردد. شکل 2- ب این روند را توضیح می‌دهد. به محض پیداشدن چنین حالتی (حالت هدف)، وارسی‌گر یک مثال نقض تولید می‌کند که شامل اطلاعاتی از جمله محل واقعی خطا در سیستم است و کاربر می‌تواند با استفاده از این اطلاعات، خطای گزارش‌شده را در سیستم رفع کند. ولی اگر چنین حالتی (حالت هدف) پیدا نشود نمی‌توان ادعا کرد که سیستم بدون خطا است زیرا فقط قسمتی از فضای حالت پیمایش شده است.

2-3 خلاصه‌ای از الگوریتم‌های به کار رفته در این مقاله

در این بخش، خلاصه‌ای از الگوریتم‌های به کار رفته در این مقاله از جمله عمقی تکرارشونده A* (IDA*) و جستجوی پرتو (BS) و الگوریتم‌های تکاملی مختلف از جمله ژنتیک (GA)، بهینه‌سازی ازدحام ذرات (PSO) و بهینه‌سازی بیزی (BOA) را ارائه می‌کنیم.

الگوریتم عمقی تکرارشونده A*: این الگوریتم ترکیبی از الگوریتم‌های جستجوی عمق اول (DFS) و A* [15] را به شکل مداوم تکرار کرده تا یا حالت هدف پیدا شود و یا تعداد تکرارها (عمق جستجو) به عدد از پیش تعیین شده برسد. در تکرار ام ، جستجوی عمقی تا عمق را انجام داده و هزینه این مسیرها را مشابه الگوریتم A* و با استفاده از هیوریسیتک ارائه‌شده محاسبه می‌کند و مسیرهایی را که هزینه آنها از یک مقدار آستانه بیشتر باشد نادیده می‌گیرد.

جستجوی پرتو: این الگوریتم مشابه جستجوی سطح اول (BFS) به صورت سطح به سطح فضای حالت را کاوش می‌کند با این تفاوت که فقط به تعداد مشخصی، حالت (عرض پرتو) با بیشترین مقدار هیوریستیک را در هر سطح در نظر گرفته و بقیه حالت‌ها را در نظر نمی‌گیرد. این الگوریتم تا موقعی ادامه پیدا می‌کند که یا حالت هدف پیدا شود و یا تعداد سطوح پیمایش‌شده (عمق جستجو) به یک عدد از پیش مشخص شده برسد.

الگوریتم ژنتیک: این الگوریتم از مشهورترین الگوریتم‌های تکاملی می‌باشد که بر اصل بقای اصلح داروین استوار است [16] و همواره با جمعیتی از راه حل‌های کاندیدا (اصطلاحاً کروموزوم‌ها) سروکار دارد که در آن جمعیت اولیه به صورت تصادفی تولید می‌شود. این الگوریتم برای تولید جمعیت بعدی، 1) جمعیت فعلی را با استفاده از یک تابع برازش ارزیابی کرده و تعدادی از برازنده‌ترین آنها را انتخاب می‌کند. 2) به کمک عملگر ترکیب و با احتمال نرخ ترکیب، کروموزوم‌های انتخاب‌شده را با هم ترکیب کرده تا کروموزوم‌های جدید تولید شوند. 3) با احتمال نرخ جهش، بعضی کروموزوم‌های جدیداً تولیدشده را انتخاب کرده و بعضی ژن‌های آنها را تغییر می‌دهد. 4) کروموزوم‌های جدیداً تولیدشده را با بعضی از کروموزوم‌های فعلی که دارای شایستگی پایینی می‌باشند جایگزین می‌کند. این روند (تولید جمعیت بعدی از فعلی) تا هنگامی ادامه پیدا می‌کند که یک راه حل (تقریباً) بهینه پیدا شود و یا تعداد تکرارها به یک عدد بیشینه برسد. در مسأله وارسی ایمنی و پیداکردن یک حالت بن‌بست توسط این الگوریتم، هر مسیری که از حالت ابتدایی شروع شده و دارای طول مشخصی باشد به عنوان یک کروموزوم در نظر گرفته می‌شود. همچنین هیوریتسیک برای یافتن بن‌بست به عنوان تابع برازش در نظر گرفته می‌شود [7].

الگوریتم بهینه‌سازی ازدحام ذرات: این الگوریتم مبتنی بر رفتار اجتماعی پرندگان است که به صورت گروهی دنبال غذا می‌گردند [17] و با گروهی از ذرات (راه حل‌ها) سروکار دارد که در ابتدا به صورت تصادفی تولید می‌شوند. هر ذره دارای یک موقعیت و سرعت حرکت در فضای جستجو است. موقعیت، سرعت و جهت حرکت یک ذره تحت تأثیر بهترین موقعیت خود و موقعیت دیگران قرار دارد. بعد از تولید تصادفی ذرات در مرحله ابتدایی، میزان برازندگی آنها با استفاده از تابع برازش محاسبه شده و مقادیر و به روز رسانی می‌شوند. در هر مرحله تکرار، موقعیت و سرعت ذرات توسط (1) و (2) به روز رسانی گردیده و این روند تا موقعی ادامه می‌یابد که یک راه حل (تقریباً) بهینه پیدا شود و یا تعداد تکرارها به یک عدد بیشینه برسد. مشابه با الگوریتم ژنتیک، در این الگوریتم نیز هر مسیری که از حالت ابتدایی شروع شده و دارای طول مشخصی باشد به عنوان یک ذره در نظر گرفته می‌شود [11]

(1)

(2)

مقدار تأثیر سرعت فعلی ذره را بر سرعت بعدی آن مشخص می‌کند. مقادیر و به ترتیب تأثیر بهترین موقعیت خود و دیگران را بر سرعت بعدی ذره تعیین می‌کنند و مقادیر آنها طوری در نظر گرفته می‌شود که مجموع آنها حداکثر برابر 4 شود.

الگوریتم بهینه‌سازی بیزی: این الگوریتم نوعی الگوریتم تخمین توزیع است که در آن، یک شبکه بیزی از راه حل‌های برازنده جمعیت فعلی ساخته شده و همچنین این شبکه نیز برای تولید راه حل‌های جدید نمونه‌برداری می‌شود [18]. شبکه بیزی یک مدل گرافیکی احتمالی است که وابستگی‌های شرطی مابین متغیرهای مختلف مسأله را نمایش می‌دهد [19]. یک شبکه بیزی دارای دو مؤلفه ساختار و پارامترها می‌باشد: ساختار توسط یک گراف جهت‌دار بدون دور نمایش داده می‌شود که در آن، رئوس و یال‌ها به ترتیب متغیرهای مسأله و وابستگی‌های شرطی مابین آنها را نشان می‌دهند. پارامترهای شبکه نیز توسط مجموعه‌ای از جداول احتمال شرطی مشخص می‌شوند به این صورت که هر جدول، احتمال‌های شرطی همه مقادیر یک متغیر وابسته را به ازای همه مقادیر والدهای (رئوس آغازین یال‌ها) آن متغیر نشان می‌دهد. الگوریتم بهینه‌سازی بیزی پس از تولید تصادفی جمعیت اولیه، آنها را با استفاده از تابع برازش ارزیابی کرده و با راه حل‌های (کروموزوم‌های) برازنده انتخاب‌شده، یک شبکه بیزی ایجاد می‌کند. سپس از روش نمونه‌برداری منطق احتمالی استفاده کرده و کروموزوم‌های جدید تولید می‌نماید و آنها را با استفاده از یک روش جایگزینی به جمعیت فعلی وارد می‌کند. این فرایند تا موقعی تکرار می‌گردد که یک راه حل (تقریباً) بهینه پیدا شود و یا تعداد تکرارها به
یک عدد بیشینه برسد. مشابه با الگوریتم ژنتیک، در این الگوریتم نیز
هر مسیری که از حالت ابتدایی شروع شده و دارای طول مشخصی باشد به عنوان یک کروموزوم در نظر گرفته می‌شود [6].

3- هیوریستیک ارائه‌شده

همان طور که اشاره شد بن‌بست در فضای حالت یک مدل به حالتی گفته می‌شود که هیچ گذار خروجی ندارد. در مدل‌های طراحی‌شده با زبان تبدیل گراف می‌توان حالت بن‌بست را به صورت زیر بیان کرد: حالت بن‌بست است اگر برای همه قوانین به شکل ، حالت دارای هیچ رخدادی از گراف نباشد یا رخداد موجود شامل گراف باشد. در مسیری که از حالت ابتدایی شروع شده و به حالت بن‌بست ختم می‌شود، ابتدا تعداد زیادی قانون می‌توانند روی حالت ابتدایی اِعمال شوند ولی روی حالت‌های بعدی (خصوصاً حالت‌های انتهایی مسیر)، تعداد قوانین اِعمال‌شده (گذارهای خروجی) کمتر گردیده و در نهایت به صفر می‌رسند. هیوریتسیکی که قبلاً برای یافتن چنین مسیری ارائه شده است (به نام HeuSum) فقط مجموع تعداد گذارهای خروجی گره‌های موجود در مسیر مورد نظر را به عنوان برازندگی در
نظر می‌گیرد. به عنوان مثال برای دو مسیر با تعداد گذارهای خروجی و به ترتیب مقادیر 10 و 11 را در نظر می‌گیرد و مفهومش این است که مسیر 1 شانس بیشتری برای رسیدن به حالت بن‌بست دارد. در حالی که احتمال رسیدن مسیر 2
به بن‌بست از مسیر 1 بیشتر است زیرا تعداد گذارهای خروجی برای حالت‌های موجود رفته‌رفته به عدد صفر نزدیک می‌شود.

هیوریستیک ارائه‌شده در این مقاله (به نام HeuSumDiff) به جای مجموع تعداد گذارهای خروجی، مجموع حاصل‌ضرب اختلاف تعداد گذارهای گره‌های پشت سر هم و در موقعیت گره یعنی را به عنوان مقدار برازندگی برای آن مسیر در نظر می‌گیرد. هرچه این مقدار برای مسیری کمتر باشد (یعنی تعداد گذارهای خروجی گره‌های موجود در آن تقریباً نزولی باشد)، احتمال رسیدن آن مسیر به بن‌بست بیشتر خواهد بود. فرض کنید که می‌خواهیم مقدار برازندگی را برای مسیر با استفاده از هیوریستیک ارائه‌شده محاسبه کنیم. اگر تعداد گذارهای خروجی برای حالت باشد، مقدار برازندگی برای مسیر از فرمول زیر محاسبه می‌شود

(3)

در مسیرهای منجر به بن‌بست، چون مقادیر برای حالت‌های آخر (های نزدیک به ) اعداد منفی نزدیک صفر هستند، جهت افزایش تأثیر این مقادیر در مقدار برازندگی، برابر این مقادیر را در نظر می‌گیریم. به عنوان مثال، این تابع برای دو مسیر با تعداد گذارهای خروجی و به ترتیب مقادیر 0 و 6- را به صورت زیر محاسبه می‌کند و این نشان می‌دهد که مسیر 2 برازنده‌تر است

(4)

4- ارزیابی و مقایسه کارایی هیوریستیک‌های HEUSUMDIFF و HEUSUM

برای ارزیابی و مقایسه کارایی هیوریستیک‌های HeuSumDiff و HeuSum، آنها را در الگوریتم‌های IDA*، BS، GA، PSO و BOA استفاده کرده و این الگوریتم‌ها را با زبان برنامه‌نویسی Java و در ابزار متن‌باز GROOVE پیاده‌سازی می‌کنیم. سپس با اجرای این الگوریتم‌ها روی مسایل غذاخوری فیلسوفان [20]، پروتکل انتقال مجدد به تعداد محدود [21] و چرخه حیات پردازه [22]، سرعت تشخیص آنها را با
هم مقایسه می‌نماییم. نسخه جدید ابزار GROOVE به همراه مسایل استفاده‌شده روی وب قابل دسترس است¹⁸.

مسأله غذاخوری فیلسوفان (DPH): این مسأله، نحوه غذاخوری چندین فیلسوف دور یک میز را توصیف می‌کند که مابین هر دوی آنها یک چنگال وجود دارد. هر فیلسوف می‌تواند در حالت‌های مختلف فکرکردن (thinking)، گرسنه‌بودن (hungry)، فقط چنگال چپ را در دست داشتن (hasLeft)، هر دو چنگال را در دست داشتن و خوردن (eating) و فقط چنگال راست در دست داشتن (hasRight) باشد. در ابتدا همه فیلسوفان در حالت thinking هستند و می‌توانند بعد از مدتی احساس گرسنگی کرده و به حالت hungry بروند. فیلسوف با حالت hungry می‌تواند چنگال چپ را در صورت آزادبودن برداشته و به حالت hasLeft برود و اگر چنگال راستش نیز آزاد باشد، آن را برداشته و به حالت eating می‌رود. فیلسوف در حال eating بعد از مدتی چنگال چپش را رها کرده و به حالت hasRight می‌رود و سپس چنگال راستش را نیز رها کرده و دوباره به حالت thinking می‌رود. در این مسأله اگر همه فیلسوفان به طور هم‌زمان چنگال چپ را برداشته و به حالت hasLeft بروند و منتظر چنگال راستشان باشند، آن گاه حالت بن‌بست پیش می‌آید.

مسأله پروتکل انتقال مجدد به تعداد محدود (BRP): این پروتکل که مربوط به انتقال فایل‌ها از طریق یک کانال ارتباطی lossy است توسط شرکت فیلیپس استفاده می‌گردد. در این پروتکل، برخی فریم‌های فایل انتقالی می‌توانند به دفعات محدودی مجدداً انتقال شوند. اگر بعضی فریم‌ها با مشکل مواجه گردند ممکن است انتقال فایل لغو شود و چنین وضعیتی را می‌توان به عنوان یک حالت بن‌بست (نهایی) تلقی کرد.

مسأله چرخه حیات پردازه (PLC): در این مسأله، چرخه حیات یک فرایند در یک سیستم عامل از مرحله تولد (ایجاد) تا مرگ (خاتمه) توصیف می‌شود. فرایند ایجادشده در صورت وجود فضای کافی، به حافظه لود شده و منتظر ابزار CPU یا I/O می‌ماند. به محض اتمام اجرای فرایند، تمام منابع در دسترس آزاد شده و فرایند خاتمه می‌یابد. در این مسأله، اجرا
و خاتمه همه فرایندهای موجود را می‌توان به عنوان وضعیت بن‌بست (نهایی) در نظر گرفت.

قبل از اجرای الگوریتم‌ها باید مقادیر مناسب را برای پارامترهای مورد نیاز آنها ارائه کنیم. بعضی پارامترها برای مدل‌ها با اندازه‌های مختلف دارای مقدار ثابتی هستند که جدول 1 مقادیر مناسب را برای این پارامترهای ثابت نشان می‌دهد. در حالی که بعضی پارامترها از جمله
اندازه جمعیت (population) و حداکثر عمق جستجو یا همان طول کروموزوم‌ها بسته به نوع مسأله و اندازه مدل دارای مقادیر متغیری می‌باشند. جدول 2 مقادیر مناسب را برای این پارامترهای متغیر نشان می‌دهد.

[1] این مقاله در تاریخ 20 اردیبهشت ماه 1400 دریافت و در تاریخ 2 آذر ماه 1400 بازنگری شد.

عین‌الله پیرا (نویسنده مسئول)، دانشكده فناوری اطلاعات و مهندسي كامپيوتر، دانشگاه شهید مدنی آذربایجان، تبریز، ایران، (email: pira@azaruniv.ac.ir).

[2] . Deadlock

[3] . Safety-Critical

[4] . Formal Methods

[5] . Model Checking

[6] . Temporal Logic

[7] . Counterexample

[8] . Depth First Search

[9] . Breadth First Search

[10] . Beam Search

[11] . Genetic Algorithm

[12] . Ant Colony Optimization

[13] . Simulated Annealing

[14] . Particle Swarm Optimization

[15] . Bayesian Optimization Algorithm

[16] . Node Types

[17] . Edge Types

[18] . https://github.com/EinPira/Groove-HEUSUMDIFF

شکل 3: مقایسه میانگین زمان اجرای الگوریتم بهینه‌سازی بیزی برای کشف بن‌بست.

جدول 1: مقادیر مناسب برای پارامترهای ثابت الگوریتم‌ها.

100		حداکثر تعداد تکرار هر الگوریتم
جستجوی پرتو (BS)		الگوریتم بهینه‌سازی بیزی (BOA)
عرض پرتو10	مسایل غذاخوری فیلسوفان و چرخه حیات پردازه	4/0	نرخ انتخاب (selecton rate)
عرض پرتو20	پروتکل انتقال مجدد به تعداد محدود	5/0	نرخ جایگزینی (replacement rate)
الگوریتم بهینه‌سازی ازدحام ذرات (PSO)		الگوریتم ژنتیک (GA)
2		6/0	نرخ ترکیب (crossover rate)
8/0		3/0	نرخ جهش (mutation rate)

جدول 2: مقادیر مناسب برای پارامترهای متغیر الگوریتم‌ها.

حداکثر عمق جستجو	اندازه جمعیت	اندازه مدل	مسأله
20	10	8 فیلسوف	غذاخوری فیلسوفان
25	15	10 فیلسوف	غذاخوری فیلسوفان
180	20	20 فرایند و 8 قطعه حافظه	چرخه حیات پردازه
280	40	30 فرایند و 8 قطعه حافظه	چرخه حیات پردازه
50	20	8 فریم	پروتکل انتقال مجدد به تعداد محدود
60	30	10 فریم	پروتکل انتقال مجدد به تعداد محدود

الگوریتم‌های استفاده‌شده در این مقاله، قبلاً در مقالات مختلفی ارائه شده‌اند و دقت آنها در تشخیص حالت بن‌بست، روی مسایل مختلف و
با اندازه‌های متفاوت بررسی گردیده‌اند. مطابق با مقالات مرتبط با این الگوریتم‌ها، میزان دقت (accuracy) هر کدام از الگوریتم‌ها به پارامترهای مختلفی از جمله حداکثر عمق جستجو وابسته است. با اجراهای مختلف این الگوریتم‌ها به ازای هیوریستیک‌های HeuSumDiff و HeuSum به این نتیجه رسیده‌ایم که این هیوریستیک‌ها دارای دقت مشابهی هستند، یعنی اگر الگوریتمی با هیوریستیک HeuSum بتواند بن‌بستی را پیدا کند با هیوریستیک HeuSumDiff نیز خواهد توانست و بالعکس. در این مقاله، مسایل (غذاخوری فیلسوفان، پروتکل انتقال مجدد به تعداد محدود و چرخه حیات پردازه) و مدل‌هایی را انتخاب کرده‌ایم که این الگوریتم‌ها بتوانند به طور 100% حالت بن‌بست را پیدا کرده تا امکان مقایسه سرعت تشخیص این هیوریستیک‌ها فراهم شود.

برای تولید نتایج، کلیه الگوریتم‌ها را با استفاده از یک پردازنده اجرا کرده‌ایم. شکل‌های 3 تا 7 نمودار میانگین حاصل از اجرای این الگوریتم‌ها به تعداد 30 بار
را برای کشف حالت بن‌بست در مدل‌ها با اندازه‌های مختلفی از مسایل غذاخوری فیلسوفان، پروتکل انتقال مجدد به تعداد محدود و چرخه حیات پردازه نمایش می‌دهد. در این نمودارها، برای مدل‌ها با اندازه فیلسوف از نماد ، برای مدل‌ها با اندازه فرایند و قطعه حافظه از نماد و برای مدل‌ها با اندازه فریم از نماد استفاده می‌کنیم.

مطابق شکل 3، در اکثر مدل‌های در نظر گرفته شده، میانگین زمان اجرای الگوریتم BOA برای هیوریستیک HeuSumDiff کمتر از زمان اجرای آن به ازای هیوریستیک HeuSum است. در مدل از مسأله چرخه حیات پردازه، هیوریستیک HeuSum دارای سرعت تشخیص بهتری نسبت به هیوریستیک HeuSumDiff است.

برای الگوریتم GA (شکل 4)، سرعت تشخیص بن‌بست در همه مدل‌های در نظر گرفته شده به ازای هیوریستیک HeuSumDiff
بیشتر از هیوریستیک HeuSum است. در همه مدل‌ها به جز مدل از مسأله چرخه حیات پردازه، تفاوت سرعت تشخیص این دو هیوریستیک نسبتاً کم است ولی در این مدل، هیوریستیک HeuSumDiff سرعت تشخیص خیلی بهتری نسبت به هیوریستیک HeuSum دارد.

مشابه با الگوریتم‌های BOA و GA، سرعت تشخیص بن‌بست توسط الگوریتم PSO در همه مدل‌های در نظر گرفته شده، به ازای هیوریستیک HeuSumDiff بیشتر از هیوریستیک HeuSum است (شکل 5). البته در همه مدل‌های مسأله چرخه حیات پردازه، تفاوت سرعت تشخیص این دو هیوریستیک خیلی زیاد است.

شکل‌های 6 و 7 تأیید می‌کنند که سرعت تشخیص بن‌بست توسط الگوریتم‌های IDA* و BS در همه مدل‌های در نظر گرفته شده به ازای هیوریستیک HeuSumDiff کمی بیشتر از هیوریستیک HeuSum است.

شکل 4: مقایسه میانگین زمان اجرای الگوریتم ژنتیک برای کشف بن‌بست.

شکل 5: مقایسه میانگین زمان اجرای الگوریتم بهینه‌سازی ازدحام ذرات برای کشف بن‌بست.

شکل 6: مقایسه میانگین زمان اجرای الگوریتم جستجوی پرتو برای کشف بن‌بست.

5- نتیجه‌گیری و کارهای آینده

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

شکل 7: مقایسه میانگین زمان اجرای الگوریتم جستجوی عمقی تکرارشونده A* برای کشف بن‌بست.

هیوریستیک قبلی مقایسه گردید. مقایسه نتایج تجربی تأیید می‌کنند که هیوریستیک جدید می‌تواند حالت بن‌بست را در زمان کمتری نسبت به هیوریستیک قبلی پیدا کند. بهبود هیوریستیک ارائه‌شده در این مقاله می‌تواند به عنوان کار بعدی در نظر گرفته شود.

مراجع

[1] C. Baier and J. P. Katoen, Principles of Model Checking, MIT Press, 2008.

[2] J. C. Bicarregui and B. M. Matthews, "Proof and refutation in formal software development," in Proc. 3rd Irish Workshop on Formal Methods, pp. 1-15, Galway, Ireland, 1-2 Jul. 1399.

[3] R. Behjati, M. Sirjani, and M. Nili Ahmadabadi, "Bounded rational search for on-the-fly model checking of LTL properties," In: F. Arbab and M. Sirjani, (eds) Fundamentals of Software Engineering. FSEN 2009. Lecture Notes in Computer Science, vol 5961. Springer, Berlin, Heidelberg. pp. 292-307, 2009.

[4] S. Edelkamp, A. L. Lafuente, and S. Leue, "Protocol verification with heuristic search: first results," in Proc. AAAI Sym. on Model-Based Validation of Intelligence, pp. 75-83, Menlo Park, CA, USA, 9 Oct. 2000.

[5] A. Groce and W. Visser, "Heuristics for model checking Java programs," International J. on Software Tools for Technology Transfer, vol. 6, no. 4, pp. 260-276, 2004.

[6] E. Pira, V. Rafe, and A. Nikanjam, "Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm," J. of Systems and Software, vol. 131, pp. 181-200, Sept. 2017.

[7] R. Yousefian, V. Rafe, and M. Rahmani, "A heuristic solution for model checking graph transformation systems," Applied Soft Computing, vol. 24, pp. 169-180, Nov. 2014.

[8] E. Alba, F. Chicano, M. Ferreira, and J. Gomez-Pulido, "Finding deadlocks in large concurrent java programs using genetic algorithms," in Proc. of the 10th Annual Conf. on Genetic and Evolutionary Computation, pp. 1735-1742, Atlanta, GA, USA, 12-16 Jul. 2008.

[9] E. Alba and F. Chicano, "Finding safety errors with ACO," in Proc. of the 9th Annual Conf. on Genetic and Evolutionary Computation, pp. 1066-1073, London, England, 7-11 Jul. 2008.

[10] F. Chicano, M. Ferreira, and E. Alba, "Comparing metaheuristic algorithms for error detection in java programs," in Proc. Int. Symp. on Search Based Software Engineering, pp. 82-96, Szeged, Hungary, 10-12 Sept. 2011.

[11] V. Rafe, M. Moradi, R. Yousefian, and A. Nikanjam, "A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations," Applied Soft Computing, vol. 33, pp. 136-149, Aug. 2015.

[12] M. Ferreira, F. Chicano, E. Alba, and J. Gomez-Pulido, "Detecting protocol errors using particle swarm optimization with java pathfinder," in Proc. of the High Performance Computing & Simulation Conf., pp. 319-325, Nicosia, Cyprus, 3-6 Jun. 2008.

[13] H. Kastenberg and A. Rensink, "Model checking dynamic states in GROOVE," in Proc. Int. SPIN Workshop on Model Checking of Software, pp. 299-305, Vienna, Austria, 30 Mar.-1 Apr. 2006.

[14] G. Rozenberg, Handbook of Graph Grammars and Computing by Graph Transformation, World Scientific, 1997.

[15] P. E. Hart, N. J. Nilsson, and B. Raphael, "A formal basis for the heuristic determination of minimum cost paths," IEEE Trans. on Systems Science and Cybernetics, vol. 4, no. 2, pp. 100-107, Jul. 1968.

[16] R. L. Haupt and S. E. Haupt, Practical Genetic Algorithms, John Wiley & Sons, 2004.

[17] J. Kennedy and R. Eberhart, "Particle swarm optimization," in Proc. IEEE Int Conf. on Neural Networks, , vol. 4, pp. 1942-1948, Perth, Australia, 27 Nov.-1 Dec. 1995.

[18] P. Larranaga and J. A. Lozano, Estimation of Distribution Algorithms: A New Tool for Evolutionary Computation, Springer Science & Business Media, 2001.

[19] J. Pearl, Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference, Morgan Kaufmann, 1988.

[20] A. Schmidt, "Model checking of visual modeling languages," in Proc. Conf. of PhD Students in Computer Science, p. 102, 2004.

[21] J. F. Groote and J. V. D. Pol, "A bounded retransmission protocol for large data packets," in Proc. Int. Conf. on Algebraic Methodology and Software Technology, pp. 536-550, Munich, Germany, 1-5 Jul. 1996.

[22] E. Pira, V. Rafe, and A. Nikanjam, "Searching for violation of safety and liveness properties using knowledge discovery in complex systems specified through graph transformations," Information and Software Technology, vol. 97, pp. 110-134, May 2018.

عینالله پیرا در سال 1379 مدرك كارشناسي مهندسي کامپیوتر خود را از دانشگاه خوارزمی، در سال 1381 مدرك كارشناسي ارشد را از دانشگاه صنعتی شریف و در سال 1396 مدرک دکتری را از دانشگاه اراک دريافت نمود. دكتر پیرا از سال 1397 در دانشكده فناوری اطلاعات و مهندسي كامپيوتر دانشگاه شهیدمدنی آذربایجان در تبریز مشغول به فعاليت گرديد و اينك نيز عضو هيأت علمي اين دانشكده مي‎باشد. زمينه‎هاي علمي مورد علاقه نامبرده شامل موضوعاتي مانند مدلسازی و وارسی رسمی نرمافزار، محاسبات تکاملی، دادهکاوی و یادگیری ماشین مي‎باشد.

شارک

عنوان URL للمقالة

یک هیوریستیک جدید برای تشخیص بن بست در تحلیل ایمنی سیستم های نرم افزاری

رایمگ

الروابط

المراكز ذات الصلة

دعامة

الصفحات الرسمية