Checking Reachability Property in Complex Concurrent Software Systems with a Knowledge Discovery Approach

Document Type : English Original Article

Authors

1 Department of Computer Engineering, Lamerd Branch, Islamic Azad University, Lamerd, IRAN.

2 Department of Computer Engineering, Yasooj Branch, Islamic Azad University, Yasooj, Iran

3 Department of Computer Engineering, Faculty of Engineering, Arak University, Arak 38156-8-8349, Iran

4 Department of Computer Engineering, Nourabad Mamasani Branch, Islamic Azad University, Nourabad Mamasani, Iran,

5 Department of Electrical Engineering yasooj Branch, Islamic azad University, Yasooj, Iran.

Abstract

The model checking technique is a formal and effectual way in verification of software systems. By generation and investigation of all model states, it analyses the software systems. The main issue in the model checking of the complicated systems having wide or infinite state space is the lack of memory in generation of all states which is referred to as "state space explosion". The Random Forest algorithm which is capable of knowledge discovery faces the above-cited problem by selecting a few promising paths. In our suggested method, first a small model of the system is developed by the formal language of graph transformation system (GTS). A training data set is created from the small state space. The generated training data set is made available to the Random Forest algorithm to detect and discover the logical relationships existent in it. Then, the knowledge acquired in this way is used in the smart and incomplete exploration of the large state space. The proposed approach is run in GROOVE which is an open source tool for designing and studying the model of graph transformation systems. The results indicate that the suggested method in accordance with the two criteria (average running time and the number of explored states) performs better compared with the other approaches.

Keywords

References

[1] Groce, A., et al., Heuristics for model checking Java programs. International Journal on Software Tools for Technology Transfer, 2004. 6(4): p. 260-276.
[2] Pira, E., et al., Using evolutionary algorithms for reachability analysis of complex software systems specified through graph transformation. Reliability Engineering & System Safety, 2019. 191: p. 106577.
[3] Yousefian, R., et al., A heuristic solution for model checking graph transformation systems. Applied Soft Computing, 2014. 24: p. 169-180.
[4] Rafe, V., et al., A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations. Applied Soft Computing, 2015. 33: p. 136-149.
[5] Partabian, J., et al., An approach based on knowledge exploration for state space management in checking reachability of complex software systems. Soft Computing, 2020. 24(10): p. 7181-7196.
[6] Zhang, H., et al. A full symbolic reachability analysis algorithm of timed automata based on BDD. in 2015 IEEE Twelfth International Symposium on Autonomous Decentralized Systems. 2015. IEEE.
[7] Lluch-Lafuente, A., Symmetry reduction and heuristic search for error detection in model checking. 2003.
[8] Lluch-Lafuente, A., et al. Partial order reduction in directed model checking. in International SPIN Workshop on Model Checking of Software. 2002. Springer.
[9] Rafe, V., Scenario-driven analysis of systems specified through graph transformations. Journal of Visual Languages & Computing, 2013. 24(2): p. 136-145.
[10] Rensink, A., et al. Pattern-based graph abstraction. in International Conference on Graph Transformation. 2012. Springer.
[11] Alba, E., et al. Finding safety errors with ACO. in Proceedings of the 9th annual conference on Genetic and evolutionary computation. 2007.
[12] Edelkamp, S., et al., Protocol verification with heuristic search. 2001: Bibliothek der Universität Konstanz.
[13] Pira, E., et al., Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm. Journal of Systems and Software, 2017. 131: p. 181-200.
[14] Pira, E., et al., EMCDM: Efficient model checking by data mining for verification of complex software systems specified through architectural styles. Applied Soft Computing, 2016. 49: p. 1185-1201.
[15] Yasrebi, M., et al., An efficient approach to state space management in model checking of complex software systems using machine learning techniques. Journal of Intelligent & Fuzzy Systems, 2020. 38(2): p. 1761-1773.
[16] Edelkamp, S., et al. OBDDs in heuristic search. in Annual Conference on Artificial Intelligence. 1998. Springer.
[17] Maeoka, J., et al., Depth-first heuristic search for software model checking, in Computer and Information Science 2015. 2016, Springer. p. 75-96.
[18] Estler, H.-C., et al. Heuristic search-based planning for graph transformation systems. in ICAPS workshop on knowledge engineering for planning and scheduling (KEPS 2011). 2011.
[19] Snippe, E. Using heuristic search to solve planning problems in GROOVE. in 14th Twente Student Conference on IT, University of Twente. Available at fmt. cs. utwente. nl/education/bachelor/73. 2011.
[20] Ziegert, S., Graph transformation planning via abstraction. arXiv preprint arXiv:1407.7933, 2014.
[21] Elsinga, J.W., On a framework for domain independent heuristics in graph transformation planning. 2016, University of Twente.
[22] Godefroid, P., et al., Exploring very large state spaces using genetic algorithms. International Journal on Software Tools for Technology Transfer, 2004. 6(2): p. 117-127.
[23] He, X., et al. A metamodel for the notation of graphical modeling languages. in 31st Annual International Computer Software and Applications Conference (COMPSAC 2007). 2007. IEEE.
[24] Yousefian, R., et al., A greedy algorithm versus metaheuristic solutions to deadlock detection in Graph Transformation Systems. Journal of Intelligent & Fuzzy Systems, 2016. 31(1): p. 137-149.
[25] Alba, E., et al. Finding deadlocks in large concurrent java programs using genetic algorithms. in Proceedings of the 10th annual conference on Genetic and evolutionary computation. 2008.
[26] Duarte, L.M., et al., Model checking the ant colony optimisation, in Distributed, parallel and biologically inspired systems. 2010, Springer. p. 221-232.
[27] Webster, B.L., Solving combinatorial optimization problems using a new algorithm based on gravitational attraction. 2004: Florida Institute of Technology.
[28] Behjati, R., et al. Bounded rational search for on-the-fly model checking of LTL properties. in International Conference on Fundamentals of Software Engineering. 2009. Springer.
[29] Pira, E., Using Markov Chain based Estimation of Distribution Algorithm for Model-based Safety Analysis of Graph Transformation. Journal of Computer Science and Technology, 2021. 36(4): p. 839-855.
[30] Pira, E., Using knowledge discovery to propose a two-phase model checking for safety analysis of graph transformations. Software Quality Journal, 2021: p. 1-28.
[31] Rezaee, N., et al., A hybrid meta-heuristic approach to cope with state space explosion in model checking technique for deadlock freeness. Journal of AI and Data Mining, 2020. 8(2): p. 189-199.
[32] Salimi, N., et al., Fuzzy particle swarm optimization algorithm (NFPSO) for reachability analysis of complex software systems. 2020.
[33] Edelkamp, S., et al., Directed explicit-state model checking in the validation of communication protocols. International journal on software tools for technology transfer, 2004. 5(2): p. 247-267.
[34] Schmidt, Á. Model checking of visual modeling languages. in CONFERENCE OF PHD STUDENTS IN COMPUTER SCIENCE. 2004.
[35] Hendrik Hausmann, J., Dynamic Meta Modeling: A Semantics Description Technique for Visual Modeling Languages. 2005.
Journal of Soft Computing and Information Technology
Volume 12, Issue 1 - Serial Number 39
Spring
May 2023
Pages 41-51

Files

Share

How to cite

Statistics