Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
International Journal on Software Tools for Technology Transfer
Published 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

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

Published in: International Journal on Software Tools for Technology Transfer | Issue 6/2021

Log in

Activate our intelligent search to find suitable subject content or patents.

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.
previous article The RERS challenge: towards controllable and scalable benchmark synthesis

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Appendix
Available only for authorised users
Footnotes
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].
 
Literature
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.
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)
Metadata
Title
Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019
Authors
Fabrice Kordon
Lom Messan Hillah
Francis Hulin-Hubard
Loïg Jezequel
Emmanuel Paviot-Adet
Publication date
01-06-2021
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 6/2021
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-021-00615-1

Other articles of this Issue 6/2021

International Journal on Software Tools for Technology Transfer 6/2021 Go to the issue

Competitions and Challenges

The RERS challenge: towards controllable and scalable benchmark synthesis

Competitions and Challenges

KLEE symbolic execution engine in 2019

Competitions and Challenges

CoCo 2019: report on the eighth confluence competition

Competitions and Challenges

First international competition on software testing

Competitions and Challenges

TOOLympics II: competitions on formal methods

Competitions and Challenges

SL-COMP: competition of solvers for separation logic

Premium Partner

    Image Credits