Navigation

AdamMC

Overview

Current Version:

adamMC_v0.tar.gz

Documentation:

User's Guide

Theoretical Background

Contact:

Manomuel1xw Gieseking (manxcueifel.gieseking@informatisiltk.unieleij-oldenburg.dnye4iu)

AdamMC: A Flow-LTL Model Checker for the Analysis of Distributed Asynchronous Models

Petri nets with transits allow us to follow the precise flow of tokens. For example, it is possible to exactly follow the flow of a packet in a software-defined network. Flow-LTL is a corresponding logic for Petri nets with transits and extends LTL. The logic has places and transitions as atomic propositions and allows to specify both global and local behavior. Run formulas for global behavior specify fairness and maximality assumptions, e.g., that the network always forwards packets eventually. Flow formulas for local behavior specify the flow of transits, e.g., that packets are routed loop free.

AdamMC provides three modules:

  • The general model checking problem of Petri nets with transits against Flow-LTL is solved.
  • Specific input languages to input updates to software-defined networks are provided and it is checked whether they fulfill properties like connectivity, packet coherence, drop freedom, and loop freedom expressed in Flow-LTL.
  • The model checking problem of Petri nets against LTL with places and transitions as atomic propositions is solved.

Authors: Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Haarbusch, Ernst-Rüdiger Olderog

Related Artifacts:

Related Publications:

  • B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)," CoRR, vol. abs/2005.07130, 2020.
    @article{DBLP:journals/corr/abs-2005-07130,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {{AdamMC}: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)},
      journal = {CoRR},
      volume = {abs/2005.07130},
      year = {2020},
      url = {http://arxiv.org/abs/2005.07130},
      archivePrefix = {arXiv},
      eprint = {2005.07130} }
  • B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Model Checking Data Flows in Concurrent Network Updates (Full Version)," CoRR, vol. abs/1907.11061, 2019.
    @article{DBLP:journals/corr/abs-1907-11061,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {Model Checking Data Flows in Concurrent Network Updates (Full Version)},
      journal = {CoRR},
      volume = {abs/1907.11061},
      year = {2019},
      url = {http://arxiv.org/abs/1907.11061},
      archivePrefix = {arXiv},
      eprint = {1907.11061},
      timestamp = {Thu, 01 Aug 2019 08:59:33 +0200},
      biburl = {https://dblp.org/rec/journals/corr/abs-1907-11061.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, und E. Olderog, "Model Checking Data Flows in Concurrent Network Updates," in Proc. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, 2019, pp. 515-533.
    @inproceedings{DBLP:conf/atva/FinkbeinerGHO19,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {Model Checking Data Flows in Concurrent Network Updates},
      booktitle = {Automated Technology for Verification and Analysis - 17th International Symposium, {ATVA} 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings},
      pages = {515--533},
      year = {2019},
      crossref = {DBLP:conf/atva/2019},
      url = {https://doi.org/10.1007/978-3-030-31784-3\_30},
      doi = {10.1007/978-3-030-31784-3\_30},
      timestamp = {Tue, 22 Oct 2019 15:35:01 +0200},
      biburl = {https://dblp.org/rec/conf/atva/FinkbeinerGHO19.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
Webmas6zflwter (m.gies4o9eking@ouh1tuol.de/p) (Stand: 21.08.2020)