Volume 19, Issue 1 (5-2022)                   JSDP 2022, 19(1): 153-166 | Back to browse issues page

XML Persian Abstract Print


Download citation:
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) :153-166
URL: http://jsdp.rcisp.ac.ir/article-1-1075-en.html
arak university
Abstract:   (306 Views)
The model checking technique is a formal and effective method for verifying software systems, which analyses it via generating and examining all possible states of a model of the software system. In safety-critical systems, one could not admit the risk of error even in the testing process, therefore it is necessary to carry out the verification process before implementation and at the model level. Using this technique to evaluate properties such as security entails all available states (all state space) being generated, then the state space of the system in question be carefully examined. The main challenge of the model checking technique in large and complex systems with wide or infinite state space is the problem of state space explosion (lack of memory in the generation of all possible states). Graph transformation systems are one of the most widely used formal modeling systems and a suitable solution for modeling and checking complex systems. In systems where security property verification is not possible, the security feature can be refuted by searching for an accessible mode in which a specific configuration (e.g. error or undesirable behavior) occurs. Recent studies advocate that partial and intelligent exploration of part of the state space could be a good solution to the problem of state space explosion. The goal of this study is to use the random forest algorithm in the model checking which can solve the problem of state space explosion by selecting a few promising paths. A path is hopeful whenever the probability of reaching an answer through this path is higher than other paths. In the proposed method, a small model of the system is first created using the official language of the Graph Description System (GTS). Afterwards, a training data set of paths to the goal is generated from the small model mode space. The generated training data set is then provided to the random forest algorithm to identify and discover the logical relationships within it. In the next stage, the acquired knowledge is used to intelligently explore the incomplete space of the large model state. The proposed approach is used in the verification of the reachability property and to refute the safety feature in large and complex systems where it is impossible to generate the entire system state space. In order to evaluate the proposed approach, it has been implemented in GROOVE which is an open source tool for designing and checking models in graph conversion systems. The results indicate that the proposed method performs better than the compared methods in terms of average running time and the length of the generated witness.
Article number: 12
Full-Text [PDF 1156 kb]   (98 Downloads)    
Type of Study: Research | Subject: Paper
Received: 2019/09/27 | Accepted: 2021/03/1 | Published: 2022/06/22 | ePublished: 2022/06/22

References
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]

Add your comments about this article : Your username or Email:
CAPTCHA

Send email to the article author


Rights and permissions
Creative Commons License This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.

© 2015 All Rights Reserved | Signal and Data Processing