Top

Published in:

2018 | OriginalPaper | Chapter

A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning

Authors : Didier Buchs, Stefan Klikovits, Alban Linard, Romain Mencattini, Dimitri Racordon

Published in: Application and Theory of Petri Nets and Concurrency

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

This paper introduces mcc4mcc, the Model Checker Collection for the Model Checking Contest, a tool that wraps multiple model checking solutions, and applies the most appropriate one based on the characteristics of the model it is given. It leverages machine learning algorithms to carry out this selection, based on the results gathered from the 2017 edition of the Model Checking Contest, an annual event in which multiple tools compete to verify different properties on a large variety of models. Our approach brings two important contributions. First, our tool offers the opportunity to further investigate on the relation between model characteristics and verification techniques. Second, it lays out the groundwork for a unified way to distribute model checking software using virtual containers.

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

previous chapter LocalProcessModelDiscovery: Bringing Petri Nets to the Pattern Mining World

next chapter Arduino Library Developed for Petri Net Inserted into RFID Database and Variants

https://www.docker.com/.

https://en.wikipedia.org/wiki/Secure_Shell.

https://www.docker.com.

https://docs.docker.com/engine/reference/builder/.

https://github.com/cui-unige/mcc4mcc.

https://hub.docker.com/.

https://mcc.lip6.fr/2017/results.php.

https://github.com/cui-unige/mcc4mcc.

André, É., Lembachar, Y., Petrucci, L., Hulin-Hubard, F., Linard, A., Hillah, L., Kordon, F.: Cosyverif: an open source extensible verification environment. In: 2013 18th International Conference on Engineering of Complex Computer Systems, Singapore, 17–19 July 2013, pp. 33–36. IEEE Computer Society (2013)

Bernstein, D.: Containers and cloud: from LXC to Docker to Kubernetes. IEEE Cloud Comput. 1(3), 81–84 (2014)CrossRef

Berthomieu, B., Vernadat, F.: Time Petri nets analysis with TINA. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), Riverside, California, USA, 11–14 September 2006, pp. 123–124. IEEE Computer Society (2006)

López Bóbeda, E., Colange, M., Buchs, D.: StrataGEM: a generic Petri net verification framework. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 364–373. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07734-5_20CrossRefMATH

Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and Regression Trees. Wadsworth, Belmont (1984)MATH

Broemeling, L.D.: Bayesian Analysis of Linear Models. Statistics: A Series of Textbooks and Monographs. Taylor & Francis, London (1984). https://books.google.ch/books?id=b8wPjIm9wcYCMATH

Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: graphical editor and analyzer for timed and stochastic Petri nets. Perform. Eval. 24(1–2), 47–68 (1995)CrossRef

Ciardo, G., Miner, A.S.: SMART: the stochastic model checking analyzer for reliability and timing. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), Enschede, The Netherlands, 27–30 September 2004, pp. 338–339. IEEE Computer Society (2004)

Cristianini, N., Shawe-Taylor, J.: An Introduction to Support Vector Machines and Other Kernel-based Learning Methods. Cambridge University Press, Cambridge (2010)MATH

10.

Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 - a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_8CrossRef

11.

Heiner, M., Rohr, C., Schwarick, M.: MARCIE – model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389–399. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38697-8_21CrossRef

12.

Hillah, L.M., Kordon, F.: Petri Nets Repository: a tool to benchmark and debug Petri Net tools. In: van der Aalst, W., Best, E. (eds.) PETRI NETS 2017. LNCS, vol. 10258, pp. 125–135. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57861-3_9CrossRef

13.

Hostettler, S., Marechal, A., Linard, A., Risoldi, M., Buchs, D.: High-level Petri net model checking with AlPiNA. Fundam. Inf. 113(3–4), 229–264 (2011)MathSciNetMATH

14.

Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P/T nets. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 307–318. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53401-4_16CrossRef

15.

Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_61CrossRef

16.

Kordon, F., et al.: Report on the model checking contest at Petri nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169–196. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35179-2_8CrossRef

17.

Kubat, M.: Neural Networks: A Comprehensive Foundation by Simon Haykin. Macmillan, Basingstoke (1994). ISBN 0-02-352781-7. Knowl. Eng. Rev. 13(4), 409–412 (1999)

18.

Linard, A., Buchs, D.: Ardoises: collaborative & interactive editing using layered data. In: 17th International Conference on Application of Concurrency to System Design, ACSD 2017, Zaragoza, Spain, June 25–30, 2017, pp. 136–145. IEEE Computer Society (2017)

19.

Mitchell, T.M.: Machine learning. McGraw Hill Series in Computer Science. McGraw-Hill, New York (1997)MATH

20.

Negus, C.: Docker Containers, 2nd edn. Addison-Wesley Professional, Boston (2015)

21.

Pan, Z., He, Q., Jiang, W., Chen, Y., Dong, Y.: Nestcloud: towards practical nested virtualization. In: 2011 International Conference on Cloud and Service Computing, CSC 2011, Hong Kong, 12–14 December 2011, pp. 321–329. IEEE Computer Society (2011)

22.

Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., Vanderplas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, E.: Scikit-learn: machine learning in Python. J. Mach. Learn. Res. 12, 2825–2830 (2011)MathSciNetMATH

23.

Racordon, D., Buchs, D.: Verifying multi-core schedulability with data decision diagrams. In: Crnkovic, I., Troubitsyna, E. (eds.) SERENE 2016. LNCS, vol. 9823, pp. 45–61. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45892-2_4CrossRef

24.

Russell, S.J., Norvig, P.: Artificial Intelligence - A Modern Approach. Prentice Hall Series in Artificial Intelligence, 2nd edn. Prentice Hall, Upper Saddle River (2003)MATH

25.

Schmidt, K.: LoLA a low level analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 465–474. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44988-4_27CrossRef

26.

Shakhnarovich, G., Darrell, T., Indyk, P.: Nearest-neighbor methods in learning and vision. IEEE Trans. Neural Netw. 19(2), 377 (2008)CrossRef

27.

Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231–237. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_20CrossRef

Title: A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning
Authors: Didier Buchs
Stefan Klikovits
Alban Linard
Romain Mencattini
Dimitri Racordon
Publisher: Springer International Publishing
Book: Application and Theory of Petri Nets and Concurrency
Print ISBN: 978-3-319-91267-7

Electronic ISBN: 978-3-319-91268-4

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-91268-4_21

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner