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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 3/2006

01.05.2006

Optimistic synchronization-based state-space reduction

verfasst von: Scott D. Stoller, Ernie Cohen

Erschienen in: Formal Methods in System Design | Ausgabe 3/2006

Einloggen

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

search-config
loading …

Abstract

Reductions that aggregate fine-grained transitions into coarser transitions can significantly reduce the cost of automated verification, by reducing the size of the state space. We propose a reduction that can exploit common synchronization disciplines, such as the use of mutual exclusion for accesses to shared data structures. Exploiting them using traditional reduction theorems requires checking that the discipline is followed in the original (i.e., unreduced) system. That check can be prohibitively expensive. This paper presents a reduction that instead requires checking whether the discipline is followed in the reduced system. This check may be much cheaper, because the reachable state space is smaller.
Vorheriger Artikel Feature interaction detection by pairwise analysis of LTL properties—A case study

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 "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

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
Fußnoten
1
The axioms are equivalent to Kozen's axioms for Kleene algebra [14], plus the three axioms for omega terms.
 
2
Magic is the program that has no possible executions (and so satisfies every possible specification). Of course, it cannot be implemented.
 
3
Note that \( u_i \) and \( v_i \) can be sums of nondeterministic actions that correspond to individual transitions of process i.
 
Literatur
1.
G. Brat, K. Havelund, S. Park, and W. Visser, “Model checking programs,” in IEEE Int'l. Conference on Automated Software Engineering (ASE), 2000, pp. 3–12.
2.
E.M. Clarke, Jr., O. Grumberg, and D.A. Peled, Model Checking, MIT Press, 1999.
3.
E. Cohen and L. Lamport, “Reduction in TLA,” in Proc. 9th Int'l. Conference on Concurrency Theory (CONCUR), vol. 1466 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 317–331.
4.
E. Cohen, “Separation and reduction,” in Proc. 5th Int'l. Conference on Mathematics of Program Construction, vol. 1837 of Lecture Notes in Computer Science, Springer-Verlag, 2000.
5.
C. Flanagan and S. Freund, “Detecting race conditions in large programs,” in Workshop on Program Analysis for Software Tools and Engineering (PASTE), ACM Press, 2001, pp. 90–96.
6.
C. Flanagan, S.N. Freund, and S. Qadeer, “Thread-modular verification for shared-memory programs,” in Proc. European Symposium on Programming (ESOP), 2002, pp. 262–277.
7.
C. Flanagan, S. Qadeer, and S. Seshia, “A modular checker for multithreaded programs,” in Proc. 14th Int'l. Conference on Computer-Aided Verification (CAV), vol. 2404 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pp. 180–194.
8.
C. Flanagan and S. Qadeer, “Transactions for software model checking,” in Proc. 2nd Workshop on Software Model Checking, vol. 89(3) of Electronic Notes in Theoretical Computer Science. Elsevier, 2003.
9.
P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, vol. 1032 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
10.
P. Godefroid, “Model checking for programming languages using VeriSoft,” in Proc. 24th ACM Symposium on Principles of Programming Languages (POPL), ACM Press, 1997, pp. 174–186.
11.
K. Havelund and T. Pressburger, “Model checking Java programs using Java PathFinder,” Int. J. on Softw. Tools for Technol. Trans., Vol. 2, No. 4, 2000.
12.
G.J. Holzmann, “The Spin model checker,” IEEE Trans. Softw. Engi., Vol. 23, No. 5, pp. 279–295, 1997.
13.
G.J. Holzmann and D. Peled, “An improvement in formal verification,” in Proc. 7th Int'l. Conference on Formal Description Techniques (FORTE ′94), Chapman & Hall, 1995, pp. 197–211.
14.
D. Kozen, “A completeness theorem for Kleene algebras and the algebra of regular events,” Inform. Comput., Vol. 110, No. 2, pp. 366–390, 1994.
15.
R.J. Lipton, “Reduction: A method of proving properties of parallel programs,” Communications of the ACM, Vol. 18, No. 12, pp. 717–721, 1975.
16.
S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T.E. Anderson, “Eraser: A dynamic data race detector for multi-threaded programs,” ACM Trans. on Comp. Syst., Vol. 15, No. 4, pp. 391–411, 1997.
17.
S.D. Stoller and E. Cohen, “Optimistic synchronization-based state-space reduction,” in Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 2619 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 489–504.
18.
S.D. Stoller, “Model-checking multi-threaded distributed Java programs,” Int. J. on Softw. Tools for Technol. Trans., Vol. 4, No. 1, pp. 71–91, 2002.
19.
A. Valmari, “Stubborn set methods for process algebras,” in D. Peled, V.R. Pratt, and G.J. Holzmann (Eds.), Proc. Workshop on Partial Order Methods in Verification, vol. 29 of DIMACS Series, American Mathematical Society, 1997, pp. 213–231.
20.
C. von Praun and T.R. Gross, “Object race detection,” in Proc. 16th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), vol. 36(11) of SIGPLAN Notices, ACM Press, 2001, pp. 70–82.
21.
J. Whaley and M.C. Rinard, “Compositional pointer and escape analysis for Java programs,” in Proc. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), ACM Press, 1999, pp. 187–206.
Metadaten
Titel
Optimistic synchronization-based state-space reduction
verfasst von
Scott D. Stoller
Ernie Cohen
Publikationsdatum
01.05.2006
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 3/2006
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-006-0003-4