A New Heuristic for Deadlock Detection in Safety Analysis of Software Systems
Subject Areas : electrical and computer engineering
1 -
Keywords: Safety analysis, model checking, deadlock, heuristic, evolutionary algorithms,
Abstract :
The safety analysis of software systems, especially safety-critical ones, should be performed exactly because even a minor failure in these systems may result in disaster consequences. Also, such analysis must be done before implementation, i.e. the design step and in the model level. Model checking is an exact and mathematical-based way that gets a model of a system and analyzes it through exploring all reachable states of the model. Due to the complexity of some systems and their models, this way may face the state space explosion problem, i.e. it cannot explore all available states. A solution to solve this problem in these systems is that model checking tries to refute them, instead of verifying them, by finding errors such as deadlock (if available).Although, a heuristic has been previously proposed to find a deadlock in the model's state space and it has been applied in several simple heuristic search and evolutionary algorithms, its detection speed has been low. In this paper, we propose a novel heuristic to detect a deadlock in the model's state space, and test and compare its detection speed by applying it in several simple heuristic search algorithms such as iterative deepening A*, beam search, and evolutionary algorithms such as genetic, particle swarm optimization, and Bayesian optimization. Comparison results confirm that the new heuristic can detect a deadlock in less time than the previous heuristic.
[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.
نشریه مهندسی برق و مهندسی كامپیوتر ایران، ب- مهندسی کامپیوتر، سال 20، شماره 1، بهار 1401 73
مقاله پژوهشی
یک هیوریستیک جدید برای تشخیص بنبست
در تحلیل ایمنی سیستمهای نرمافزاری
عینالله پیرا
چكیده: تحلیل ایمنی سیستمهای نرمافزاری، خصوصاً از نوع بحرانی- ایمنی، باید به طور دقیق انجام شود زیرا وجود حتی یک خطای کوچک در چنین سیستمهایی ممکن است نتایج فاجعهباری داشته باشد. ضمناً چنین تحلیلی باید قبل از پیادهسازی یعنی در مرحله طراحی و در سطح مدل انجام شود. وارسی مدل، یک روش دقیق و مبتنی بر ریاضی است که ایمنی سیستمهای نرمافزاری را با دریافت مدلی از آن و بررسی تمام حالتهای قابل دسترس مدل انجام میدهد. با توجه به پیچیدگی بعضی سیستمها و مدلهای آن، وارسی مدل ممکن است با مشکل انفجار فضای حالت مواجه شود، یعنی نتواند تمام حالتهای قابل دسترس را پیمایش کند. یک راه حل برای حل مشکل انفجار فضای حالت در چنین سیستمهایی این است که به جای تأیید ایمنی، وارسی مدل سعی میکند آنها را با یافتن خطاهایی از جمله بنبست (در صورت موجود) رد کند. اگرچه قبلاً هیوریستیکی برای یافتن بنبست در فضای حالت مدل ارائه شده و آن را در چندین الگوریتم جستجوی مکاشفهای ساده و تکاملی به کار بردهاند ولی سرعت تشخیص آن پایین بوده است. این مقاله، یک هیوریستیک جدید برای یافتن بنبست در فضای حالت مدل ارائه میکند و سرعت تشخیص آن با به کار بردن در الگوریتمهای جستجوی مکاشفهای ساده از جمله عمقی تکرارشونده A* و جستجوی پرتو و الگوریتمهای تکاملی مختلف از جمله ژنتیک، بهینهسازی ازدحام ذرات و بهینهسازی بیزی با روش قبلی مقایسه میشود. مقایسه نتایج تجربی تأیید میکنند که هیوریستیک جدید میتواند حالت بنبست را در زمان کمتری نسبت به هیوریستیک قبلی پیدا کند.
کلیدواژه: الگوریتمهای تکاملی، بنبست، تحلیل ایمنی، وارسی مدل، هیوریستیک.
1- مقدمه
سیستمهای نرمافزاری مدرن شامل زیرسیستمهایی میباشند که در بعضی شرایط مجبور هستند به منابع سیستم به طور همروند و مشترک دسترسی پیدا کنند و این ممکن است باعث ایجاد حالت بنبست2 شود. کشف و رفع حالتهای خطا (برای مثال بنبست) یا به عبارت کلیتر، تحلیل ایمنی سیستمهای نرمافزاری، خصوصاً از نوع بحرانی- ایمنی3، باید به طور دقیق و قبل از پیادهسازی یعنی در مرحله طراحی و در سطح مدل انجام شود. مجموعهای از روشهای رسمی4 مبتنی بر تحلیلهای دقیق ریاضی وجود دارند که صحت مدل را با توجه به ویژگیهای مورد انتظار بررسی میکنند. وارسی مدل5 یک روش رسمی است که مدلی از سیستم به همراه ویژگیهای توصیفشده در قالب فرمولهای منطق زمانی6 را دریافت کرده و درستی/ نادرستی ویژگیها را با کاوش همه حالتهای قابل دسترسِ (فضای حالت) مدل بررسی میکند [1]. با توجه به پیچیدگی بعضی سیستمها و مدلهای آن، وارسی مدل ممکن است با مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالتهای ممکن) مواجه شود. یک راه حل برای حل مشکل انفجار فضای حالت در چنین سیستمهایی این است که وارسی مدل سعی میکند آنها را با یافتن خطاهایی از جمله بنبست (در صورت موجود) رد کند. به این مفهوم که به جای اثبات عدم وجود خطا، دنبال خطا میگردد. لازم به ذکر است که اگر وارسی مدل در چنین حالتی نتواند خطایی پیدا را کند، نمیتوان ادعا کرد که سیستم بدون خطا است زیرا فقط قسمتی از فضای حالت پیمایش شده است [2]. البته میتوان با روشهای احتمالی از جمله مونتکارلو تخمین معناداری را از میزان صحت سیستم ارائه کرد [3].
فضای حالت مدل معمولاً با یک گراف نمایش داده میشود که در آن، رئوس و یالها به ترتیب مجموعه حالتها و گذارهای مابین آنها را نشان میدهند. در فضای حالت مدل، بنبست، حالتی را نشان میدهد که هیچ گذار خروجی ندارد که به چنین حالتی، حالت نهایی نیز میگویند. به عبارت دیگر، چنین گرهی در گراف معادل، یال خروجی ندارد. بعد از عمل وارسی، وارسیگر یک مثال نقض7 تولید میکند. یک مثال نقض نشاندهنده مسیری از حالتها (گرهها) و گذارهای (یالهای) مابین آنها است به طوری که این مسیر از حالت (گره) ابتدایی شروع شده و به یک حالت (گره) بنبست ختم میشود. یافتن چنین مسیری نیز ممکن است باعث بروز مشکل انفجار فضای حالت شود. در [4] هیوریستیکی برای یافتن بنبست در فضای حالت مدل ارائه شده است. این هیوریستیک مسیری را دریافت کرده و مجموع تعداد گذارهای خروجی گرههای موجود در مسیر مورد نظر را برمیگرداند. واضح است که هرچه مقدار هیوریستیک برای مسیری کمتر باشد، احتمال به بنبست رسیدن آن بالا خواهد بود. برای تست این هیوریستیک، آن را در الگوریتمهای جستجوی عمقی 8(DFS) و ردیفی 9(BFS) [5]، جستجوی مکاشفهای ساده از جمله A* [5]، عمقی تکرارشونده A* (IDA*) و جستجوی پرتو 10(BS)
شکل 1: جزئیات مدل طراحیشده برای مسأله غذاخوری فیلسوفان با 2 فیلسوف [6].
[6] و الگوریتمهای تکاملی مختلف از جمله ژنتیک 11(GA) [4]، [7] و [8]، بهینهسازی کلونی مورچگان 12(ACO) [9]، شبیهسازی ذوب فلزات 13(SA) [10]، بهینهسازی ازدحام ذرات 14(PSO) [11] و [12] و بهینهسازی بیزی 15(BOA) [6] به کار بردهاند. اگرچه این الگوریتمها میتوانند حالت بنبست را با موفقیت تشخیص دهند ولی سرعت تشخیص میتواند بهبود پیدا کند.
در این مقاله، یک هیوریستیک جدید برای یافتن بنبست در فضای حالت مدل ارائه میکنیم. این هیوریستیک به هر مسیری که تعداد گذارهای خروجی گرههای موجود در آن تقریباً نزولی باشد، عدد کمتری
را اختصاص میدهد. در واقع به جای مجموع تعداد گذارهای خروجی گرههای موجود، مجموع حاصلضرب اختلاف تعداد گذارهای گرههای پشت سر هم 
و 
در موقعیت گره 
یعنی 
را به عنوان مقدار برازندگی برای آن مسیر در نظر میگیرد. هرچه این مقدار برای مسیری کمتر باشد (یعنی تعداد گذارهای خروجی گرههای موجود در آن تقریباً نزولی باشد)، احتمال رسیدن آن مسیر به بنبست بیشتر خواهد بود. برای تست هیوریستیک جدید، آن را در الگوریتمهای مختلف استفاده کرده و این الگوریتمها را در ابزار GROOVE [13] پیادهسازی میکنیم. سپس با اجرای این الگوریتمها روی چندین مسأله شناختهشده، سرعت تشخیص آن را با هیوریستیک قبلی مقایسه میکنیم. قابل ذکر است که ابزار GROOVE، مدلهای توصیفشده با زبان رسمی تبدیل گراف [14] را میپذیرد و در نتیجه مسایل در نظر گرفته شده نیز باید با این زبان رسمی توصیف شوند.
2- پیشزمینه
2-1 زبان رسمی تبدیل گراف
این زبان از گرافها و تبدیلات مابین آنها جهت مدلسازی حالتها و رفتارهای یک سیستم بهره میبرد [14]. مدلهایی که با این زبان توصیف میشوند دارای سه جزء گراف نوع 
، گراف میزبان 
و مجموعه قوانین تبدیل 
است. گراف شامل مجموعهای از نوعهای گره16 و مجموعهای از نوعهای یال17 است و گرهها و یالهای مجاز را نشان میدهد که میتوانند در طی تبدیلات گراف وجود داشته باشند. گراف حالت اولیه (آغازین) سیستم را نشان میدهد و بدیهی است که گرهها و یالهای آن باید جزء نوعهای گره و نوعهای یال موجود در گراف باشند. مجموعه قوانین تبدیلی را نشان میدهد که حالات مختلف سیستم را میتوانند تولید کنند. هر قانون تبدیل 
به صورت سهتایی 
تعریف میشود که در آن، گراف 
شرایطی را مشخص میکند که باید گراف مربوط به حالت فعلی داشته باشد تا این قانون بتواند روی این حالت اِعمال شود. گراف 
نیز شرایطی را تعیین میکند که باید گراف مربوط به حالت حاصل بعد از اِعمال قانون داشته باشد. گراف 
نیز محدودیتهایی را مشخص میکند که نباید در گراف مربوط به حالت فعلی باشند تا این قانون بتواند اِعمال شود. شکل 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 به همراه مسایل استفادهشده روی وب قابل دسترس است18.
مسأله غذاخوری فیلسوفان (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: مقادیر مناسب برای پارامترهای ثابت الگوریتمها.
حداکثر تعداد تکرار هر الگوریتم | |||
جستجوی پرتو (BS) | الگوریتم بهینهسازی بیزی (BOA) | ||
عرض پرتو | مسایل غذاخوری فیلسوفان و چرخه حیات پردازه | 4/0 | نرخ انتخاب (selecton rate) |
عرض پرتو | 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 فرایند و | چرخه حیات پردازه |
280 | 40 | 30 فرایند و | |
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 در دانشكده فناوری اطلاعات و مهندسي كامپيوتر دانشگاه شهیدمدنی آذربایجان در تبریز مشغول به فعاليت گرديد و اينك نيز عضو هيأت علمي اين دانشكده ميباشد. زمينههاي علمي مورد علاقه نامبرده شامل موضوعاتي مانند مدلسازی و وارسی رسمی نرمافزار، محاسبات تکاملی، دادهکاوی و یادگیری ماشین ميباشد.