research-article

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-AdetAuthors Info & Claims

International Journal on Software Tools for Technology Transfer, Volume 23, Issue 6

Pages 931 - 952

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

Published: 01 December 2021 Publication History

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.

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

ω

-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, and Sinz C Overview and analysis of the SAT challenge 2012 solver competition Artificual Intelligence 2015 223 120-155

[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 PO, and Vernadat F The tool TINA-construction of abstract state spaces for Petri nets and Time Petri nets In. J. Prod. Res. 2004 42 14 2741-2756

[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, and Wendler P Reliable benchmarking: requirements and solutions Int. J. Softw. Tools Technol. Transf. 2019 21 1 1-29

[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. 1986 35 8 677-691

[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, and Haddad S A symbolic reachability graph for coloured Petri nets Theor. Comput. Sci. 1997 176 1–2 39-65

[21]

Ciardo G, Miner AS, and Wan M Advanced features in SMART: the stochastic model checking analyzer for reliability and timing SIGMETRICS Perform. Eval. Rev. 2009 36 4 58-63

[22]

Clarke EM, Biere A, Raimi R, and Zhu Y Bounded model checking using satisfiability solving Form. Methods Sys. Des. 2001 19 1 7-34

[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

ω

-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. 2019 104 60-85

[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 LM, Kindler E, Kordon F, Petrucci L, and Trèves N A primer on the Petri Net Markup Language and ISO/IEC 15909–2 Petri Net Newsl. 2009 76 9-28

[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 KL A technique of state space search based on unfolding Form. Methods Syst. Des. 1995 6 1 45-65

[59]

Murata T Petri nets: Properties, analysis and applications Proc. IEEE 1989 77 4 541-580

[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 DG, and Levesque HJ Generating hard satisfiability problems Artif. Intell. 1996 81 1–2 17-29

[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. 2017 30 419-432

[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)

Cited By

Amat NAmparore EBerthomieu BBouvier PZilio SHulin-Hubard FJensen PJezequel LKordon FLi SPaviot-Adet EPetrucci LSrba JThierry-Mieg YWolf K(2024)Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023TOOLympics Challenge 202310.1007/978-3-031-67695-6_3(52-89)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_3
André ÉArias JBarbot BHulin-Hubard FKordon FLe VPetrucci L(2024)CosyVerif: The Path to Formalisms CohabitationApplication and Theory of Petri Nets and Concurrency10.1007/978-3-031-61433-0_21(432-444)Online publication date: 26-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-61433-0_21
Amat NZilio S(2023)SMPT: A Testbed for Reachability Methods in Generalized Petri NetsFormal Methods10.1007/978-3-031-27481-7_25(445-453)Online publication date: 6-Mar-2023
https://dl.acm.org/doi/10.1007/978-3-031-27481-7_25

Index Terms

Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Index terms have been assigned to the content through auto-classification.

Recommendations

Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering

Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Combining Theorem Proving with Model Checking through Predicate Abstraction

This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal on Software Tools for Technology Transfer (STTT)

International Journal on Software Tools for Technology Transfer (STTT) Volume 23, Issue 6

Dec 2021

117 pages

ISSN:1433-2779

EISSN:1433-2787

Issue’s Table of Contents

© The Author(s), under exclusive licence to Springer-Verlag GmbH Germany, part of Springer Nature 2021.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 December 2021

Accepted: 06 May 2021

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Amat NAmparore EBerthomieu BBouvier PZilio SHulin-Hubard FJensen PJezequel LKordon FLi SPaviot-Adet EPetrucci LSrba JThierry-Mieg YWolf K(2024)Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023TOOLympics Challenge 202310.1007/978-3-031-67695-6_3(52-89)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_3
André ÉArias JBarbot BHulin-Hubard FKordon FLe VPetrucci L(2024)CosyVerif: The Path to Formalisms CohabitationApplication and Theory of Petri Nets and Concurrency10.1007/978-3-031-61433-0_21(432-444)Online publication date: 26-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-61433-0_21
Amat NZilio S(2023)SMPT: A Testbed for Reachability Methods in Generalized Petri NetsFormal Methods10.1007/978-3-031-27481-7_25(445-453)Online publication date: 6-Mar-2023
https://dl.acm.org/doi/10.1007/978-3-031-27481-7_25

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents