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

اشتراک گذاری

آدرس مقاله


کد مقاله : 14000219273356 بازدید : 4741 صفحه: 73 - 79

20.1001.1.16823745.1401.20.1.8.2

نوع مقاله: پژوهشی

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

محورهای موضوعی : مهندسی برق و کامپیوتر

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

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

تاریخ دریافت : 1400/02/19 تاریخ پذیرش : 1400/10/25 تاریخ انتشار : 1401/03/30

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

چکیده مقاله :

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

چکیده انگلیسی:

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

مقاله پژوهشی

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

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

 

 

1 

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

 

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

1-       مقدمه

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

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

img0 

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

 

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

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

2-       پیش‌زمینه

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

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

2-2 وارسی مدل

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

img0   img0

                        (الف)                                               (ب)

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

 

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

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

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

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

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

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

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

img0        (1)

img0        (2)

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

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

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

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

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

img0        (3)

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

img0        (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) و حداکثر عمق جستجو یا همان طول کروموزوم‌ها img0 بسته به نوع مسأله و اندازه مدل دارای مقادیر متغیری می‌باشند. جدول 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

img0 

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

 

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

 

100

حداکثر تعداد تکرار هر الگوریتم

جستجوی پرتو (BS)

الگوریتم بهینه‌سازی بیزی (BOA)

عرض پرتوimg010

مسایل غذاخوری فیلسوفان و چرخه حیات پردازه

4/0

نرخ انتخاب (selecton rate)

عرض پرتوimg020

پروتکل انتقال مجدد به تعداد محدود

5/0

نرخ جایگزینی (replacement rate)

الگوریتم بهینه‌سازی ازدحام ذرات (PSO)

الگوریتم ژنتیک (GA)

2

img0 

6/0

نرخ ترکیب (crossover rate)

8/0

img0 

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% حالت بن‌بست را پیدا کرده تا امکان مقایسه سرعت تشخیص این هیوریستیک‌ها فراهم شود.

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

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

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

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

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

 

img0 

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

 

img0 

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

 

img0 

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

 

 

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

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

img0 

شکل 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 در دانشكده فناوری اطلاعات و مهندسي كامپيوتر دانشگاه شهیدمدنی آذربایجان در تبریز مشغول به فعاليت گرديد و اينك نيز عضو هيأت علمي اين دانشكده مي‎باشد. زمينه‎هاي علمي مورد علاقه نام­برده شامل موضوعاتي مانند مدل­سازی و وارسی رسمی نرم­افزار، محاسبات تکاملی، داده­کاوی و یادگیری ماشین مي‎باشد.

 

 

 


رایمگ

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

پیوندهای سایت

مراکز مرتبط

پشتیبانی

صفحات رسمی

حقوق این وب‌سایت متعلق به سامانه مدیریت نشریات رایمگ است.
حق نشر © 1403-1396

صفحه اصلی| عضویت/ ورود| درباره رایمگ| تماس با ما|
[English] [العربية] [en] [ar]