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
Erschienen in:
Place Bisimulation and Liveness for Open Petri Nets Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Exploiting Symmetry for Efficient Verification of Infinite-State Component-Based Systems

verfasst von : Qiang Wang

Erschienen in: Dependable Software Engineering: Theories, Tools, and Applications

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

In this paper we present an efficient verification algorithm for infinite-state component-based systems modeled in the behavior-interaction-priority (\(\textsc {BIP}\)) framework. Our algorithm extends the persistent set partial order reduction by taking into account system symmetries, and further combines it with lazy predicate abstraction. We have implemented the new verification algorithm in our model checker for \(\textsc {BIP}\). The experimental evaluation shows that for systems exhibiting certain symmetries, our new algorithm outperforms the existing algorithms significantly.

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 Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies
Nächstes Kapitel Formalization of Fault Trees in Higher-Order Logic: A Deep Embedding Approach
Fußnoten
2
We include the independence detection time in the running time of our new algorithm.
 
3
Red diagonal guides provide a reference for comparison, each indicating shift of one order of magnitude.
 
Literatur
1.
Abdellatif, T., Bensalem, S., Combaz, J., de Silva, L., Ingrand, F.: Rigorous design of robot software: a formal component-based approach. Robot. Auton. Syst. 60, 1563–1578 (2012)CrossRef
2.
Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
3.
Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28, 41–48 (2011)CrossRef
4.
Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. STTT 14, 53–72 (2012)CrossRef
5.
Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: a tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614–619. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02658-4_​45 CrossRef
6.
Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: D-Finder 2: towards efficient correctness of incremental design. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 453–458. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-20398-5_​32 CrossRef
7.
Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326–343. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-24953-7_​25 CrossRef
8.
9.
Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46–61. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54862-8_​4 CrossRef
10.
Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking with explicit scheduler and symbolic threads. Log. Meth. Comput. Sci. 8(2) (2012). doi:10.​2168/​LMCS-8(2:​18)2012
11.
Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 147–158. Springer, Heidelberg (1998). doi:10.​1007/​BFb0028741 CrossRef
12.
Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9, 77–104 (1996)CrossRef
13.
Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2, 279–287 (1999)CrossRefMATH
14.
15.
Donaldson, A.F., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods Syst. Des. 41, 25–44 (2012)CrossRefMATH
16.
Emerson, E.A., Jha, S., Peled, D.: Combining partial order and symmetry reductions. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 19–34. Springer, Heidelberg (1997). doi:10.​1007/​BFb0035378 CrossRef
17.
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods Syst. Des. 9, 105–131 (1996)CrossRef
18.
Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999). doi:10.​1007/​3-540-48153-2_​12 CrossRef
19.
20.
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL (2005)
21.
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. ACM SIGPLAN Not. 37, 191–202 (2002). ACMCrossRefMATH
22.
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, New York (1996)CrossRefMATH
23.
24.
He, F., Yin, L., Wang, B.-Y., Zhang, L., Mu, G., Meng, W.: VCS: a verifier for component-based systems. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 478–481. Springer, Heidelberg (2013). doi:10.​1007/​978-3-319-02444-8_​39 CrossRef
25.
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. ACM SIGPLAN Not. 39, 232–244 (2004). ACMCrossRefMATH
26.
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. ACM SIGPLAN Not. 37, 58–70 (2002)CrossRefMATH
27.
Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. STTT 6, 302–319 (2004)CrossRef
28.
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9, 41–75 (1996)CrossRef
29.
Konnov, I., Kotek, T., Wang, Q., Veith, H., Bliudze, S., Sifakis, J.: Parameterized systems in BIP: design and model checking. In: CONCUR (2016, to appear)
30.
31.
Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. (2006)
32.
33.
Sifakis, J.: Rigorous system design. Found. Trends Electron. Des. Autom. 6(4), 293–362 (2013)CrossRef
34.
Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991). doi:10.​1007/​BFb0023729 CrossRef
35.
Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with Impact. In: FMCAD (2013)
36.
Wahl, T., Donaldson, A.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2, 799–847 (2010)MathSciNetCrossRef
37.
38.
Qiang, W., Bliudze, S.: Verification of component-based systems via predicate abstraction and simultaneous set reduction. In: Ganty, P., Loreti, M. (eds.) TGC 2015. LNCS, vol. 9533, pp. 147–162. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-28766-9_​10 CrossRef
Metadaten
Titel
Exploiting Symmetry for Efficient Verification of Infinite-State Component-Based Systems
verfasst von
Qiang Wang
Copyright-Jahr
2016
Buch
Dependable Software Engineering: Theories, Tools, and Applications

Print ISBN: 978-3-319-47676-6

Electronic ISBN: 978-3-319-47677-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-47677-3_16