دوره 19، شماره 1 - ( 3-1401 )
جلد 19 شماره 1 صفحات 166-153 |
برگشت به فهرست نسخه ها
Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
partabian J, rafe V, parvin H, nejatian S, bagherifard K. Reachability checking in complex and concurrent software systems using intelligent search methods. JSDP 2022; 19 (1) : 12
URL: http://jsdp.rcisp.ac.ir/article-1-1075-fa.html
URL: http://jsdp.rcisp.ac.ir/article-1-1075-fa.html
پرتابیان جعفر، رافع وحید، پروین حمید، نجاتیان صمد، باقری‌فرد کرم‌اله. وارسی ویژگی دسترس‌پذیری در سامانه‌های نرم‌افزاری پیچیده و هم‌روند با استفاده از الگوریتم‌های جستجوی هوشمند. پردازش علائم و داده‌ها. 1401; 19 (1) :153-166
دانشگاه اراک
چکیده: (1312 مشاهده)
روش وارسی مدل، روشی رسمی و مؤثر جهت تأیید سامانه‌های نرم‌افزاری است که با تولید و بررسی همه حالتهایِ ممکنِ مدلی از سامانه نرم‌افزار به تحلیل آن می‌پردازد. در سامانه‌های ایمنی– بحرانی، نمیتوان ریسک بروز خطا را حتی در فرآیند تست پذیرفت و لذا لازم است فرآیند درستی‌یابی، قبل از پیاده‌سازی و در سطح مدل انجام شود. استفاده از این روش به‌منظور بررسی خواصی مانند ایمنی ایجاب می‌کند که تمام حالت‌های قابل دسترس (تمام فضای حالت) تولید و سپس فضای حالت سامانه مورد نظر به‌صورت دقیق بررسی شوند. چالش اساسی روش وارسی مدل در سامانه‌های بزرگ و پیچیده که دارای فضای حالت گسترده و نامحدود هستند، مشکل انفجار فضای حالت (کمبود حافظه در تولید همه حالت‌های ممکن) است. سامانه‌های تبدیل گراف، از پرکاربردترین سامانه‌های مدل‌سازی رسمی و راه‌کاری مناسب به‌منظور مدل‌سازی و وارسی سامانه‌های پیچیده هستند. در سامانه‌هایی که تأیید ویژگی ایمنی غیرممکن است، می‌توان با جستجویِ یک حالت قابل دسترسی که در آن پیکربندی خاصی (به‌عنوان مثال خطا یا رفتار نامطلوب) رخ می‌دهد، ویژگی ایمنی را رد کرد. مطالعات اخیر حاکی از آن است که اکتشاف جزئی و هوشمندانه بخشی از فضای حالت می‌تواند راه حل مناسبی برای مشکل انفجار فضای حالت باشد. هدف این پژوهش، استفاده از الگوریتم جنگل تصادفی در وارسی مدل است که می‌تواند با گزینش تعداد محدودی مسیر امیدبخش مشکل انفجار فضای حالت را برطرف سازد. مسیری امیدبخش است که احتمال رسیدن به یک جواب از طریق این مسیر، بیشتر از بقیه مسیرها باشد. در روش پیشنهادی، ابتدا مدل کوچکی از سامانه با استفاده از زبان رسمی سامانه توصیف گراف (GTS) ایجاد، سپس، از فضای حالت مدل کوچک، مجموعه آموزشی از مسیرهایی که به هدف می‌رسند ایجاد می‌شود. پس‌ازآن، مجموعه آموزشی تولیدشده در اختیار الگوریتم جنگل تصادفی قرار داده می‌شود تا روابط منطقی موجود در آن شناسایی و کشف شوند. در مرحله بعد از دانش به‌دست‌آمده جهت پیمایش هوشمند و غیر کامل فضایِ حالتِ مدلِ بزرگ استفاده می‌شود. رویکرد پیشنهادی برای تأیید ویژگی دسترس‌پذیری و رد ویژگی ایمنی در سامانه‌های بزرگ و پیچیده که ایجاد تمام فضای حالت سامانه ناممکن است، استفاده می‌شود. به منظور ارزیابی رویکرد پیشنهادی، این رویکرد در ابزار GROOVEکه از ابزار متن‌باز برای طراحی و وارسی مدل برای سامانه‌های تبدیل گراف است، اجراشده است. نتایج نشان می‌دهند که روش پیشنهادی ازنظر میانگین زمان اجرا و طول شاهد تولیدشده نسبت به روش‌های مورد مقایسه عملکرد بهتری دارد.
شماره‌ی مقاله: 12
نوع مطالعه: پژوهشي |
موضوع مقاله:
مقالات پردازش داده‌های رقمی
دریافت: 1398/7/5 | پذیرش: 1399/12/11 | انتشار: 1401/4/1 | انتشار الکترونیک: 1401/4/1
دریافت: 1398/7/5 | پذیرش: 1399/12/11 | انتشار: 1401/4/1 | انتشار الکترونیک: 1401/4/1
فهرست منابع
1. [1] H. Zhang, J. Du, L. Cao and G. Zhu, "A full symbolic reachability analysis algorithm of timed automata based on BDD", In Autonomous Decentralized Systems (ISADS), IEEE Twelfth International Symposium, pp. 301-304, 2015. [DOI:10.1109/ISADS.2015.20]
2. [2] A. L. Lafuente, "Symmetry reduction and heuristic search for error detection in model checking", Workshop on Model Checking and Artificial Intelligence, 2003.
3. [3] A. L. Lafuente, S. Edelkamp, and S. Leue, "Partial order reduction in directed model checking", International SPIN Workshop on Model Checking of Software, Springer Berlin Heidelberg, pp. 112-127, 2002. [DOI:10.1007/3-540-46017-9_10]
4. [4] V. Rafe, "Scenario-driven analysis of systems specified through graph transformations", Journal of Visual Languages & Computing, vol. 24, no. 2, pp. 136-145, 2013. [DOI:10.1016/j.jvlc.2012.12.002]
5. [5] A. Rensink and E. Zambon, "Pattern-based graph abstraction in Graph transformations", Springer Berlin Heidelberg, pp 66-80, 2012. [DOI:10.1007/978-3-642-33654-6_5]
6. [6] S. Edelkamp, A. L. Lafuente, and S. Leue, "Protocol verification with heuristic search", AAAI Symposium on Model based Validation of Intelligence, 2001.
7. [7] S. Edelkamp, A. L. Lafuente, and S. Leue, "Directed explicit model checking with HSF-SPIN", Proceedings of the 8th international SPIN workshop on Model checking of software, pp. 57-79,2001. [DOI:10.1007/3-540-45139-0_5]
8. [8] S. Edelkamp and F. Reffel, "OBDDs in heuristic search", Annual Conference on Artificial Intelligence, Springer Berlin Heidelberg, pp. 81-92, 1998. [DOI:10.1007/BFb0095430]
9. [9] J. Maeoka, Y. Tanabe, and F. Ishikawa, "Depth-First Heuristic Search for Software Model Checking", In Computer and Information Science, Springer International Publishing, pp. 75-96, 2016. [DOI:10.1007/978-3-319-23467-0_6]
10. [10] K. Havelund, T. Pressburger, "Model checking JAVA programs using JAVA Path Finder", International Journal on Software Tools for Technology Transfer, vol. 2, pp. 366-381,2000 [DOI:10.1007/s100090050043]
11. [11] H. C. Estler and H. Wehrheim, "Heuristic search-based planning for graph transformation systems", KEPS 2011, pp. 54-66, 2011.
12. [12] E. Snippe, "Using heuristic search to solve planning problems in GROOVE", In 14th Twente Student Conference on IT, University of Twente, 2011.
13. [13] S. Ziegert, "Graph Transformation Planning via Abstraction", arXiv preprint arXiv: 1407.7933. 2014. [DOI:10.4204/EPTCS.159.7]
14. [14] J. W. Elsinga, "On a framework for domain independent heuristics in graph transformation planning", Master's thesis, University of Twente, 2016.
15. [15] P. Godefroid and S. Khurshid, "Exploring very large state spaces using genetic algorithms", International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp. 266-280, 2002. [DOI:10.1007/3-540-46002-0_19]
16. [16] P. Godefroid, "Software Model Checking: The VeriSoft Approach Patrice Godefroid, Formal Methods in System Design". vol.26, pp. 77-101, 2005 [DOI:10.1007/s10703-005-1489-x]
17. [17] R. Yousefian, V. Rafe, M. Rahmani, "a heuristic approach for model checking graph transformation systems", Appl. Soft Compute, Vol. 24, pp. 169-180, 2014 [DOI:10.1016/j.asoc.2014.06.055]
18. [18] X. He, Z. Ma, W. Shao, G. Li, "A meta model for the notation of graphical modeling languages", In Computer Software and Applications Conference, COMPSAC 2007. 31st Annual International, IEEE, vol. 1, pp. 219-224, 2007. [DOI:10.1109/COMPSAC.2007.27]
19. [19] GROOVE, groove.sourceforge.net/groove-index.html
20. [20] R. Yousefian, S. Aboutorabi, and V. Rafe, "A greedy algorithm versus meta heuristic solutions to deadlock detection in Graph Transformation Systems", Journal of Intelligent & Fuzzy Systems, vol. 13, no. 1, pp. 1-13, 2016. [DOI:10.3233/IFS-162127]
21. [21] E. Alba, F. Chicano, M. Ferreira, and J. Gomez-Pulido, "finding deadlocks in large concurrent java programs using genetic algorithms", 10th annual conference on Genetic and evolutionary computation, pp. 1735-1742, 2008. [DOI:10.1145/1389095.1389432]
22. [22] L. M. Duarte, L. Foss, R. Wagner, and T. Heimfarth, "Model Checking the Ant Colony Optimization, Distributed, Parallel and Biologically Inspired Systems IFIP Advances'', Information and Communication Technology, vol. 329, pp. 221-232, 2010 [DOI:10.1007/978-3-642-15234-4_22]
23. [23] B. L. Webster, "solving combinatorial optimization problems using a new algorithm based on gravitational attraction", Florida Institute of Technology, 2004.
24. [24] R. Behjati, M. Sirjani, and M. N. Ahmadabadi, "Bounded Rational Search for On-the-Fly Model Checking of LTL Properties", Fundamentals of Software Engineering, vol. 5961, pp. 292-307, 2010 [DOI:10.1007/978-3-642-11623-0_17]
25. [25] G.J. Holzmann, "On-The-Fly Model Checking", ACM Comput Surv, vol.28(4es), pp.120, 1996 [DOI:10.1145/242224.242379]
26. [26] E. Pira, V. Rafe, A. Nikanjam, "EMCDM: efficient model checking by data mining for verification of complex software systems specified through architectural styles", Appl. Soft Compute, Vol. 44pp, pp.1185-1201, 2016. [DOI:10.1016/j.asoc.2016.06.039]
27. [27] E. Pira, V. Rafe, A. Nikanjam, "Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm", Journal of System and Software, vol. 131, pp. 181-200, 2017 [DOI:10.1016/j.jss.2017.05.128]
28. [28] J. Partabian, V. Rafe, H. Parvin, S. Nejatian, "An Approach Based on Knowledge Exploration for State Space Management in Checking Reachability of Complex Software Systems", soft computing, vol. 24, pp.1-16, 2019. [DOI:10.1007/s00500-019-04334-3]
29. [29] M. Yasrebi, V. Rafe, H. Parvin, S. Nejatian, "An efficient approach to state space management in model checking of complex software system using machine learning technique", journal of intelligent & Fuzzy system, vol.38, no. 2, pp. 1761-1773, 2020. [DOI:10.3233/JIFS-190023]
30. [30] G. Rozenberg, "Handbook of Graph Grammars and Comp", World scientific, vol. 1, 1997.
31. [31] H. Kastenberg and A. Rensink, "Model Checking Dynamic States in GROOVE", International SPIN Workshop on Model Checking of Software, Springer Berlin Heidelberg, pp. 299-305, 2006. [DOI:10.1007/11691617_19]
32. [32] A. Groce and W. Visser, "Heuristics for model checking Java programs", International Journal on Software Tools for Technology Transfer (STTT), vol. 6, no. 4, pp. 260-276, 2004. [DOI:10.1007/s10009-003-0130-9]
33. [33] S. Edelkamp, A. L. Lafuente, and S. Leue, "Protocol verification with heuristic search", In AAAI Symposium on Model-based Validation of Intelligence, pp. 75-83, 2001.
34. [34] V. Rafe, M. Moradi, R. Yousefian, and A. Nikanjam, "A Meta-Heuristic Approach for Automated Refutation of Complex Software Systems Specified through Graph Transformations", Applied Soft Computing, vol. 33, pp. 136-149, 2015. [DOI:10.1016/j.asoc.2015.04.032]
ارسال پیام به نویسنده مسئول
| بازنشر اطلاعات | |
 |
این مقاله تحت شرایط Creative Commons Attribution-NonCommercial 4.0 International License قابل بازنشر است. |
