Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

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

  • Competitions and Challenges
  • TOOLympics 2019
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4

Similar content being viewed by others

Notes

  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.

  3. https://cadp.inria.fr/man/caesar.bdd.html

  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].

  6. https://mcc.lip6.fr/bibliography.php#references

  7. http://project-coco.uibk.ac.at

  8. https://maxsat-evaluations.github.io

  9. http://www.qbflib.org/index_eval.php

  10. http://www.satcompetition.org

References

  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. Balint, A., Belov, A., Järvisalo, M., Sinz, C.: Sat challenge 2012 (2012). https://baldur.iti.kit.edu/SAT-Challenge-2012

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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. Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1–29 (2019). https://doi.org/10.1007/s10009-017-0469-y

    Article  Google Scholar 

  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. Bjørner, N., Benney, E., Gupta, A., Horrocks, I., Iannni, G., Le Berre, D., Wakdmann, J.: Starexec (2020). https://www.starexec.org/starexec/public/about.jsp

  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)

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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. enPAC git-hug page (2020). https://github.com/Tj-Cong/enPAC

  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. Garavel, H.: Nested-unit petri nets. J. Log. Algebr. Meth. Program. 104, 60–85 (2019)

    Article  MathSciNet  Google Scholar 

  34. Girault, C., Valk, R.: Petri nets for systems engineering - a guide to modeling, verification, and applications. Springer (2003). http://www.springer.com/computer/swe/book/978-3-540-41217-5

  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)

    Google Scholar 

  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. Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Jézéquel, L., Paviot-adet, E.: The Model Checking Contest (2019). https://mcc.lip6.fr

  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)

    Article  Google Scholar 

  59. Murata, T.: Petri nets: Properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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. The international SAT competition web page (2020). http://www.satcompetition.org

  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)

Download references

Acknowledgements

The authors would like to thank the developers of the tools participating in the model checking contest since the beginning to make this event successful. We, more particularly, thank the developers participating between 2015 and 2019 for their kindness while answering our questions about some technical details on their tools.

Author information

Authors and Affiliations

  1. CNRS, LIP66, Sorbonne Université, 75005, Paris, France

    Fabrice Kordon, Lom Messan Hillah, Francis Hulin-Hubard & Emmanuel Paviot-Adet

  2. Université Paris Nanterre, 92001, Nanterre, France

    Lom Messan Hillah

  3. LS2N, UMR CNRS 6004, Université de Nantes, 44321, Nantes, France

    Loïg Jezequel

  4. Université de Paris, 75005, Paris, France

    Emmanuel Paviot-Adet

Authors
  1. Fabrice Kordon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lom Messan Hillah
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Francis Hulin-Hubard
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Loïg Jezequel
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Emmanuel Paviot-Adet
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fabrice Kordon.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

The authors thank the following organizations for having lent powerful computers to process all the experiments of the Model Checking Contest over the years: Rostock University, Sorbonne Université, Université de Genève, Université Paris Nanterre, University of Twente.

A: Detailed description of additional techniques reported in Sect. 3

A: Detailed description of additional techniques reported in Sect. 3

Abstractions This technique denotes a family of methods that perform abstract reasoning on the model so that a decision about the expected result can be taken rapidly. Typical examples of abstractions are: Bounded model checking, K-induction, and counterexample-guided abstraction refinement (CEGAR).

Bounded model checking [22] deals with the encoding of the system and its properties into a satisfiability problem which is then processed, typically by a SAT or SMT solver. Usually, the transition relation is encoded up to a certain bound with the hope of finding a counterexample. It is a semi-decision algorithm often coupled with K-induction.

K-induction is a SAT-based analysis technique [55] performed in two steps. First, the analyzed property must hold for any sequence of K steps starting from the initial state; then, the SAT solver is used to verify that any path with the property satisfied for K consecutive states, always leads to a K+1 state, that also satisfies the property.

CEGAR [23] consists in checking the property of a system at a coarse (imprecise) abstraction level. If a counterexample is found, the tool checks for its feasibility (e.g., checks if the violation is due to the imprecision of the abstraction or not). If the counterexample is not feasible, then the abstraction must be refined to exclude the false counterexample and then the property must be checked again.

Compression This technique denotes a family of methods that replace a state space S with another (simplified) state space \(S'\) such that S and \(S'\) are related in a way (e.g., simulation, bisimulation) so that results obtained for \(S'\) imply validity of the results in S [46]. We distinguish decision diagrams and structural reductions from compression.

Linear programming This technique denotes the use of linear programming to answer or reduce some queries without exploring the state space.

Unfolding the system into a prefix graph [58]. This technique provides a very efficient representation of the state space generated by a Petri net model using a variant on the same notation. It allows to represent infinite state spaces in a finite way and is also quite useful for very large systems [29, 30].

Partial order reduction This technique denotes a family of methods that reduce the size of the state space [35], by exploiting the commutativity of concurrently executed transitions. Usually, such commutativity generates a large number of paths from a given state s to another one \(s'\) in the state space. Among the partial order techniques, there are stubborn set [73] and ample sets [61].

Query reduction This technique denotes a family of methods that reduce the size of a query without the need of explicitly searching through the state-space, for example using state equations, detecting tautologies, and formula rewriting [3, 16].

Use of satisfiability This technique denotes the use of satisfiability for the optimization of the transition relations or of the formula to be verified in order to speed up the model checking. A typical example is the use of SMT solvers in the context of linear-programming. It is also useful to check for the deadlock freeness of a specification.

Structural reductions Some tools perform structural reductions on the input specification before performing the model checking itself. Berthelot’s reductions [8] or Haddad’s reductions [36] are typical examples of such transformations. Of course, such reductions must happen in situations where they preserve the properties to be checked.

Topological analysis Structural information may be extracted from the model (e.g., traps/deadlocks, state equation) and used to speed up the analysis or over-approximate the state space [59].

A good example and application of topological analysis is variable reordering when dealing with the encoding of the model, for example into decision diagrams [43]. It is also mentioned as a way to optimize state compression techniques.

Petri net properties like invariants, siphons or traps, as well as NUPN information or the definitions of types in colored Petri nets are typical topological information considered by tools in the MCC.

1.1 B: Instances of models used in the MCC Benchmark to evaluate the hardness of the verification tasks (Sect. 7.3)

The following instances of model have been selected for the analysis presented in Sect. 7.3:

  • ARMCacheCoherence-PT-none

  • Angiogenesis-PT-50

  • BridgeAndVehicles-COL-V80P50N50

  • BridgeAndVehicles-PT-V80P50N50

  • CSRepetitions-COL-10

  • CSRepetitions-PT-10

  • CircadianClock-PT-100000

  • CircularTrains-PT-768

  • DatabaseWithMutex-COL-40

  • DatabaseWithMutex-PT-40

  • Dekker-PT-200

  • Diffusion2D-PT-D50N150

  • DrinkVendingMachine-COL-98

  • DrinkVendingMachine-PT-10

  • ERK-PT-100000

  • Echo-PT-d02r19

  • Echo-PT-d05r03

  • EnergyBus-PT-none

  • Eratosthenes-PT-500

  • FMS-PT-500

  • GlobalResAllocation-COL-11

  • GlobalResAllocation-PT-05

  • HypercubeGrid-PT-C3K4P4B12

  • HypercubeGrid-PT-C5K3P3B15

  • IBM319-PT-none

  • IBM5964-PT-none

  • IBM703-PT-none

  • IBMB2S565S3960-PT-none

  • IOTPpurchase-PT-C12M10P15D17

  • Kanban-PT-1000

  • LamportFastMutEx-COL-8

  • LamportFastMutEx-PT-8

  • MultiwaySync-PT-none

  • NeoElection-COL-8

  • NeoElection-PT-8

  • ParamProductionCell-PT-5

  • Parking-PT-864

  • PermAdmissibility-COL-50

  • PermAdmissibility-PT-50

  • Peterson-COL-7

  • Peterson-PT-7

  • PhaseVariation-PT-D30CS100

  • Philosophers-COL-100000

  • Philosophers-PT-010000

  • PhilosophersDyn-COL-80

  • PhilosophersDyn-PT-20

  • Planning-PT-none

  • PolyORBLF-COL-S04J06T10

  • PolyORBLF-COL-S06J06T08

  • PolyORBLF-PT-S04J06T10

  • PolyORBLF-PT-S06J06T08

  • PolyORBNT-COL-S10J80

  • PolyORBNT-PT-S10J80

  • ProductionCell-PT-none

  • QuasiCertifProtocol-COL-32

  • QuasiCertifProtocol-PT-32

  • Raft-PT-10

  • Railroad-PT-100

  • ResAllocation-PT-R003C100

  • ResAllocation-PT-R100C002

  • Ring-PT-none

  • RwMutex-PT-r2000w0010

  • SafeBus-COL-80

  • SafeBus-PT-20

  • SharedMemory-COL-100000

  • SharedMemory-PT-000200

  • SimpleLoadBal-PT-20

  • SmallOperatingSystem-PT-MT8192DC4096

  • Solitaire-PT-EngCT7x7

  • Solitaire-PT-EngNC7x7

  • Solitaire-PT-FrnCT7x7

  • Solitaire-PT-FrnNC7x7

  • Solitaire-PT-SqrCT5x5

  • Solitaire-PT-SqrNC5x5

  • SquareGrid-PT-130613

  • SwimmingPool-PT-10

  • TokenRing-COL-500

  • TokenRing-PT-050

  • UtahNoC-PT-none

  • Vasy2003-PT-none

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Kordon, F., Hillah, L.M., Hulin-Hubard, F. et al. Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019. Int J Softw Tools Technol Transfer 23, 931–952 (2021). https://doi.org/10.1007/s10009-021-00615-1

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-021-00615-1

Keywords

Search

Navigation