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:
Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Running LoLA 2.0 in a Model Checking Competition

verfasst von : Karsten Wolf

Erschienen in: Transactions on Petri Nets and Other Models of Concurrency XI

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

We report on the performance of the tool LoLA 2.0 in the model checking contest (MCC) 2015. As in the years before, LoLA ranked first in the reachability category of the contest. We identify critical success factors and discuss the impact of the contest design. Conclusions include further improvements for the tool as well as suggestions concerning the setup of future contests.

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 MCC’2015 – The Fifth Model Checking Contest
Nächstes Kapitel MARCIE’s Secrets of Efficient Model Checking
Fußnoten
1
Based on the result sheets of the MCC 2015. Not included are 290 queries that LoLA found to be equivalent to a formula without temporal operators. Such formulas could be evaluated by just inspecting the initial marking. Also not included are 603 extremely long formulas where a time limit was reached while parsing the query. Also not included is the compute-bounds subcategory.
 
Literatur
1.
Billington, J., et al.: The Petri Net Markup Language: concepts, technology, and tools. In: Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 483–505. Springer, Heidelberg (2003)CrossRef
2.
Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422–426 (1970)CrossRefMATH
3.
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)CrossRef
4.
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10{^{20}}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)MathSciNetCrossRefMATH
5.
Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)CrossRef
6.
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7–34 (2001)CrossRefMATH
7.
Das, D., Chakrabarti, P.P., Kumar, R.: Functional verification of task partitioning for multiprocessor embedded systems. ACM Trans. Des. Autom. Electr. Syst., 12(4) (2007)
8.
David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc Petri nets. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012)CrossRef
9.
10.
Fahland, D., Favre, C., Koehler, J., Lohmann, N., Völzer, H., Wolf, K.: Analysis on demand: instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70(5), 448–466 (2011)CrossRef
11.
Heiner, M., Rohr, C., Schwarick, M.: MARCIE – model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389–399. Springer, Heidelberg (2013)CrossRef
12.
Huber, P., Jensen, A.M., Jepsen, L.O., Jensen, K.: Reachability trees for high-level Petri nets. Theor. Comput. Sci. 45(3), 261–292 (1986)MathSciNetCrossRefMATH
13.
Junttila, T.A.: Computational complexity of the place/transition-net symmetry reduction method. J. UCS 7(4), 307–326 (2001)MathSciNetMATH
14.
Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645–659. Springer, Heidelberg (2010)CrossRef
15.
Kordon, F.: Report from MCC at PETRI NETS (2014)
16.
Kordon, F.: Report from MCC at PETRI NETS (2015)
17.
Kristensen, L.M., Schmidt, K., Valmari, A.: Question-guided stubborn set methods for state properties. Formal Methods Syst. Des. 29(3), 215–251 (2006)CrossRefMATH
18.
Lohmann, N., Kopp, O., Leymann, F., Reisig, W.: Analyzing BPEL4Chor: verification and participant synthesis. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 46–60. Springer, Heidelberg (2008)CrossRef
19.
Oanea, O., Wimmel, H., Wolf, K.: New algorithms for deciding the siphon-trap property. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 267–286. Springer, Heidelberg (2010)CrossRef
20.
21.
Schmidt, K.: Integrating low level symmetries into reachability analysis. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 315–330. Springer, Heidelberg (2000)CrossRef
22.
Schmidt, K.: Automated generation of a progress measure for the sweep-line method. STTT 8(3), 195–203 (2006)CrossRef
23.
Stahl, C., Reisig, W., Krstic, M.: Hazard detection in a GALS wrapper: a case study. In: Proceedings of ACSD. IEEE (2005)
24.
Talcott, C., Dill, D.L.: The pathway logic assistant. In: Proceedings of Computational Methods in Systems Biology (2005)
25.
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1989)CrossRef
26.
Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Logical Meth. Comput. Sci. 8(3) (2012)
27.
Wolf, K.: Generating Petri net state spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 29–42. Springer, Heidelberg (2007)CrossRef
Metadaten
Titel
Running LoLA 2.0 in a Model Checking Competition
verfasst von
Karsten Wolf
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Transactions on Petri Nets and Other Models of Concurrency XI

Print ISBN: 978-3-662-53400-7

Electronic ISBN: 978-3-662-53401-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-662-53401-4_13