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
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 6/2021

01.06.2021 | Competitions and Challenges

Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019

verfasst von: Fabrice Kordon, Lom Messan Hillah, Francis Hulin-Hubard, Loïg Jezequel, Emmanuel Paviot-Adet

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2021

Einloggen

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

search-config
loading …

Abstract

In various scientific communities dealing with formal analysis, software competitions have emerged and contributed to fostering progress in state of the art and providing insight into the evolution of the involved technologies. The model checking contest (MCC) is one of them; it focuses on asynchronous concurrent systems. This paper reports what the organizers have observed over five editions of the MCC between 2015 and 2019. It shows the evolution of state-of-the-art model checking tools in performing large and difficult verification tasks by improving existing techniques or designing new and innovative (combinations of) techniques. This paper also shows the impact of such an event on the corresponding scientific community.
Vorheriger Artikel The RERS challenge: towards controllable and scalable benchmark synthesis

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
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
From 2015 to 2018, Deadlock detection was part of the reachability examination. It moved into a dedicated category that requested only deadlock detection in 2019, but groups several generic properties in 2020. To be consistent with the 2019 presentation scheme, we only refer in this paper to “deadlock”, while detailed results in [49] are provided differently or as a part of other examinations.
 
2
In 2015, Upper bounds computation was part of the reachability examination, but became a distinct one in 2016. To be consistent with the 2019 presentation scheme, we only refer in this paper to “Upper bounds”, while detailed results in [49] are provided as a part of another examination in 2015.
 
4
Results are globally expressed in the 2019 way. For instance, deadlock detection was part of the reachability examination before 2019 so the corresponding data are not explicitly displayed on the MCC web site. Similarly, in 2015, computation of upper bounds was also part of the reachability examination and thus not noted explicitly on the MCC web site.
 
5
Until 2019, the formula generation did not support the categories Reactivity and Obligation in the Manna&Pnueli classification [57].
 
Literatur
1.
Amendola, G., Ricca, F., Truszczynski, M.: A generator of hard 2qbf formulas and ASP programs. In: 16th International Conference on Principles of Knowledge Representation and Reasoning, pp. 52–56. AAAI Press (2018)
2.
Amparore, E.G., Balbo, G., Beccuti, M., Donatelli, S., Franceschinis, G.: 30 years of GreatSPN. In: Principles of Performance and Reliability Modeling and Evaluation, pp. 227–254. Springer (2016)
3.
Baarir, S., Duret-Lutz, A.: Sat-based minimization of deterministic \(\omega \)-automata. In: 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, vol. 9450, pp. 79–87. Springer (2015)
4.
Babar, J., Beccuti, M., Donatelli, S., Miner, A.S.: GreatSPN Enhanced with Decision Diagram Data Structures. In: 31st International Conference on Applications and Theory of Petri Nets, Lecture Notes in Computer Science, vol. 6128, pp. 308–317. Springer (2010)
5.
6.
Balint, A., Belov, A., Järvisalo, M., Sinz, C.: Overview and analysis of the SAT challenge 2012 solver competition. Artificual Intelligence 223, 120–155 (2015)CrossRef
7.
Barrett, C., de Moura, L., Stump, A.: Smt-comp: Satisfiability modulo theories competition. In: 17th International Conference on Computer Aided Verification—CAV, Lecture Notes in Computer Science, vol. 3576, pp. 20–23. Springer (2005)
8.
Berthelot, G., Roucairol, G.: Reduction of Petri Nets. In: 5th Symposium on Mathematical Foundations of Computer Science 1976, Lecture Notes in Computer Science, vol. 45, pp. 202–209. Springer (1976)
9.
Berthomieu, B., Botlan, D.L., Dal-Zilio, S.: Petri net reductions for counting markings. In: 25th International Symposium on Model Checking Software (SPIN), Lecture Notes in Computer Science, vol. 10869, pp. 65–84. Springer (2018)
10.
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA-construction of abstract state spaces for Petri nets and Time Petri nets. In. J. Prod. Res. 42(14), 2741–2756 (2004)CrossRef
11.
Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.): Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics. Lecture Notes in Computer Science, vol. 11429. Springer (2019)
12.
13.
Beyer, D., Wendler, P.: CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 12079, pp. 126–133. Springer (2020)
14.
Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: FMCAD, p. 9. IEEE (2017)
15.
16.
Bønneland, F., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Simplification of CTL formulae for efficient model checking of petri nets. In: 39th International Conference on Application and Theory of Petri Nets and Concurrency, Lecture Notes in Computer Science, vol. 10877, pp. 143–163. Springer (2018)
17.
Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRef
18.
Buchs, D., Klikovits, S., Linard, A., Mencattini, R., Racordon, D.: A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning. In: 39th International Conference on Application and Theory of Petri Nets and Concurrency, Lecture Notes in Computer Science, vol. 10877, pp. 385–395. Springer (2018)
19.
Burch, J., Clarke, E., McMillan, K.: Symbolic model checking: \(10^{20}\) states and beyond. Information and Computation (Special issue for best papers from LICS90) 98(2), 153–181 (1992)
20.
Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: A symbolic reachability graph for coloured Petri nets. Theor. Comput. Sci. 176(1–2), 39–65 (1997)MathSciNetCrossRef
21.
Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS Perform. Eval. Rev. 36(4), 58–63 (2009)CrossRef
22.
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Sys. Des. 19(1), 7–34 (2001)CrossRef
23.
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: 12th International Conference on Computer Aided Verification—CAV, Lecture Notes in Computer Science, vol. 1855, pp. 154–169. Springer (2000)
24.
Colange, M., Hillah, L.M., Kordon, F., Parutto, P.: Extreme Symmetries in Complex Distributed Systems: the Bag-Oriented Approach. In: 17th Monterey Workshop : Development. Operation and Management of Large-Scale Complex IT Systems, Revised Selected Papers, Lecture Notes in Computer Science, vol. 7539, pp. 330–352. Springer, Oxford, UK (2012)
25.
Couvreur, J., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: 25th International Conference on Formal Techniques for Networked and Distributed Systems—FORTE, Lecture Notes in Computer Science, vol. 3731, pp. 443–457. Springer (2005)
26.
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - A framework for LTL and \(\omega \)-automata manipulation. In: 14th International Symposium on Automated Technology for Verification and Analysis—ATVA, Lecture Notes in Computer Science, vol. 9938, pp. 122–129 (2016)
27.
28.
Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: Verifythis—verification competition with a human factor. In: Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics, Lecture Notes in Computer Science, vol. 11429, pp. 176–195. Springer (2019)
29.
Esparza, J., Hoffmann, P.: Reduction rules for colored workflow nets. In: 19th International Conference on Fundamental Approaches to Software Engineering—FASE (ETAPS), Lecture Notes in Computer Science, vol. 9633, pp. 342–358. Springer (2016)
30.
Esparza, J., Schröter, C.: Net reductions for LTL model-checking. In: 11th IFIP WG 10.5 conference in Correct Hardware Design and Verification Methods CHARME, Lecture Notes in Computer Science, vol. 2144, pp. 310–324. Springer (2001)
31.
Fehling, R.: A concept of hierarchical petri nets with building blocks. In: Advances in Petri Nets, Lecture Notes in Computer Science, vol. 674, pp. 148–168. Springer (1993)
32.
Garavel, H.: Nested-Unit Petri Nets: A structural means to increase efficiency and scalability of verification on elementary nets. In: International Conference on Application and Theory of Petri Nets and Concurrency, LNCS, vol. 9115, pp. 179–199. Springer (2015)
33.
34.
35.
Godefroid, P., Peled, D.A., Staskauskas, M.G.: Using partial-order methods in the formal validation of industrial concurrent programs. In: International Symposium on Software Testing and Analysis – ISSTA, pp. 261–269. ACM (1996)
36.
Haddad, S.: A reduction theory for coloured nets. In: Advances in Petri Nets 1989, covers the 9th European Workshop on Applications and Theory in Petri Nets, held in Venice, Italy in June 1988, selected papers, Lecture Notes in Computer Science, vol. 424, pp. 209–235. Springer (1990)
37.
Haddad, S.: Introduction: issues in verification. In: C. Girault, R. Valk (eds.) Petri Nets for Systems Engineering, A Guide to Modeling, Verification, and Applications, pp. 183–200 (2003)
38.
Haddad, S., Kordon, F., Petrucci, L., Pradat-Peyre, J.F., Trèves, N.: Efficient State-Based Analysis by Introducing Bags in Petri Net Color Domains. In: 28th American Control Conference—ACC, pp. 5018–5025. Omnipress IEEE, St-Louis, USA (2009)
39.
Hamez, A.: A Symbolic Model Checker for Petri Nets: pnmc. Transactions on Petri Nets and Other Models of Concurrency XI 297–306, (2016)
40.
Heiner, M., Rohr, C., Schwarick, M., Tovchigrechko, A.A.: Marcie’s secrets of efficient model checking. Transactions on Petri Nets and Other Models of Concurrency XI 286–296, (2016)
41.
Hillah, L., Kordon, F., Petrucci, L., Trèves, N.: PN standardisation : a survey. In: International Conference on Formal Methods for Networked and Distributed Systems—FORTE. Lecture Notes in Computer Science, vol. 4229, pp. 307–322. Springer Verlag, Paris, France (2006)
42.
Hillah, L.M., Kindler, E., Kordon, F., Petrucci, L., Trèves, N.: A primer on the Petri Net Markup Language and ISO/IEC 15909–2. Petri Net Newsl. 76, 9–28 (2009)
43.
Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a hierarchical static order for decision diagram-based representation from P/T nets. Transactions on Petri Nets and Other Models of Concurrency V 121–140, (2012)
44.
Jasper, M., Mues, M., Murtovi, A., Schlüter, M., Howar, F., Steffen, B., Schordan, M., Hendriks, D., Schiffelers, R.R.H., Kuppens, H., Vaandrager, F.W.: RERS 2019: Combining synthesis with real-world models. In: Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics, Lecture Notes in Computer Science, vol. 11429, pp. 101–115. Springer (2019)
45.
Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P/T nets. Transactions on Petri Nets and Other Models of Concurrency XI 307–318, (2016)
46.
Jensen, P.G., Larsen, K.G., Srba, J.: PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing. In: 14th International Colloquium on Theoretical Aspects of Computing—ICTAC, Lecture Notes in Computer Science, vol. 10580, pp. 248–265. Springer (2017)
47.
Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: Ltsmin: High-performance language-independent model checking. In: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems—TACAS (ETAPS), Lecture Notes in Computer Science, vol. 9035, pp. 692–707. Springer (2015)
48.
Kordon, F., Garavel, H., Hillah, L., Paviot-Adet, E., Jezequel, L., Hulin-Hubard, F., Amparore, E.G., Beccuti, M., Berthomieu, B., Evrard, H., Jensen, P.G., Botlan, D.L., Liebke, T., Meijer, J., Srba, J., Thierry-Mieg, Y., van de Pol, J., Wolf, K.: Mcc’2017—the seventh model checking contest. Transactions on Petri Nets and Other Models of Concurrency XIII 181–209, (2018)
49.
50.
Kordon, F., Hulin-Hubard, F.: BenchKit, a Tool for Massive Concurrent Benchmarking. In: 14th International Conference on Application of Concurrency to System Design—ACSD, pp. 159–165. IEEE Computer Society (2014)
51.
Kordon, F., Leuschel, M., van de Pol, J., Thierry-Mieg, Y.: Software Architecture of Modern Model Checkers. In: B. Steffen, G.J. Woeginger (eds.) Computing and Software Science—State of the Art and Perspectives, Lecture Notes in Computer Science, vol. 10000, pp. 393–419. Springer (2019)
52.
Kordon, F., Peyre, J.F.: Process decomposition for Rapid Prototyping of Parallel systems. In: Proceedings of the 6th International Symposium on Computer and Information Science, Kener, Antalya, Turkey (1991)
53.
Kordon, F., van de Pol, J., Seidl, M.: Lorentz workshop, advancing verification competitions as a scientific method (2019)
54.
Le, D., Nguyen, H., Nguyen, V., Mai, P., Pham-Duy, B., Quan, T., André, É., Petrucci, L., Liu, Y.: Pecan: Compositional verification of petri nets made easy. In: 12th International Symposium on Automated Technology for Verification and Analysis—ATVA, Lecture Notes in Computer Science, vol. 8837, pp. 242–247. Springer (2014)
55.
Leino, R.: Dafny: An automatic program verifier for functional correctness. In: 16th International Conference on Logic Programming and Automated Reasoning—LPAR, Lecture Notes in Artificial Intelligence, vol. 6355, pp. 348–370. Springer (2010)
56.
López Bóbeda, E., Colange, M., Buchs, D.: Stratagem: A generic petri net verification framework. In: 35th International Conference on Application and Theory of Petri Nets and Concurrency—PETRI NETS. Lecture Notes in Computer Science, vol. 8489, pp. 364–373. Springer, Tunis, Tunisia (2014)
57.
Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper, 1989). In: 9th Annual ACM Symposium on Principles of Distributed Computing—PODC, pp. 377–410. ACM (1990)
58.
McMillan, K.L.: A technique of state space search based on unfolding. Form. Methods Syst. Des. 6(1), 45–65 (1995)CrossRef
59.
Murata, T.: Petri nets: Properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRef
60.
Narizzano, M., Pulina, L., Tacchella, A.: Ranking and reputation systems in the qbf competition. In: AI*IA 2007: Artificial Intelligence and Human-Oriented Computing, Lecture Notes in Artificial Intelligence, vol. 4733, pp. 97–108. Springer (2007)
61.
Peled, D.A.: All from one, one for all: on model checking using representatives. In: 5th International Conference on Computer Aided Verification—CAV, Lecture Notes in Computer Science, vol. 697, pp. 409–423. Springer (1993)
62.
Racordon, D., Buchs, D.: Verifying multi-core schedulability with data decision diagrams. In: 8th International Workshop on Software Engineering for Resilient Systems—SERENE, Lecture Notes in Computer Science, vol. 9823, pp. 45–61. Springer (2016)
63.
Rodríguez, C., Schwoon, S.: Cunf: A tool for unfolding and verifying Petri Nets with Read Arcss. In: 11th International Symposium on Automated Technology for Verification and Analysis—ATVA, Lecture Notes in Computer Science, vol. 8172, pp. 492–495. Springer (2013)
64.
Runeson, P., Höst, M.: Guidelines for conducting and reporting case study research in software engineering. Empir. Softw. Eng. 14(2), 131–164 (2009)
65.
Selman, B., Mitchell, D.G., Levesque, H.J.: Generating hard satisfiability problems. Artif. Intell. 81(1–2), 17–29 (1996)MathSciNetCrossRef
66.
Steffen, B., Jasper, M., Meijer, J., van de Pol, J.: Property-preserving generation of tailored benchmark petri nets. In: 17th International Conference on Application of Concurrency to System Design—CSD, pp. 1–8. IEEE Computer Society (2017)
67.
Sutcliffe, G.: The cade-26 automated theorem proving system competition—CASC-26. AI Commun. 30, 419–432 (2017)MathSciNetCrossRef
68.
Thierry-Mieg, Y.: Symbolic Model-Checking Using ITS-Tools. In: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems—TACAS (ETAPS), Lecture Notes in Computer Science, vol. 9035, pp. 231–237. Springer (2015)
69.
Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical set decision diagrams and regular models. In: 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems—TACAS (ETAPS), Lecture Notes in Computer Science, vol. 5505, pp. 1–15. Springer (2009)
70.
71.
van Dijk, T., van de Pol, J.: Multi-core decision diagrams. In: Y. Hamadi, L. Sais (eds.) Handbook of Parallel Constraint Reasoning., pp. 509–545 (2018)
72.
Valk, R.: Object petri nets. In: Advances in Petri Nets, Lecture Notes in Computer Science, vol. 3098, pp. 819–848. Springer (2004)
73.
Valmari, A.: A stubborn attack on state explosion. In: Computer Aided Verification, 2nd International Workshop—CAV, Lecture Notes in Computer Science, vol. 531, pp. 156–165. Springer (1991)
74.
Wolf, K.: Petri Net Model Checking with LoLA 2. In: 39th International Conference on Application and Theory of Petri Nets and Concurrency—PETRI NETS, Lecture Notes in Computer Science, vol. 10877, pp. 351–362. Springer (2018)
75.
Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Evaluating component solver contributions to portfolio-based algorithm selectors. In: 15th International Conference on Theory and Applications of Satisfiability Testing—SAT 2012, Lecture Notes in Computer Science, vol. 7317, pp. 228–241. Springer (2012)
Metadaten
Titel
Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019
verfasst von
Fabrice Kordon
Lom Messan Hillah
Francis Hulin-Hubard
Loïg Jezequel
Emmanuel Paviot-Adet
Publikationsdatum
01.06.2021
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 6/2021
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-021-00615-1

Weitere Artikel der Ausgabe 6/2021

International Journal on Software Tools for Technology Transfer 6/2021 Zur Ausgabe

Introduction

TOOLympics I: Competition on software testing

Competitions and Challenges

CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation

Competitions and Challenges

Symbiotic  6: generating test cases by slicing and symbolic execution

Competitions and Challenges

KLEE symbolic execution engine in 2019

Competitions and Challenges

Plain random test generation with PRTest

Competitions and Challenges

The RERS challenge: towards controllable and scalable benchmark synthesis

Premium Partner

    Bildnachweise