دوره 20، شماره 2 - ( 6-1402 )
جلد 20 شماره 2 صفحات 194-175 |
برگشت به فهرست نسخه ها
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-fa.html
URL: http://jsdp.rcisp.ac.ir/article-1-1240-fa.html
پرتابیان جعفر. وارسی ویژگی دسترس‌پذیری در سیستم‌های تبدیل گراف با رویکرد کشف وابستگی شرطی بین قوانین. پردازش علائم و داده‌ها. 1402; 20 (2) :175-194
دانشگاه ازاد اسلامی لامرد
چکیده: (574 مشاهده)
وارسی مدل[1] یکی از مؤثرترین تکنیکهای صحت سنجی خودکار ویژگی‌های سیستم‌های سخت‌افزاری و نرم‌افزاری است. در حالت کلی، در این روش، مدلی از سیستم موردنظر تولید میشود و تمام حالات ممکن در گراف فضای حالت مورد کاوش قرار می‌گیرد تا بتواند خطاها و الگوهای نامطلوب را پیدا کند. در سیستم‌های بزرگ و پیچیده تولید تمام فضای حالت منجر به مشکل انفجار فضای حالت[2] میشود. تحقیقات اخیر نشان می‌دهند که کاوش در فضای حالت با استفاده از روش‌های هوشمندانه، می‌تواند ایده امیدوارکننده‌ای باشد. ازاین‌رو در این تحقیق ابتدا مدلی از سیستم موردنظر ایجاد میشود، سپس بخشی از فضای حالت مدل، تولیدشده و با استفاده از احتمالات شرطی، وابستگی بین قوانین موجود در فضای حالت کشف می‌شوند. پس از آن، با کمک وابستگی‌های کشف‌شده، بقیه فضای حالت مدل را به‌طور هوشمندانه مورد کاوش قرار می‌گیرد. در این مقاله روشی برای وارسی ویژگی دسترس‌پذیری[3] در سیستم‌های نرم‌افزاری پیچیده و بزرگ که به زبان رسمی تبدیل گراف[4] (GTS) مدل شده‌اند، ارائه میشود. روش پیشنهادی در GROOVE که یک مجموعه ابزار منبع باز برای طراحی و بررسی وارسی مدل سیستم‌های تبدیل گراف می‌باشد، پیاده‌سازی شده است. نتایج آزمایش‌های تجربی نشان می‌دهند که رویکرد پیشنهادی نسبت به روش‌های قبلی سریع‌تر بوده و مثال‌های نقض[5]/شاهد[6]کوتاه‌تری تولید می‌کند.
شماره‌ی مقاله: 11
نوع مطالعه: پژوهشي |
موضوع مقاله:
مقالات پردازش داده‌های رقمی
دریافت: 1400/3/20 | پذیرش: 1402/3/12 | انتشار: 1402/7/30 | انتشار الکترونیک: 1402/7/30
دریافت: 1400/3/20 | پذیرش: 1402/3/12 | انتشار: 1402/7/30 | انتشار الکترونیک: 1402/7/30
فهرست منابع
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]
ارسال پیام به نویسنده مسئول
| بازنشر اطلاعات | |
 |
این مقاله تحت شرایط Creative Commons Attribution-NonCommercial 4.0 International License قابل بازنشر است. |
