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:
SAT-Based Combinational and Sequential Dependency Computation Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Multi-core SCC-Based LTL Model Checking

verfasst von : Vincent Bloemen, Jaco van de Pol

Erschienen in: Hardware and Software: Verification and Testing

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel.
To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.

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 SAT-Based Combinational and Sequential Dependency Computation
Nächstes Kapitel Gating Aware Error Injection
Fußnoten
1
In practice this is not exactly true, however all necessary conditions are preserved by using a fine-grained locking structure.
 
2
With sufficiently maintaining a DFS order we mean that for any two successive states v and w on the local search stack, we have \(v\rightarrow ^+w\); i.e. we do not require a direct edge from v to w, but w must be reachable from v.
 
6
The reason for this selection is to avoid unrealistic computation times, since the scalability measurements require a run of a sequential algorithm as well.
 
7
When we discuss averages over the experiments, we always take the geometric mean.
 
Literatur
1.
Blahoudek, F., Duret-Lutz, A., Křetínský, M., Strejček, J.: Is there a best Büchi automaton for explicit model checking? In: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014, pp. 68–76. ACM (2014)
2.
Bloemen, V., Laarman, A., van de Pol, J.: Multi-core on-the-fly SCC decomposition. In: Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, pp. 8:1–8:12. ACM (2016)
3.
Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Kurshan, R. (ed.) Computer-Aided Verification, pp. 129–142. Springer US, New York (1993)CrossRef
4.
Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999). doi:10.​1007/​3-540-48119-2_​16
5.
Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized Büchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169–184. Springer, Heidelberg (2005). doi:10.​1007/​11537328_​15 CrossRef
6.
Dijkstra, E.W.: Finding the maximum strong components in a directed graph. In: Dijkstra, E.W. (ed.) Selected Writings on Computing: A personal Perspective. Texts and Monographs in Computer Science, pp. 22–30. Springer, New York (1982)CrossRef
7.
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-46520-3_​8 CrossRef
8.
Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In: Chakraborty, S., Mukund, M. (eds.) Automated Technology for Verification and Analysis. LNCS, vol. 7561, pp. 269–283. Springer, Heidelberg (2012)CrossRef
9.
Evangelista, S., Petrucci, L., Youcef, S.: Parallel nested depth-first searches for LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 381–396. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-24372-1_​27 CrossRef
10.
Fleischer, L.K., Hendrickson, B., Pınar, A.: On identifying strongly connected components in parallel. In: Rolim, J. (ed.) IPDPS 2000. LNCS, vol. 1800, pp. 505–511. Springer, Heidelberg (2000). doi:10.​1007/​3-540-45591-4_​68 CrossRef
11.
Gaiser, A., Schwoon, S.: Comparison of Algorithms for Checking Emptiness on Büchi Automata. CoRR abs/0910.3766 (2009)
12.
Geldenhuys, J., Valmari, A.: Tarjan’s algorithm makes on-the-fly LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 2988, pp. 205–219. Springer, Heidelberg (2004)CrossRef
13.
Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002). doi:10.​1007/​3-540-36135-9_​20 CrossRef
14.
Holzmann, G., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845–857 (2011)CrossRef
15.
Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: Proceedings of the Second SPIN Workshop, vol. 32, pp. 81–89 (1996)
16.
Hong, S., Rodia, N., Olukotun, K.: On fast parallel detection of strongly connected components (SCC) in small-world graphs. In: 2013 International Conference High Performance Computing, Networking, Storage and Analysis (SC), pp. 1–11 (2013)
17.
Kant, G., Laarman, A., Meijer, J., Pol, J., Blom, S., Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​61
18.
Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Trinh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest (2016)
19.
Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Linard, A., Beccuti, M., Hamez, A., Lopez-Bobeda, E., Jezequel, L., Meijer, J., Paviot-Adet, E., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Wolf, K.: Complete Results for the 2015 Edition of the Model Checking Contest (2015)
20.
Laarman, A., Langerak, R., Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 321–335. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-24372-1_​23 CrossRef
21.
Laarman, A., van de Pol, J.: Variations on multi-core nested depth-first search. In: Barnat, J., Heljanko, K. (eds.) PDMC 2011. EPTCS, vol. 72, pp. 13–28 (2011)
22.
Laarman, A., Pol, J., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506–511. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-20398-5_​40 CrossRef
23.
Lowe, G.: Concurrent depth-first search algorithms based on Tarjan’s algorithm. Int. J. Softw. Tools Technol. Transf. 18(2), 1–19 (2015)
24.
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, PODC 1987, p. 205. ACM (1987)
25.
Orzan, S.: On Distributed Verification and Verified Distribution. Ph.D. thesis (2004)
26.
27.
Pelánek, R.: Properties of state spaces and their applications. Int. J. Softw. Tools Technol. Transf. 10(5), 443–454 (2008)CrossRef
28.
Rao, V.N., Kumar, V.: Superlinear speedup in parallel state-space search. In: Nori, K.V., Kumar, S. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 338, pp. 161–174. Springer, Heidelberg (1988)CrossRef
29.
Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 613–627. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​56
30.
31.
Schudy, W.: Finding strongly connected components in parallel using O(log2n) reachability queries. In: Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, SPAA 2008, pp. 146–151. ACM (2008)
32.
33.
Slota, G.M., Rajamanickam, S., Madduri, K.: BFS and coloring-based parallel algorithms for strongly connected components and related problems. In: 2014 IEEE 28th International Parallel and Distributed Processing Symposium, pp. 550–559 (2014)
34.
35.
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science, pp. 322–331. IEEE Computer Society (1986)
36.
Černá, I., Pelánek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 318–327. Springer, Heidelberg (2003). doi:10.​1007/​978-3-540-45138-9_​26 CrossRef
Metadaten
Titel
Multi-core SCC-Based LTL Model Checking
verfasst von
Vincent Bloemen
Jaco van de Pol
Copyright-Jahr
2016
Buch
Hardware and Software: Verification and Testing

Print ISBN: 978-3-319-49051-9

Electronic ISBN: 978-3-319-49052-6

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-49052-6_2