Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Soft Computing
Published in: Soft Computing 12/2019

10-08-2018 | Methodologies and Application

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

Authors: Vahid Rafe, Mahsa Darghayedi, Einollah Pira

Published in: Soft Computing | Issue 12/2019

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Model checking is one of the successful techniques in automated verification of software and hardware systems. However, employing this technique for verification of properties such as the safety and liveness requires that all possible states of a system are generated and then the given property is checked. In large and complex systems, generating all states causes the state space explosion problem. Hence, it is possible to refute such properties by searching the state space to find a state in which the given property is violated. Of course, it is possible that detecting such states in complex systems leads to the exhaustive exploration of the state space. Recent researches confirm that using meta-heuristic and evolutionary approaches to intelligently explore a portion of the state space can be a promising idea. Hence, in this paper, we propose an approach based on ant colony optimization algorithm for refuting the safety and liveness properties and also analyzing reachability ones in systems specified formally through graph transformation system. Refutation of liveness and analyzing reachability properties in systems modeled by graph transformations are the prominent advantages of this approach in comparison with the previous approaches. The proposed approach is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. Experimental results show that our proposed approach is faster and it generates shorter counterexamples in comparison with others.
previous article A new effective solution method for fully intuitionistic fuzzy transportation problem
next article AFCGD: an adaptive fuzzy classifier based on gradient descent

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
Particle Swarm Optimization.
 
2
Simulated Annealing.
 
Literature
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
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, CambridgeMATH
Blum C, Roli A (2003) Metaheuristics in combinatorial optimization: overview and conceptual comparison. ACM Comput Surv 35(3):268–308CrossRef
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–39CrossRef
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–232CrossRef
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–267CrossRef
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
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–40CrossRef
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–164CrossRefMATH
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, HeidelbergCrossRef
Groce A, Visser W (2004) Heuristics for model checking Java programs. Int J Softw Tools Technol Transf (STTT) 6(4):260–276CrossRefMATH
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–198CrossRef
Heckel R, Thöne S (2005) Behavioral refinement of graph transformation-based models. Electron Notes Theor Comput Sci 127(3):101–111CrossRefMATH
Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279–295CrossRef
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–192CrossRef
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–826MATH
Pearl J (2014) Probabilistic reasoning in intelligent systems: networks of plausible inference. Morgan Kaufmann, BurlingtonMATH
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
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–1201CrossRef
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–200CrossRef
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–134CrossRef
Rafe V (2013) Scenario-driven analysis of systems specified through graph transformations. J Vis Lang Comput 24(2):136–145CrossRef
Rafe V, Hajvali M (2013) Designing an architectural style for pervasive healthcare systems. J Med Syst 37(2):1–13CrossRef
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–1105CrossRefMATH
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–149CrossRef
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
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–67CrossRefMATH
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–348CrossRef
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–140CrossRef
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–83CrossRef
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–180CrossRef
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–149CrossRef
Ziegert S (2014) Graph transformation planning via abstraction. arXiv preprint arXiv: 1407.7933
Metadata
Title
MS-ACO: a multi-stage ant colony optimization to refute complex software systems specified through graph transformation
Authors
Vahid Rafe
Mahsa Darghayedi
Einollah Pira
Publication date
10-08-2018
Publisher
Springer Berlin Heidelberg
Published in
Soft Computing / Issue 12/2019
Print ISSN: 1432-7643
Electronic ISSN: 1433-7479
DOI
https://doi.org/10.1007/s00500-018-3444-y

Other articles of this Issue 12/2019

Soft Computing 12/2019 Go to the issue

Methodologies and Application

A simple water cycle algorithm with percolation operator for clustering analysis

Methodologies and Application

Belief-based chaotic algorithm for support vector data description

Methodologies and Application

Automatic identification of characteristic points related to pathologies in electrocardiograms to design expert systems

Methodologies and Application

An angle-based method for measuring the semantic similarity between visual and textual features

Methodologies and Application

C-means clustering and deep-neuro-fuzzy classification for road weight measurement in traffic management system

Methodologies and Application

A two-product, multi-period nonstationary newsvendor problem with budget constraint

Premium Partner

    Image Credits