{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:42:19Z","timestamp":1762324939086,"version":"3.37.3"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,2,21]],"date-time":"2021-02-21T00:00:00Z","timestamp":1613865600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,2,21]],"date-time":"2021-02-21T00:00:00Z","timestamp":1613865600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2022,3]]},"DOI":"10.1007\/s11219-020-09542-x","type":"journal-article","created":{"date-parts":[[2021,2,21]],"date-time":"2021-02-21T06:03:18Z","timestamp":1613887398000},"page":"37-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Using knowledge discovery to propose a two-phase model checking for safety analysis of graph transformations"],"prefix":"10.1007","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9010-6113","authenticated-orcid":false,"given":"Einollah","family":"Pira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,2,21]]},"reference":[{"key":"9542_CR1","doi-asserted-by":"crossref","unstructured":"Abowd, G., Allen, R., & Garlan D. (1993). Using style to give meaning to software architecture, in Proc. of SIGSOFT \u201893: Foundations of Software Engineering. p. 9\u201320.","DOI":"10.1145\/167049.167055"},{"key":"9542_CR2","doi-asserted-by":"crossref","unstructured":"Alba E., & Chicano, F. (2007). Finding safety errors with ACO, in Proceedings of the 9th annual conference on Genetic and evolutionary computation. p. 1066\u20131073.","DOI":"10.1145\/1276958.1277171"},{"key":"9542_CR3","doi-asserted-by":"crossref","unstructured":"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. p. 1735\u20131742.","DOI":"10.1145\/1389095.1389432"},{"key":"9542_CR4","doi-asserted-by":"crossref","unstructured":"Alba, E., & Troya, JM. (1996). Genetic algorithms for protocol validation, in International Conference on Parallel Problem Solving from Nature. p. 869\u2013879.","DOI":"10.1007\/3-540-61723-X_1050"},{"key":"9542_CR5","doi-asserted-by":"crossref","unstructured":"Arcuri, A., & Briand. L. (2011). A practical guide for using statistical tests to assess randomized algorithms in software engineering, in 2011 33rd International Conference on Software Engineering (ICSE). p. 1\u201310.","DOI":"10.1145\/1985793.1985795"},{"issue":"1","key":"9542_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.14257\/ijunesst.2014.7.1.18","volume":"7","author":"MRS Azim","year":"2014","unstructured":"Azim, M. R. S., Mahmud, K., & Das, C. K. (2014). Automatic train track switching system with computerized control from the central monitoring unit. International Journal of u-and e-Service, Science and Technology, 7(1), 201\u2013212.","journal-title":"International Journal of u-and e-Service, Science and Technology"},{"key":"9542_CR7","first-page":"1","volume":"1","author":"C Baier","year":"2008","unstructured":"Baier, C., & Katoen, J.-P. (2008). Principles of model checking. MIT press, 1, 1\u201313.","journal-title":"Principles of model checking. MIT press"},{"issue":"9","key":"9542_CR8","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/35.312843","volume":"32","author":"SM Bellovin","year":"1994","unstructured":"Bellovin, S. M., & Cheswick, W. R. (1994). Network firewalls. IEEE communications magazine, 32(9), 50\u201357.","journal-title":"IEEE communications magazine"},{"key":"9542_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ress.2011.10.003","volume":"99","author":"M Bouali","year":"2012","unstructured":"Bouali, M., Barger, P., & Schon, W. (2012). Backward reachability of Colored Petri Nets for systems diagnosis. Reliability Engineering & System Safety, 99, 1\u201314.","journal-title":"Reliability Engineering & System Safety"},{"key":"9542_CR10","first-page":"171","volume":"4","author":"H Chen","year":"2004","unstructured":"Chen, H., Dean, D., & Wagner, D. (2004). Model Checking One Million Lines of C Code. NDSS, 4, 171\u2013185.","journal-title":"NDSS"},{"key":"9542_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E., McMillan, K., Campos, S., & V. (1996). Hartonas-Garmhausen, Symbolic model checking, in International conference on computer aided verification, pp. 419\u2013422.","DOI":"10.1007\/3-540-61474-5_93"},{"key":"9542_CR12","doi-asserted-by":"crossref","unstructured":"Dajani-Brown, S., Cofer, D., Hartmann, G., & Pratt, S., (2003) Formal modeling and analysis of an avionics triplex sensor voter, in International SPIN Workshop on Model Checking of Software. p. 34\u201348.","DOI":"10.1007\/3-540-44829-2_3"},{"key":"9542_CR13","unstructured":"Edelkamp, S., Lafuente, L., & Leue, S. (2001). Protocol verification with heuristic search. Bibliothek der Universit\u00e4t Konstanz."},{"key":"9542_CR14","doi-asserted-by":"crossref","unstructured":"Francesca, G, Santone, A., Vaglini, G., & Villani, ML. (2011). Ant colony optimization for deadlock detection in concurrent systems, in Computer software and applications conference (COMPSAC), 2011 IEEE 35th annual. p. 108\u2013117.","DOI":"10.1109\/COMPSAC.2011.22"},{"key":"9542_CR15","doi-asserted-by":"crossref","unstructured":"Godefroid P., Holzmann G.J., Pirottin D. (1992). State space caching revisited, in International Conference on Computer Aided Verification, pp. 178\u2013191.","DOI":"10.1007\/3-540-56496-9_15"},{"issue":"4","key":"9542_CR16","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/s10009-003-0130-9","volume":"6","author":"A Groce","year":"2004","unstructured":"Groce, A., & Visser, W. (2004). Heuristics for model checking Java programs. International Journal on Software Tools for Technology Transfer, 6(4), 260\u2013276.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9542_CR17","doi-asserted-by":"crossref","unstructured":"Groote, J.F., & de Pol, J, van. (1996) A bounded retransmission protocol for large data packets, in International Conference on Algebraic Methodology and Software Technology. p. 536\u2013550.","DOI":"10.1007\/BFb0014338"},{"key":"9542_CR18","unstructured":"Hausmann, JH. (2005) Dynamic META modeling: a semantics description technique for visual modeling languages."},{"issue":"4","key":"9542_CR19","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., & Pressburger, T. (2000). Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 2(4), 366\u2013381.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9542_CR20","first-page":"339","volume":"87","author":"GJ Holzmann","year":"1987","unstructured":"Holzmann, G. J. (1987). On limits and possibilities of automated protocol analysis. PSTV, 87, 339\u2013344.","journal-title":"PSTV"},{"key":"9542_CR21","doi-asserted-by":"crossref","unstructured":"Kastenberg, H., & Rensink, A. (2006). Model checking dynamic states in GROOVE, in International SPIN Workshop on Model Checking of Software. p. 299\u2013305.","DOI":"10.1007\/11691617_19"},{"key":"9542_CR22","unstructured":"Koller, D., Friedman, N., & Bach. F. (2009). Probabilistic graphical models: principles and techniques. MIT press."},{"key":"9542_CR23","doi-asserted-by":"crossref","unstructured":"Lluch-Lafuente, A., Edelkamp, S., & Leue S., (2002). Partial order reduction in directed model checking, in International SPIN Workshop on Model Checking of Software, pp. 112\u2013127.","DOI":"10.1007\/3-540-46017-9_10"},{"key":"9542_CR24","unstructured":"Lluch-Lafuente, A., (2003) Symmetry reduction and heuristic search for error detection in model checking."},{"key":"9542_CR25","first-page":"75","volume":"2016","author":"J Maeoka","year":"2015","unstructured":"Maeoka, J., Tanabe, Y., & Ishikawa, F. (2015). Depth-first heuristic search for software model checking, in Computer and Information Science. Springer, 2016, 75\u201396.","journal-title":"Springer"},{"key":"9542_CR26","doi-asserted-by":"crossref","unstructured":"Marrero M., Clarke E., & Jha S. (1997). Model checking for security protocols, Carnegie-Mellon Univ Pittsburgh Pa Dept Of Computer Science.","DOI":"10.21236\/ADA327281"},{"issue":"1","key":"9542_CR27","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1504\/IJCAET.2013.050552","volume":"5","author":"A Nassima","year":"2013","unstructured":"Nassima, A., Zahia, T., & Nadjet, K. (2013). Toward a backward model checking. International Journal of Computer Aided Engineering and Technology, 5(1), 20\u201343.","journal-title":"International Journal of Computer Aided Engineering and Technology"},{"key":"9542_CR28","doi-asserted-by":"publisher","first-page":"1185","DOI":"10.1016\/j.asoc.2016.06.039","volume":"49","author":"E Pira","year":"2016","unstructured":"Pira, E., Rafe, V., & Nikanjam, A. (2016). EMCDM: Efficient model checking by data mining for verification of complex software systems specified through architectural styles. Applied Soft Computing, 49, 1185\u20131201.","journal-title":"Applied Soft Computing"},{"key":"9542_CR29","doi-asserted-by":"crossref","unstructured":"Pira, E., Rafe, V., & Nikanjam, A. (2019). Using evolutionary algorithms for reachability analysis of complex software systems specified through graph transformation, Reliability Engineering & System Safety, p. 106577.","DOI":"10.1016\/j.ress.2019.106577"},{"key":"9542_CR30","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/j.jss.2017.05.128","volume":"131","author":"E Pira","year":"2017","unstructured":"Pira, E., Rafe, V., & Nikanjam, A. (2017). Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm. Journal of Systems and Software, 131, 181\u2013200.","journal-title":"Journal of Systems and Software"},{"key":"9542_CR31","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.infsof.2018.01.004","volume":"97","author":"E Pira","year":"2018","unstructured":"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. Information and Software Technology, 97, 110\u2013134.","journal-title":"Information and Software Technology"},{"issue":"2","key":"9542_CR32","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.jvlc.2012.12.002","volume":"24","author":"V Rafe","year":"2013","unstructured":"Rafe, V. (2013). Scenario-driven analysis of systems specified through graph transformations. Journal of Visual Languages & Computing, 24(2), 136\u2013145.","journal-title":"Journal of Visual Languages & Computing"},{"key":"9542_CR33","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.asoc.2015.04.032","volume":"33","author":"V Rafe","year":"2015","unstructured":"Rafe, V., Moradi, M., Yousefian, R., & Nikanjam, A. (2015). A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations. Applied Soft Computing, 33, 136\u2013149.","journal-title":"Applied Soft Computing"},{"key":"9542_CR34","unstructured":"Rozenberg, G. (1997). Handbook of graph grammars and comp., vol. 1. World scientific."},{"key":"9542_CR35","unstructured":"Runge, O., Khan, TA., & Heckel, R., (2013). Test case generation using visual contracts, Electronic Communications of the EASST, vol. 58."},{"key":"9542_CR36","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/j.ress.2014.10.025","volume":"135","author":"S Sharvia","year":"2015","unstructured":"Sharvia, S., & Papadopoulos, Y. (2015). Integrating model checking with HiP-HOPS in model-based safety analysis. Reliability Engineering & System Safety, 135, 64\u201380.","journal-title":"Reliability Engineering & System Safety"},{"key":"9542_CR37","first-page":"212","volume":"2010","author":"J Staunton","year":"2010","unstructured":"Staunton, J., & Clark, J. A. (2010). Searching for safety violations using estimation of distribution algorithms, in Software Testing, Verification, and Validation Workshops (ICSTW). Third International Conference on, 2010, 212\u2013221.","journal-title":"Third International Conference on"},{"key":"9542_CR38","doi-asserted-by":"crossref","unstructured":"Staunton, J., & Clark, JA. (2011). Finding short counterexamples in promela models using estimation of distribution algorithms, in Proceedings of the 13th annual conference on Genetic and evolutionary computation. p. 1923\u20131930.","DOI":"10.1145\/2001576.2001834"},{"key":"9542_CR39","doi-asserted-by":"crossref","unstructured":"Staunton, J., & Clark, JA. (2011). Applications of model reuse when using estimation of distribution algorithms to test concurrent software, in International Symposium on Search Based Software Engineering. p. 97\u2013111.","DOI":"10.1007\/978-3-642-23716-4_12"},{"key":"9542_CR40","unstructured":"Th\u00f6ne, S. (2005). Dynamic software architectures: a style-based modeling and refinement technique with graph transformations,\u201d PhD Thesis."},{"key":"9542_CR41","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.ress.2018.03.035","volume":"176","author":"D Wu","year":"2018","unstructured":"Wu, D., & Zheng, W. (2018). Formal model-based quantitative safety analysis using timed Coloured Petri Nets. Reliability Engineering & System Safety, 176, 62\u201379.","journal-title":"Reliability Engineering & System Safety"},{"key":"9542_CR42","first-page":"65","volume":"2010","author":"X-S Yang","year":"2010","unstructured":"Yang, X.-S. (2010). A new metaheuristic bat-inspired algorithm, in Nature inspired cooperative strategies for optimization (NICSO. Springer, 2010, 65\u201374.","journal-title":"Springer"},{"issue":"1","key":"9542_CR43","doi-asserted-by":"publisher","first-page":"137","DOI":"10.3233\/IFS-162127","volume":"31","author":"R Yousefian","year":"2016","unstructured":"Yousefian, R., Aboutorabi, S., & Rafe, V. (2016). A greedy algorithm versus metaheuristic solutions to deadlock detection in Graph Transformation Systems. Journal of Intelligent & Fuzzy Systems, 31(1), 137\u2013149.","journal-title":"Journal of Intelligent & Fuzzy Systems"},{"key":"9542_CR44","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.asoc.2014.06.055","volume":"24","author":"R Yousefian","year":"2014","unstructured":"Yousefian, R., Rafe, V., & Rahmani, M. (2014). A heuristic solution for model checking graph transformation systems. Applied Soft Computing, 24, 169\u2013180.","journal-title":"Applied Soft Computing"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-020-09542-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-020-09542-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-020-09542-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,22]],"date-time":"2022-04-22T10:11:55Z","timestamp":1650622315000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-020-09542-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,21]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,3]]}},"alternative-id":["9542"],"URL":"https:\/\/doi.org\/10.1007\/s11219-020-09542-x","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"type":"print","value":"0963-9314"},{"type":"electronic","value":"1573-1367"}],"subject":[],"published":{"date-parts":[[2021,2,21]]},"assertion":[{"value":"25 November 2020","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 February 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}