Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

07.09.2019 | Methodologies and Application | Ausgabe 10/2020

Soft Computing 10/2020

An approach based on knowledge exploration for state space management in checking reachability of complex software systems

Zeitschrift:
Soft Computing > Ausgabe 10/2020
Autoren:
Jaafar Partabian, Vahid Rafe, Hamid Parvin, Samad Nejatian
Wichtige Hinweise
Communicated by V. Loia.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

Model checking is one of the most efficient techniques in software system verification. However, state space explosion is a big challenge while using this technique to check different properties like safety ones. In this situation, one can search the state space to find a reachable state in which the safety property is violated. Hence, reachability checking can be done instead of checking safety property. However, checking reachability in the worst case may cause state space explosion again. To handle this problem, our idea is based on generating a small model consistent with the main model. Then by exploring the state space entirely, we search it to find the goal states. After finding the goal states, we label the paths which start from the initial state and leading to a goal state. Then using the ensemble classification technique, the necessary knowledge is extracted from these paths to intelligently explore the state space of the bigger model. Ensemble machine learning technique uses Boosting method along with decision trees. It follows sampling techniques by replacement. This method generates k predictive models after sampling k times. Finally, it uses a voting mechanism to predict the labels of the final path. Our proposed approach is implemented in GROOVE, which is an open source toolset for designing and model checking graph transformation systems. Our experiments show a significant improvement in terms of both speed and memory usage. In average, our approach consumes nearly 42% fewer memory than other approaches. Also, it generates witnesses nearly 20% shorter than others, in average.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 10/2020

Soft Computing 10/2020 Zur Ausgabe

Premium Partner

    Bildnachweise