Abstract
Model checking is one of the most efficient techniques in software system verification. However, state space explosion is a big challenge while using this technique to check different properties like safety ones. In this situation, one can search the state space to find a reachable state in which the safety property is violated. Hence, reachability checking can be done instead of checking safety property. However, checking reachability in the worst case may cause state space explosion again. To handle this problem, our idea is based on generating a small model consistent with the main model. Then by exploring the state space entirely, we search it to find the goal states. After finding the goal states, we label the paths which start from the initial state and leading to a goal state. Then using the ensemble classification technique, the necessary knowledge is extracted from these paths to intelligently explore the state space of the bigger model. Ensemble machine learning technique uses Boosting method along with decision trees. It follows sampling techniques by replacement. This method generates k predictive models after sampling k times. Finally, it uses a voting mechanism to predict the labels of the final path. Our proposed approach is implemented in GROOVE, which is an open source toolset for designing and model checking graph transformation systems. Our experiments show a significant improvement in terms of both speed and memory usage. In average, our approach consumes nearly 42% fewer memory than other approaches. Also, it generates witnesses nearly 20% shorter than others, in average.
Similar content being viewed by others
References
Alba E, Chicano F (2007) Finding safety errors with ACO. In: Proceedings of the 9th annual conference on genetic and evolutionary computation. ACM, pp. 1066–1073
Alba E, Chicano F, Ferreira M, Gomez-Pulido J (2008) Finding deadlocks in large concurrent java programs using genetic algorithms. In: 10th annual conference on genetic and evolutionary computation, pp 1735–1742
Allen R, Garlan D (1997) A formal basis for architectural connection. ACM Trans Softw Eng Methodol (TOSEM) 6(3):213–249
Alpaydin E (2011) Introduction to machine learning, 2nd edn. MIT Press, Cambridge
Arcuri A, Briand L (2011) A practical guide for using statistical tests to assess randomized algorithms in software engineering. In: 33rd international conference software engineering (ICSE). IEEE, pp 1–10
Behjati R, Sirjani M, Ahmadabadi MN (2010) Bounded rational search for on-the-fly model checking of LTL properties. Fundam Softw Eng 5961:292–307
Boneva I, Kreiker J, Kurban M, Rensink A, Zambon E (2012) Graph abstraction and abstract graph transformation (amended version). Technical Report TR-CTIT-12-26, University of Twente, October 2012
Castro SJB, Crespo RG, García VHM (2011) Patterns of software development process. Int J Interact Multimed Artif Intell 1(4):33–40
Clarke EM, McMillan KL, Campos SVA, Hartonas-Garmhausen VI (1996) Symbolic model checking. Comput Aided Verif 1102:419–422
Duarte LM, Foss L, Wagner R, Heimfarth T (2010) Model checking the ant colony optimization. In: Distributed, parallel and biologically inspired systems. IFIP advances in information and communication technology, vol 329, pp 221–232
Edelkamp S, Reffel F (1998) OBDDs in heuristic search. In: Annual conference on artificial intelligence. Springer, Berlin, pp 81–92
Edelkamp S, Lafuente AL, Leue S (2001) Protocol verification with heuristic search. In: AAAI symposium on model based validation of intelligence
Edelkamp S, Lafuente AL, Leue S (2001) Protocol verification with heuristic search. In: AAAI symposium on model-based validation of intelligence, pp 75–83
Edelkamp S, Leue S, Lafuente AL (2004) Directed explicit-state model checking in the validation of communication protocols. Int J Softw Tools Technol Transf (STTT) 5(2–3):247–267
Elsinga JW (2016) On a framework for domain independent heuristics in graph transformation planning. Master’s thesis, University of Twente
Engels G, Hausmann JH, Heckel R, Sauer S (2000) Dynamic meta modeling: a graphical approach to the operational semantics of behavioral diagrams in UML. In: 3rd international conference on the unified modeling language: advancing the standard (UML’00). Springer, pp. 323–337
Estler HC, Wehrheim H (2011) Heuristic search-based planning for graph transformation systems. In: KEPS 2011, p 54
Francesca G, Santone A, Vaglini G, Villani ML (2011) Ant colony optimization for deadlock detection in concurrent systems. IEEE Computer Society, pp 108–117
Garlan D, Allen R, Ockerbloom J (1994) Exploiting style in architectural design environments. In ACM SIGSOFT software engineering notes, vol 19, no 5. ACM, pp 175–188
Godefroid P, Khurshid S (2002) Exploring very large state spaces using genetic algorithms. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 266–280
Groce A, Visser W (2004) Heuristics for model checking Java programs. Int J Softw Tools Technol Transf (STTT) 6(4):260–276
Gyuris V, Sistla A (1999) On-the-fly model checking under fairness that exploits symmetry. Form Methods Syst Des 15:217–238
Habiboghli A, Jalali T (2016) A solution to the N-queens problem using biogeography-based optimization. Int J Interact Multimed Artif Intell 4(4):20–26
He X, Ma Z, Shao W, Li G (2007) A meta model for the notation of graphical modeling languages. In: 31st annual international computer software and applications conference, COMPSAC 2007, vol 1. IEEE, pp 219–224
Heckel R (2006) Graph transformation in a Nutshell. Electron Notes Theor Comput Sci (ENTCS) 148:187–198
Heckel R, Baresi L (2002) Tutorial introduction to graph transformation: a software engineering perspective. In: First international conference on graph transformation (ICGT), pp 402–429
i Casas PF, Pi X, Casanovas J, Jové J (2013) Definition of virtual reality simulation models using specification and description language diagrams. In: International SDL Forum. Springer, Berlin, pp 258–274
Kastenberg H, Rensink A (2006) Model checking dynamic states in GROOVE. In: Of the 13th international conference on model checking software. Springer-Verlag, Berlin, pp 299–305
Khari M, Kumar P, Burgos D, Crespo RG (2018) Optimized test suites for automated testing using different optimization techniques. Soft Comput 22(24):8341–8352
Lafuente AL (2003) Symmetry reduction and heuristic search for error detection in model checking. In: Workshop on model checking and artificial intelligence
Maeoka J, Tanabe Y, Ishikawa F (2016) Depth-first heuristic search for software model checking. In: Lee R (ed) Computer and information science. Springer, Berlin, pp 75–96
Meza J, Espitia H, Montenegro C, Crespo RG (2016) Statistical analysis of a multi-objective optimization algorithm based on a model of particles with vorticity behavior. Soft Comput 20(9):3521–3536
Peng H, Tahar S (1998) A survey on compositional verification. J Circuits Syst Comput 8:16–25
Pira E, Rafe V, Nikanjam A (2016) EMCDM: efficient model checking by data mining for verification of complex software systems specified through architectural styles. Appl Soft Comput 44:1185–1201
Pira E, Rafe V, Nikanjam A (2017) Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm. J Syst Softw 131:181–200
Rafe V (2013) Scenario-driven analysis of systems specified through graph transformations. J Vis Lang Comput 24(2):136–145
Rafe V, Moradi M, Yousefian R, Nikanjam A (2015) a meta-heuristic approach for automated refutation of complex software systems specified through graph transformations. Appl Soft Comput 33:136–149
Rahmani AT, Rafe V (2009) Towards automated software model checking using graph transformation systems and Bogor. Zhejiang Univ Sci A 10:1093–1105
Rensink A, Zambon E (2012) Pattern-based graph abstraction in graph transformations. Springer, Berlin, pp 66–80
Rozenberg G (1997) Handbook of graph grammars and computing by graph transformation, vol 1. World Scientific, Singapore
Seni G, Elder JF (2010) Ensemble methods in data mining: improving accuracy through combining prediction. Morgan and Claypool, San Rafael
Serengil SI, Ozpinar A (2018) Workforce optimization for bank operation centers: a machine learning approach. Int J Interact Multimed Artif Intell 4(6):81–87
Snippe E (2011) Using heuristic search to solve planning problems in GROOVE. In: 14th Twente student conference on IT, University of Twente
Theodoridis S, Koutroumbas K (2008) Pattern recognition, 4th edn. Academic Press, Cambridge
Thöne S (2005) Dynamic software architectures: a style based modeling and refinement technique with graph transformations. Ph.D. Thesis, Faculty of Computer Science, Electrical Engineering, and Mathematics, University of Paderborn
Webster BL (2004) Solving combinatorial optimization problems using a new algorithm based on gravitational attraction. Florida Institute of Technology
Wolper P, Godefroid P (1991) Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design—Special issue on computer-aided verification: special methods II, pp 149–164
Yousefian R, Rafe V, Rahmani M (2014) A heuristic approach for model checking graph transformation systems. Appl Soft Comput 24:169–180
Yousefian R, Aboutorabi S, Rafe V (2016) A greedy algorithm versus metaheuristic solutions to deadlock detection in graph transformation systems. J Intell Fuzzy Syst 13(1):1–13
Ziegert S (2014) Graph transformation planning via abstraction. arXiv preprint arXiv:1407.7933
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
Conflict of interest
The authors declare that there is no conflict of interest for any of them in this article.
Ethical approval
This article does not contain any studies with human participants or animals performed by any of the authors.
Additional information
Communicated by V. Loia.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Partabian, J., Rafe, V., Parvin, H. et al. An approach based on knowledge exploration for state space management in checking reachability of complex software systems. Soft Comput 24, 7181–7196 (2020). https://doi.org/10.1007/s00500-019-04334-3
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00500-019-04334-3