Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Study and Analysis of Subthreshold Leakage Current in Sub-65 nm NMOSFET Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Towards Distributed Solution to the State Explosion Problem

verfasst von : Lamia Allal, Ghalem Belalem, Philippe Dhaussy

Erschienen in: Information Systems Design and Intelligent Applications

Verlag: Springer India

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In the life cycle of any software system, a crucial phase formalization and validation through verification or testing induces an identification of errors infiltrated during its design. This is achieved through verification by model checking. A model checking algorithm is based on two steps: the construction of state space of the system specification and the verification of this state space. However, these steps are limited by the state explosion problem, which occurs when models are large. In this paper, we propose a solution to this problem to improve performance in execution time and memory space by performing the exploration of state space in a distributed architecture consisting of several machines.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel ICC Cricket World Cup Prediction Model
Nächstes Kapitel Real Time Bus Monitoring System
Literatur
1.
S. Christensen, L. M. Kristensen, and T. Mailund. A sweep-line method for state space exploration. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’2001, pp. 450–464, April 2001.
2.
M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review, 36(4):40–45, 2009.
3.
E. M. Clarke, W. Klieber, M. Nováček, and P. Zuliani. Model checking and the state explosion problem. In Proceedings of the 8th Laser Summer School on Software Engineering, volume 7682, pp. 1–30, September 2011.
4.
R. Pelánek. Fighting state space explosion: Review and evaluation. In Proceedings of the 13th on Formal Methods for Industrial Critical Systems, volume 5596 of FMICS’08, pp. 37–52, September 2008.
5.
E. M. Clarke, O Grumberg, S Jha, Y Lu, and H Veith. Progress on the state explosion problem in model checking. In Informatics—10 Years Back. 10 Years Ahead, pp. 176–194, London, UK, UK, 2001. Springer-Verlag.
6.
K. L McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Pittsburgh, PA, USA, 1992. UMI Order No. GAX92-24209.
7.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 428–439, Philadelphia, PA, 1990. IEEE.
8.
N. M Arkey and Ph. Schnoebelen. Symbolic model checking of simply-timed systems. In Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 2004, volume 3253, pp. 102–117, Grenoble, France, 2004. LSV, ENS Cachan, Springer Berlin Heidelberg.
9.
G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on the fly model checking for ctl. In Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, LICS’95, 1995.
10.
A. Mukherjee, Z.Tari, and P. Bertok. Memory efficient state-space analysis in software model-checking. In Proceedings of the Thirty-Third Australasian Conference on Computer Science, volume 102 of ACSC’10, pp. 23–32, January 2010.
11.
F. Lerda and R. Sisto. Distributed-memory model-checking with spin. In Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, volume 1680, pp. 22–39, July 1999.
12.
P. Dhaussy, J. C. Roger, and F. Boniol. Reducing state explosion with context modeling for model-checking. In Proceedings of the 13th International Symposium on High Assurance Systems Engineering, HASE, pp. 130–137, November 2011.
13.
G. J. Holzmann. The model checker spin. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.
14.
G. J. Holzmann and D Peled. An improvement in formal verification. In Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp. 197–211, 1995.
15.
D Peled. Combining partial order reductions with on-the-fly model-checking. In Proceedings of the 6th International Conference on Computer Aided Verification, CAV’94, pp. 377–390, 1994.
16.
R. T. Saad, S. D. Zilio, and B. Berthomieu. Mixed shared-distributed hash tables approaches for parallel state space construction. In Proceedings of the 10th International Symposium on Parallel and Distributed Computing, ISPDC’11, pp. 9–16, July 2011.
Metadaten
Titel
Towards Distributed Solution to the State Explosion Problem
verfasst von
Lamia Allal
Ghalem Belalem
Philippe Dhaussy
Copyright-Jahr
2016
Verlag
Springer India
Buch
Information Systems Design and Intelligent Applications

Print ISBN: 978-81-322-2753-3

Electronic ISBN: 978-81-322-2755-7

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-81-322-2755-7_56

Premium Partner

    Bildnachweise