MS-ACO: a multi-stage ant colony optimization to refute complex software systems specified through graph transformation

• 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

• Abreu N, Ajmal M, Kokkinogenis Z, Bozorg B (2011) Ant colony optimization [Online]. http://paginas.fe.up.pt/~mac/ensino/docs/DS20102011/Presentations/PopulationalMetaheuristics/ACO_Nuno_Muhammad_Zafeiris_Behdad.pdf. Accessed 18 Jun 2012

• 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

• 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

• Alba E, Chicano F (2007b) ACOhg: dealing with huge graphs. In: Proceedings of the 9th annual conference on genetic and evolutionary computation. ACM, pp 10–17

• Alba E, Chicano F (2007c) 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 (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

• 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

• Baier C, Katoen JP, Larsen KG (2008) Principles of model checking, vol 2620264. MIT press, Cambridge

  MATH  Google Scholar 

• Blum C, Roli A (2003) Metaheuristics in combinatorial optimization: overview and conceptual comparison. ACM Comput Surv 35(3):268–308

  Article  Google Scholar 

• 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

• 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

• 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

• Dorigo M, Birattari M, Stutzle T (2006) ant colony optimization. IEEE Comput Intell Mag 1(4):28–39

  Article  Google Scholar 

• 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

  Chapter  Google Scholar 

• Edelkamp S, Reffel F (1998) OBDDs in heuristic search. In: Annual conference on artificial intelligence. Springer, Berlin Heidelberg, pp 81–92

• 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

• Edelkamp S, Lafuenteand AL, Leue S (2001) Protocol verification with heuristic search. In: AAAI symposium on model based validation of intelligence

• 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

  Article  Google Scholar 

• 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

• 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: International conference on the unified modeling language. Springer, Berlin Heidelberg, pp 323–337

• Estler HC, Wehrheim H (2011) Heuristic search-based planning for graph transformation systems. KEPS 2011:54

  Google Scholar 

• 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

• 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

• 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

• Gaschnig J (1979) Performance measurement and analysis of certain search algorithms. Technical Report. CMU-CS-79-124, Carnegie-Mellon University

• Ghamarian AH, de Mol M, Rensink A, Zambon E, Zimakova M (2012) Modelling and analysis using GROOVE. Int J Softw Tools Technol Transf (STTT) 14(1):15–40

  Article  Google Scholar 

• Godefroid P (1990) Using partial orders to improve automatic verification methods. In: International conference on computer aided verification. Springer, Berlin, Heidelberg, pp 176–185

• 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

• 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

• 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

  Article  MATH  Google Scholar 

• 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

  Book  Google Scholar 

• Groce A, Visser W (2004) Heuristics for model checking Java programs. Int J Softw Tools Technol Transf (STTT) 6(4):260–276

  Article  MATH  Google Scholar 

• Hausmann JH (2005) Dynamic meta modeling: a semantics description technique for visual modeling techniques. Ph.D. Thesis, Universität Paderborn

• Heckel R (2006) Graph transformation in a nutshell. Electron Notes Theoret Comput Sci 148(1):187–198

  Article  Google Scholar 

• Heckel R, Thöne S (2005) Behavioral refinement of graph transformation-based models. Electron Notes Theor Comput Sci 127(3):101–111

  Article  MATH  Google Scholar 

• Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279–295

  Article  Google Scholar 

• 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

  Chapter  Google Scholar 

• 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

• 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: Computer and information science, vol 614. Springer International Publishing, pp 75–96

• 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

• Mens T, Van Der Straeten R, D’Hondt M (2006) Detecting and resolving model inconsistencies using transformation dependency analysis. In: International conference on model driven engineering languages and systems. Springer, Berlin Heidelberg, pp 200–214

• Naddaf MR, Rafe V (2014) Performance modeling and analysis of software architectures specified through graph transformations. Comput Inform 32(4):797–826

  MATH  Google Scholar 

• Pearl J (2014) Probabilistic reasoning in intelligent systems: networks of plausible inference. Morgan Kaufmann, Burlington

  MATH  Google Scholar 

• 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

  Google Scholar 

• Peng H, Tahar S (1998) A survey on compositional verification. Technical Report, Department of Electrical and Computer Engineering, Concordia University

• 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

  Article  Google Scholar 

• 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

  Article  Google Scholar 

• 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

  Article  Google Scholar 

• Rafe V (2013) Scenario-driven analysis of systems specified through graph transformations. J Vis Lang Comput 24(2):136–145

  Article  Google Scholar 

• Rafe V, Hajvali M (2013) Designing an architectural style for pervasive healthcare systems. J Med Syst 37(2):1–13

  Article  Google Scholar 

• 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

• 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

  Article  MATH  Google Scholar 

• 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

  Article  Google Scholar 

• Rensink A (2003) The GROOVE simulator: a tool for state space generation. In: International workshop on applications of graph transformations with industrial relevance. Springer, Berlin, Heidelberg, pp 479–485

• Rensink A, Boneva I, Kastenberg H, Staijen T (2010) User manual for the GROOVE tool set. Department of Computer Science, University of Twente, Enschede

  Google Scholar 

• Roever WP (1998) The need for compositional proof systems: a survey. In: Compositionality: the significant difference. Springer, Berlin, Heidelberg, pp 1–22

• Schmidt A (2004) Model checking of visual modeling languages. Master’s Thesis, Budapest University of Technology and Economics, Hungary

• Sivaraja H, Gopalakrishnan G (2003) Random walk based heuristic algorithms for distributed memory model checking. Electron Notes Theoret Comput Sci 89(1):51–67

  Article  MATH  Google Scholar 

• Snippe E (2011) Using heuristic search to solve planning problems in GROOVE. In: 14th Twente student conference on IT. University of Twente

• 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

• Stern U, Dill DL (1996) A new scheme for memory-efficient probabilistic verification. In: Formal description techniques IX. Springer, US, pp 333–348

  Chapter  Google Scholar 

• Swaroop D (1997) String stability of interconnected systems: an application to platooning in automated highway systems. California Partners for Advanced Transit and Highways (PATH)

• 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

• 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

• Thomas JP (2000) Design and verification of a coordination protocol for cooperating systems. Soft Comput 4(2):130–140

  Article  Google Scholar 

• 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

• 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

• Wilcoxon F (1945) Individual comparisons by ranking methods. Biom Bull 1(6):80–83

  Article  Google Scholar 

• Wolper P, Leroy D (1993) Reliable hashing without collision detection. In: International conference on computer aided verification. Springer, Berlin Heidelberg, pp 59–70

• Yang CH (1999) Prioritized model checking. Ph.D. thesis, Stanford University

• Yang XS (2010) A new metaheuristic bat-inspired algorithm. In: Nature inspired cooperative strategies for optimization (NICSO 2010), vol 284, pp 65–74

• 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

• Yousefian R, Rafe V, Rahmani M (2014) A heuristic solution for model checking graph transformation systems. Appl Soft Comput 24:169–180

  Article  Google Scholar 

• 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

  Article  Google Scholar 

• Zhu W, Han Y, Zhou Q (2018) Performing CTL model checking via DNA computing. Soft Comput. https://doi.org/10.1007/s00500-018-3314-7

  Google Scholar 

• Ziegert S (2014) Graph transformation planning via abstraction. arXiv preprint arXiv: 1407.7933

Download references