یک هیوریستیک جدید برای تشخیص بن بست در تحلیل ایمنی سیستم های نرم افزاری
محورهای موضوعی : مهندسی برق و کامپیوتر
عین الله پیرا
1
(دانشگاه شهید مدنی آذربایجان،دانشكده فناوری اطلاعات و مهندسي كامپيوتر)
کلید واژه: تحلیل ایمنیوارسی مدلبن¬, بست هیوریستیک الگوریتم¬, های تکاملی,
چکیده مقاله :
تحلیل ایمنیِ سیستم های نرم افزاری، خصوصاً از نوع بحرانی-ایمنی، باید بطور دقیق انجام شود چون که وجود حتی یک خطای کوچک در چنین سیستم هایی ممکن است نتایج فاجعه باری داشته باشد ضمناً چنین تحلیلی باید قبل از پیاده سازی یعنی در مرحله طراحی و در سطح مدل انجام شود. وارسی مدل یک روش دقیق و مبتنی بر ریاضی است که ایمنی سیستم های نرم افزاری را با دریافت مدلی از آن و بررسی تمام حالت های قابل دسترس مدل انجام می دهد. با توجه به پیچیدگی بعضی سیستم ها و مدل های آن، وارسی مدل ممکن است با مشکل انفجار فضای حالت مواجه شود. بنابراین، وارسی مدل بجای تایید ایمنی چنین سیستم هایی، آنها را با یافتن خطاهایی از جمله بن بست رد می-کند. اگر چه قبلا هیوریستیکی برای یافتن بن بست در فضای حالت مدل ارائه شده و آن را در چندین الگوریتم جستجوی مکاشفه ای ساده و تکاملی بکار برده اند ولی سرعت تشخیص آن پایین بوده است. در این مقاله، یک هیوریستیک جدید برای یافتن بن بست در فضای حالت مدل ارائه کرده و سرعت تشخیص آن را، با بکار بردن در الگوریتم های جستجوی مکاشفه ای ساده از جمله عمقی تکرار شونده 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.