AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL

The correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more convenient to specify the correct behavior of packets than the global behavior of the entire network. Petri nets with trans...

Descripción completa

Detalles Bibliográficos
Autores principales: Finkbeiner, Bernd, Gieseking, Manuel, Hecking-Harbusch, Jesko, Olderog, Ernst-Rüdiger
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363180/
http://dx.doi.org/10.1007/978-3-030-53291-8_5
_version_ 1783559618402713600
author Finkbeiner, Bernd
Gieseking, Manuel
Hecking-Harbusch, Jesko
Olderog, Ernst-Rüdiger
author_facet Finkbeiner, Bernd
Gieseking, Manuel
Hecking-Harbusch, Jesko
Olderog, Ernst-Rüdiger
author_sort Finkbeiner, Bernd
collection PubMed
description The correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more convenient to specify the correct behavior of packets than the global behavior of the entire network. Petri nets with transits extend Petri nets and Flow-LTL extends LTL such that the data flows of tokens can be tracked. We present the tool AdamMC as the first model checker for Petri nets with transits against Flow-LTL. We describe how AdamMC can automatically encode concurrent updates of software-defined networks as Petri nets with transits and how common network specifications can be expressed in Flow-LTL. Underlying AdamMC is a reduction to a circuit model checking problem. We introduce a new reduction method that results in tremendous performance improvements compared to a previous prototype. Thereby, AdamMC can handle software-defined networks with up to 82 switches.
format Online
Article
Text
id pubmed-7363180
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73631802020-07-16 AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL Finkbeiner, Bernd Gieseking, Manuel Hecking-Harbusch, Jesko Olderog, Ernst-Rüdiger Computer Aided Verification Article The correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more convenient to specify the correct behavior of packets than the global behavior of the entire network. Petri nets with transits extend Petri nets and Flow-LTL extends LTL such that the data flows of tokens can be tracked. We present the tool AdamMC as the first model checker for Petri nets with transits against Flow-LTL. We describe how AdamMC can automatically encode concurrent updates of software-defined networks as Petri nets with transits and how common network specifications can be expressed in Flow-LTL. Underlying AdamMC is a reduction to a circuit model checking problem. We introduce a new reduction method that results in tremendous performance improvements compared to a previous prototype. Thereby, AdamMC can handle software-defined networks with up to 82 switches. 2020-06-16 /pmc/articles/PMC7363180/ http://dx.doi.org/10.1007/978-3-030-53291-8_5 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Finkbeiner, Bernd
Gieseking, Manuel
Hecking-Harbusch, Jesko
Olderog, Ernst-Rüdiger
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
title AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
title_full AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
title_fullStr AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
title_full_unstemmed AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
title_short AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
title_sort adammc: a model checker for petri nets with transits against flow-ltl
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363180/
http://dx.doi.org/10.1007/978-3-030-53291-8_5
work_keys_str_mv AT finkbeinerbernd adammcamodelcheckerforpetrinetswithtransitsagainstflowltl
AT giesekingmanuel adammcamodelcheckerforpetrinetswithtransitsagainstflowltl
AT heckingharbuschjesko adammcamodelcheckerforpetrinetswithtransitsagainstflowltl
AT olderogernstrudiger adammcamodelcheckerforpetrinetswithtransitsagainstflowltl

Ejemplares similares