Volume 20, Issue 2 (9-2023)
JSDP 2023, 20(2): 175-194 |
Back to browse issues page
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. Checking reachability property of systems specified through graph transformation with the approach of discovery conditional dependency between the rules. JSDP 2023; 20 (2) : 11
URL: http://jsdp.rcisp.ac.ir/article-1-1240-en.html
URL: http://jsdp.rcisp.ac.ir/article-1-1240-en.html
Abstract: (585 Views)
Model checking is among the most effective techniques for automatic verification of hardware and software systems’ properties. Generally, in this method, a model of the desired system is generated and all possible states are explored in the space state graph to find errors and undesirable patterns. In models of large and complex systems, if the size of the generated state space is too extensive so that not all available states can be explored due to computational restrictions, the problem of state space explosion occurs. In fact, this problem confines the validation process in model verification systems. To use the model checking technique, the system must be described in a formal language. Graphs are very beneficial and intuitive tools for describing and modeling software systems. Correspondingly, graph transformation system provides a proper tool for formal description of software system features as well as their automatic verification.
Various techniques have been investigated in the researches to reduce the effect of state space explosion problem in the model checking process. Some of these methods try to reduce the required memory by reducing the number of cases explored. Among others are symbolic model checking, partial-order reduction, symmetry reduction, and scenario-driven model checking. In a complex system, these algorithms, along with conventional methods such as DFS or BFS search algorithms may not afford any complete answer due to the explosion of state space. Hence, the use of intelligent methods such as knowledge-based techniques, datamining, machine learning, and meta-heuristic algorithms which do not entail full state space exploration could be advantageous.
Recent researches attest that exploring the state space using intelligent methods could be a promising idea. Therefore, an intelligent method is used in this research to explore the state space of large and complex systems. Accordingly in this paper, first a model of the desired system is created using graph conversion system. Then a portion of the state space of the model is generated. Afterwards, using the conditional probability table, the dependencies between the rules in the paths toward the goal state are discovered. Finally, by means of the discovered dependencies, the rest of the model state space is intelligently explored. In other words, only promising paths, i.e. those who match the detected dependencies are explored to reach the goal state. It is worth noting that the first goal of the proposed approach is to find a goal state, i.e., one in which either the safety property is violated or the reachability property is satisfied in the shortest possible time. The second less important goal is to reduce the number of explored states in the graph of the state space until reaching the goal state. This paper provides a way to check the availability feature in complex and large software systems modeled in the official graph transformation language. The suggested method is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. The results of experimental tests indicate that the proposed approach is faster than the previous methods and produces a shorter counterexample/witness.
Various techniques have been investigated in the researches to reduce the effect of state space explosion problem in the model checking process. Some of these methods try to reduce the required memory by reducing the number of cases explored. Among others are symbolic model checking, partial-order reduction, symmetry reduction, and scenario-driven model checking. In a complex system, these algorithms, along with conventional methods such as DFS or BFS search algorithms may not afford any complete answer due to the explosion of state space. Hence, the use of intelligent methods such as knowledge-based techniques, datamining, machine learning, and meta-heuristic algorithms which do not entail full state space exploration could be advantageous.
Recent researches attest that exploring the state space using intelligent methods could be a promising idea. Therefore, an intelligent method is used in this research to explore the state space of large and complex systems. Accordingly in this paper, first a model of the desired system is created using graph conversion system. Then a portion of the state space of the model is generated. Afterwards, using the conditional probability table, the dependencies between the rules in the paths toward the goal state are discovered. Finally, by means of the discovered dependencies, the rest of the model state space is intelligently explored. In other words, only promising paths, i.e. those who match the detected dependencies are explored to reach the goal state. It is worth noting that the first goal of the proposed approach is to find a goal state, i.e., one in which either the safety property is violated or the reachability property is satisfied in the shortest possible time. The second less important goal is to reduce the number of explored states in the graph of the state space until reaching the goal state. This paper provides a way to check the availability feature in complex and large software systems modeled in the official graph transformation language. The suggested method is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. The results of experimental tests indicate that the proposed approach is faster than the previous methods and produces a shorter counterexample/witness.
Article number: 11
Keywords: Model checking, State space explosion, Graph transformation system, Conditional probability table, Reachability property
Type of Study: Research |
Subject:
Paper
Received: 2021/06/10 | Accepted: 2023/06/2 | Published: 2023/10/22 | ePublished: 2023/10/22
Received: 2021/06/10 | Accepted: 2023/06/2 | Published: 2023/10/22 | ePublished: 2023/10/22
References
1. [1] Baier C, Katoen JP, Larsen KG (2008) Principles of model checking, vol 2620264. MIT press, Cambridge
2. [2] Chicano F, Francisco M, Ferreira M, Alba E (2011) Comparing metaheuristic algorithms for error detection in java programs. In: International symposium on Search based software engineering, vol 6956. Springer, Berlin, Heidelberg, pp 82-96 [DOI:10.1007/978-3-642-23716-4_11]
3. [3] Taentzer G, Ehrig K, Guerra E, Lara JD, Lengyel L, Levendovszky T, Prange U, Varro D, Varro-Gyapay S (2005) Model transformation by graph transformation: a comparative study. In: Proceedings of model transformations in practice workshop, Models conference, Montego Bay, Jamaica
4. [4] Rafe V, Hajvali M (2013) Designing an architectural style for pervasive healthcare systems. J Med Syst 37(2):1-13 [DOI:10.1007/s10916-013-9927-6] [PMID]
5. [5] Heckel R, Thöne S (2005) Behavioral refinement of graph transformation-based models. Electron Notes the or Comput Sci 127(3):101-111 [DOI:10.1016/j.entcs.2004.08.037]
6. [6] 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: International conference on the unified modeling language. Springer, Berlin Heidelberg, pp 323-337 [DOI:10.1007/3-540-40011-7_23]
7. [7] Mens T (2006) On the use of graph transformations for model refactoring. In: Generative and transformational techniques in software engineering. Springer, Berlin Heidelberg, pp 219-257 [DOI:10.1007/11877028_7]
8. [8] Rafe V, Rahmani AT (2008) Formal analysis of workflows using UML 2.0 activities and graph transformation systems. In: International colloquium on theoretical aspects of computing. Springer Berlin, Heidelberg, pp 305-318 [DOI:10.1007/978-3-540-85762-4_21]
9. [9] Naddaf M, Rafe V (2014) Performance modeling and analysis of software architectures specified through graph transformations. Comput Inform 32(4):797-826
10. [10] Clarke E, McMillan K, Campos S, Hartonas-Garmhausen V (1996) Symbolic model checking. In: International conference on computer aided verification, vol 1102. Springer, Berlin, Heidelberg, pp 419-422 [DOI:10.1007/3-540-61474-5_93]
11. [11] Godefroid P, Van Leeuwen J, Hartmanis J, Goos G, Wolper P (1996) Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, vol 1032. Springer, Heidelberg [DOI:10.1007/3-540-60761-7]
12. [12] Lafuente AL (2003) Symmetry reduction and heuristic search for error detection in model checking. In: Workshop on model checking and artificial intelligence
13. [13] Rafe V (2013) Scenario-driven analysis of systems specified through graph transformations. J Vis Lang Comput 24(2):136-145 [DOI:10.1016/j.jvlc.2012.12.002]
14. [14] Alba E, Chicano F (2008) Searching for liveness property violations in concurrent systems with ACO. In: Proceedings of the 10th annual conference on genetic and evolutionary computation, pp 1727-1734 [DOI:10.1145/1389095.1389431]
15. [15] Rafe V, Moradi M, Yousefian R, Nikanjam A (2015) A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations. Appl Soft Comput 33:136-149 [DOI:10.1016/j.asoc.2015.04.032]
16. [16] Pira E, Rafe V, Nikanjam A (2019) Using evolutionary algorithms for reachability analysis of complex software systems specified through graph transformation, Reliability Engineering and System Safety, vol 191
17. [17] Partabian J, Rafe V, Parvin H, Nejatian S (2019), An Approach Based on Knowledge Exploration for State Space Management in Checking Reachability of Complex Software Systems, soft computing, vol. 24, pp.1-16. [DOI:10.1007/s00500-019-04334-3]
18. [18] Yasrebi M, Rafe V, Parvin H, Nejatian S (2020), 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. [DOI:10.3233/JIFS-190023]
19. [19] Rensink A, Boneva I, Kastenberg H, Staijen T (2010) User manual for the GROOVE tool set. Department of Computer Science, University of Twente, Enschede
20. [20] Peng H, Tahar S (1998) A survey on compositional verification. Technical Report, Department of Electrical and Computer Engineering, Concordia University
21. [21] Roever WP (1998) The need for compositional proof systems: a survey. In: Compositionality: the significant difference. Springer, Berlin, Heidelberg, pp 1-22 [DOI:10.1007/3-540-49213-5_1]
22. [22] Godefroid P (1990) Using partial orders to improve automatic verification methods. In: International conference on computer aided verification. Springer, Berlin, Heidelberg, pp 176-185 [DOI:10.1007/BFb0023731]
23. [23] Valmari A (1988) Error detection by reduced reachability graph generation. In: Proceedings of the 9th European workshop on application and theory of petri nets, pp 95-112
24. [24] Godefroid P, Wolper P (1993) Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods Syst Des 2(2):149-164 [DOI:10.1007/BF01383879]
25. [25] Godefroid P, Van Leeuwen J, Hartmanis J, Goos G, Wolper P (1996) Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, vol 1032. Springer, Heidelberg [DOI:10.1007/3-540-60761-7]
26. [26] Lafuente AL (2003) Symmetry reduction and heuristic search for error detection in model checking. In: Workshop on model checking and artificial intelligence
27. [27] Wolper P, Leroy D (1993) Reliable hashing without collision detection. In: International conference on computer aided verification. Springer, Berlin Heidelberg, pp 59-70 [DOI:10.1007/3-540-56922-7_6]
28. [28] Stern U, Dill D (1995) Improved probabilistic verification by hash compaction. In: Advanced research working conference on correct hardware design and verification methods, vol 987. Springer, Berlin, Heidelberg, pp 206-224 [DOI:10.1007/3-540-60385-9_13]
29. [29] Stern U, Dill DL (1996) A new scheme for memory-efficient probabilistic verification. In: Formal description techniques IX. Springer, US, pp 333-348 [DOI:10.1007/978-0-387-35079-0_21]
30. [30] Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. In: Computer-aided verification, vol 1, issue 2-3. Springer, US, pp 129-142
https://doi.org/10.1007/BF00121128 [DOI:10.1007/978-1-4615-3556-0_5]
31. [31] Isenberg T, Steenken D, Wehrheim H (2013) Bounded model checking of graph transformation systems via SMT solving. In: Formal techniques for distributed systems, vol 7892. Springer, Berlin, Heidelberg, pp 178-192 [DOI:10.1007/978-3-642-38592-6_13]
32. [32] Sivaraja H, Gopalakrishnan G (2003) Random walk based heuristic algorithms for distributed memory model checking. Electron Notes Theory Comput Sci 89(1):51-67 [DOI:10.1016/S1571-0661(05)80096-9]
33. [33] Yang CH (1999) Prioritized model checking. Ph.D. thesis, Stanford Universit
34. [34] Edelkamp S, Lafuente AL, Leue S (2001) Directed explicit model checking with HSF-SPIN. In: Proceedings of the 8th international SPIN workshop on Model checking of software. Springer, New York, pp 57-79 [DOI:10.1007/3-540-45139-0_5]
35. [35] Yang CH, Dill DL (1998) Validation with guided search of the state space. In: Proceedings of the 35th annual design automation conference, pp 599-604 [DOI:10.1145/277044.277201]
36. [36] Groce A, Visser W (2004) Heuristics for model checking Java programs. Int J Software Tools Technology Transf (STTT) 6(4):260-276 [DOI:10.1007/s10009-003-0130-9]
37. [37] Edelkamp S, Reffel F (1998) OBDDs in heuristic search. In: Annual conference on artificial intelligence. Springer, Berlin Heidelberg, pp 81-92 [DOI:10.1007/BFb0095430]
38. [38] Maeoka J, Tanabe Y, Ishikawa F (2016) Depth-first heuristic search for software model checking. In: Computer and information science, vol 614. Springer International Publishing, pp 75-96 [DOI:10.1007/978-3-319-23467-0_6]
39. [39] Edelkamp S, Leue S, Lafuente AL (2004) Directed explicit-state model checking in the validation of communication protocols. Int J Softw Tools Technol (STTT) 5(2-3):247-267 [DOI:10.1007/s10009-002-0104-3]
40. [40] Estler HC, Wehrheim H (2011) Heuristic search-based planning for graph transformation systems. KEPS 2011:54
41. [41] Snippe E (2011) Using heuristic search to solve planning problems in GROOVE. In: 14th Twente student conference on IT. University of Twente
42. [42] Ziegert S (2014) Graph transformation planning via abstraction. arXiv preprint arXiv: 1407.7933 [DOI:10.4204/EPTCS.159.7]
43. [43] Elsinga JW (2016) On a framework for domain independent heuristics in graph transformation planning. Master's thesis, University of Twente
44. [44] Duarte LM, Foss L, Wagner FR, Heimfarth T (2010) Model checking the ant colony optimization. In: Hinchey M, Kleinjohann B, Kleinjohann L, Lindsay P, Rammig FJ, Timmis J, Wolf M (eds) Distributed, parallel and biologically inspired systems, vol 329. Springer, Berlin, Heidelberg, pp 221-232 [DOI:10.1007/978-3-642-15234-4_22]
45. [45] Alba E, Chicano F (2007a) Ant colony optimization for model checking. In: International conference on computer aided systems theory. Springer, Berlin, Heidelberg, pp 523-530 [DOI:10.1007/978-3-540-75867-9_66]
46. [46] Francesca G, Santone A, Vaglini G, Villani ML (2011) Ant colony optimization for deadlock detection in concurrent systems. In: 2011 IEEE 35th annual computer software and applications conference. IEEE, pp 108-117 [DOI:10.1109/COMPSAC.2011.22]
47. [47] Alba E, Chicano F (2008) Searching for liveness property violations in concurrent systems with ACO. In: Proceedings of the 10th annual conference on genetic and evolutionary computation, pp 1727-1734 [DOI:10.1145/1389095.1389431]
48. [48] Kumazawa T, Yokoyama C, Takimoto M, Kambayashi Y (2016) Ant colony Optimization based model checking extended by smell like pheromone. In: Proceedings of the 9th EAI international conference on bio-inspired information and communications technologies (formerly BIONETICS), pp 214-220
https://doi.org/10.4108/eai.21-4-2016.151156 [DOI:10.4108/eai.3-12-2015.2262408]
49. [49] Takada K, Takimoto M, Kumazawa T, Kambayashi Y (2017) ACO based model checking extended by smell-like pheromone with hop counts. In: Harmony search algorithm: proceedings of the 3rd international conference on harmony search algorithm, vol 514 (ICHSA 2017). Springer, p 52 [DOI:10.1007/978-981-10-3728-3_7]
50. [50] Foster H, Uchitel S, Magee J, Kramer J (2006) LTSA-WS: a tool for model-based verification of web service compositions and choreography. In: Proceedings of the 28th international conference on software engineering, Shanghai, China, pp 771-774 [DOI:10.1145/1134285.1134408]
51. [51] 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 Heidelberg, pp 266-280 [DOI:10.1007/3-540-46002-0_19]
52. [52] Alba E, Chicano F, Ferreira M, Gomez-Pulido J (2008) Finding deadlocks in large concurrent java programs using genetic algorithms. In: Proceedings of the 10th annual conference on genetic and evolutionary computation, pp 1735-1742 [DOI:10.1145/1389095.1389432]
53. [53] Godefroid P (1997) Model checking for programming languages using Verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, pp 174-186 [DOI:10.1145/263699.263717]
54. [54] Chicano F, Francisco M, Ferreira M, Alba E (2011) Comparing metaheuristic algorithms for error detection in java programs. In: International symposium on Search based software engineering, vol 6956. Springer, Berlin, Heidelberg, pp 82-96 [DOI:10.1007/978-3-642-23716-4_11]
55. [55] Edelkamp S, Jabbar S, Lafuente AL (2006) Heuristic search for the analysis of graph transition systems. In: International conference on graph transformation. Springer, Berlin, Heidelberg, pp 414-429 [DOI:10.1007/11841883_29]
56. [56] Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279-295 [DOI:10.1109/32.588521]
57. [57] Yousefian R, Aboutorabi S, Rafe V (2016) A greedy algorithm versus metaheuristic solutions to deadlock detection in graph transformation systems. J Intell Fuzzy Syst 31(1):137-149 [DOI:10.3233/IFS-162127]
58. [58] Yang XS (2010) A new meta heuristic bat-inspired algorithm. In: Nature inspired cooperative strategies for optimization (NICSO 2010), vol 284, pp 65-74 [DOI:10.1007/978-3-642-12538-6_6]
59. [59] 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 49:1185-1201 [DOI:10.1016/j.asoc.2016.06.039]
60. [60] Abowd G, Allen R, Garlan D (1993) Using style to give meaning to software architecture. In: ACM SIGSOFT software engineering notes, vol 18, no. 5. ACM, pp 9-20 [DOI:10.1145/167049.167055]
61. [61] Garlan D, Allen R, Ockerbloom J (1994) Exploiting style in architectural design environments. In: ACMSIGSOFT software engineering notes, vol. 19, no. 5. ACM, pp 175-188 [DOI:10.1145/195274.195404]
62. [62] Pira E, Rafe V, Nikanjam A (2018) Searching for violation of safety and liveness properties using knowledge discovery in complex systems specified through graph transformations. Inf Softw Technol 97:110-134 [DOI:10.1016/j.infsof.2018.01.004]
63. [63] Agrawal R, Srikant R (1994) Fast algorithms for mining association rules. In: Proceedings of 20th international conferences on very large data bases, VLDB, vol 1215, pp 487-499
64. [64] 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 [DOI:10.1016/j.jss.2017.05.128]
65. [65] Pelikan M, Goldberg DE, Tsutsui S (2003) Hierarchical Bayesian optimization algorithm: toward a new generation of evolutionary algorithms, vol 3. Springer, Berlin, Heidelberg, pp 2738-2743
66. [66] Thomas JP (2000) Design and verification of a coordination protocol for cooperating systems. Soft Comput 4(2):130-140 [DOI:10.1007/s005000000047]
67. [67] Zhu W, Han Y, Zhou Q (2018) Performing CTL model checking via DNA computing. Soft Comput. [DOI:10.1007/s00500-018-3314-7]
68. [68] Godefroid P (1997) Model checking for programming languages using Verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, pp 174-186 [DOI:10.1145/263699.263717]
69. [69] Taentzer G, Ehrig K, Guerra E, Lara JD, Lengyel L, Levendovszky T, Prange U, Varro D, Varro-Gyapay S (2005) Model transformation by graph transformation: a comparative study. In: Proceedings of model transformations in practice workshop, Models conference, Montego Bay, Jamaica
70. [70] Rafe V, Hajvali M (2013) Designing an architectural style for pervasive healthcare systems. J Med Syst 37(2):1-13 [DOI:10.1007/s10916-013-9927-6] [PMID]
71. [71] Heckel R, Thöne S (2005) Behavioral refinement of graph transformation-based models. Electron Notes Theory Comput Sci 127(3):101-111 [DOI:10.1016/j.entcs.2004.08.037]
72. [72] 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: International conference on the unified modeling language. Springer, Berlin Heidelberg, pp 323-337 [DOI:10.1007/3-540-40011-7_23]
73. [73] Mens T (2006) On the use of graph transformations for model refactoring. In: Generative and transformational techniques in software engineering. Springer, Berlin Heidelberg, pp 219-257 [DOI:10.1007/11877028_7]
74. [74] Naddaf M, Rafe V (2014) Performance modeling and analysis of software architectures specified through graph transformations. Comput Inform 32(4):797-826
75. [75] Rafe V, Rahmani AT (2009) Towards automated software model checking using graph transformation systems and Bogor. J Zhejiang Univ Sci A 10(8):1093-1105 [DOI:10.1631/jzus.A0820415]
76. [76] Moradi M. Rafe V. Yousefian R. and Nikanjam A. (2015). A Meta-Heuristic Solution for Automated Refutation of Complex Software Systems Specified through Graph Transformations. Applied Soft Computing. vol. 33, 136-149. [DOI:10.1016/j.asoc.2015.04.032]
77. [77] Yousefian R, Rafe V, Rahmani M (2014) A heuristic solution for model checking graph transformation systems. Appl Soft Comput 24:169-180 [DOI:10.1016/j.asoc.2014.06.055]
78. [78] Edelkamp S, Lafuente AL, Leue S (2001) Protocol verification with heuristic search. In: AAAI symposium on model-based validation of intelligence, pp 75-83
79. [79] Schmidt A. Model checking of visual modeling languages Master's Thesis Hungary: Budapest University of Technology; 2004
80. [80] Gaschnig J (1979) Performance measurement and analysis of certain search algorithms. Technical Report. CMU-CS-79-124, Carnegie-Mellon University
81. [81] 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
82. [82] Hausmann JH (2005) Dynamic meta modeling: a semantics description technique for visual modeling techniques. Ph.D. Thesis, Universität Paderborn
83. [83] S. Ziegert. "Graph transformation planning via abstraction", arXiv preprint arXiv: 1407.7933. 2014. [DOI:10.4204/EPTCS.159.7]
Send email to the article author
| Rights and permissions | |
 |
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License. |
