Abstract
Developing algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms. Petri nets with transits allow us to follow the data flow between components in a distributed system. They can be model checked against specifications in LTL on both the local data flow and the global behavior. Petri games allow the synthesis of local controllers for distributed systems from safety specifications. Modeling problems in these formalisms requires defining extended Petri nets which can be cumbersome when performed textually.
In this paper, we present a web interface (The web interface is deployed at http://adam.informatik.uni-oldenburg.de.) that allows an intuitive, visual definition of Petri nets with transits and Petri games. The corresponding model checking and synthesis problems are solved directly on a server. In the interface, implementations, counterexamples, and all intermediate steps can be analyzed and simulated. Stepwise simulations and interactive state space generation support the user in detecting modeling errors.
This work has been supported by the German Research Foundation (DFG) through Grant Petri Games (392735815) and through the Collaborative Research Center “Foundations of Perspicuous Software Systems” (TRR 248, 389792660), and by the European Research Council (ERC) through Grant OSARES (683300).
Chapter PDF
Similar content being viewed by others
References
Adam: https://github.com/adamtool/ (2020)
AdamWEB: https://github.com/adamtool/webinterface(2020)
Beutner, R., Finkbeiner, B., Hecking-Harbusch, J.: Translating asynchronous games for distributed synthesis. In: 30th International Conference on Concurrency Theory, CONCUR. LIPIcs, vol. 140, pp. 26:1–26:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019), https://doi.org/10.4230/LIPIcs.CONCUR.2019.26
Casado, M., Foster, N., Guha, A.: Abstractions for software-defined networks. Commun. ACM 57(10), 86–95 (2014), https://doi.org/10.1145/2661061.2661063
D3: https://d3js.org/ (2020)
David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: Integrated development environment for timed-arcPetri nets. In: Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS. Lecture Notes in Computer Science, vol. 7214, pp. 492–497. Springer (2012), https://doi.org/10.1007/978-3-642-28756-5_36
Finkbeiner, B.: Bounded synthesis for Petri games. In: Correct System Design- Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His60th Birthday. Lecture Notes in Computer Science, vol. 9360, pp. 223–237. Springer (2015), https://doi.org/10.1007/978-3-319-23506-6_15
Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, E.: Symbolicvs. bounded synthesis for Petri games. In: Sixth Workshop on Synthesis, SYNT@CAV. EPTCS, vol. 260, pp. 23–43 (2017), https://doi.org/10.4204/EPTCS.260.5
Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, E.: Modelchecking data flows in concurrent network updates. In: Automated Technology for Verification and Analysis - 17th International Symposium, ATVA. Lecture Notes in Computer Science, vol. 11781, pp. 515–533. Springer (2019), https://doi.org/10.1007/978-3-030-31784-3_30
Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, E.: AdamMC: A model checker for Petri nets with transits against Flow-LTL. In: Computer Aided Verification - 32nd International Conference, CAV. Lecture Notes in Computer Science, vol. 12225, pp. 64–76. Springer (2020), https://doi.org/10.1007/978-3-030-53291-8_5
Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, E.: Model checking branching properties on Petri nets with transits. In: Automated Technology for Verification and Analysis - 18th International Symposium, ATVA. Lecture Notes in Computer Science, vol. 12302, pp. 394–410. Springer(2020), https://doi.org/10.1007/978-3-030-59152-6_22
Finkbeiner, B., Gieseking, M., Olderog, E.: Adam: Causality-based synthesis of distributed systems. In: Computer Aided Verification - 27th International Conference, CAV. Lecture Notes in Computer Science, vol. 9206, pp. 433–439. Springer (2015), https://doi.org/10.1007/978-3-319-21690-4_25
Finkbeiner, B., Gölz, P.: Synthesis in distributed environments. In: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS. LIPIcs, vol. 93, pp. 28:1–28:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017), https://doi.org/10.4230/LIPIcs.FSTTCS.2017.28
Finkbeiner, B., Olderog, E.: Petri games: Synthesis of distributed systems with causal memory. Inf. Comput. 253, 181–203 (2017), https://doi.org/10.1016/j.ic.2016.07.006
Förster, K., Mahajan, R., Wattenhofer, R.: Consistent updates in software defined networks: On dependencies, loop freedom, and blackholes. In: IFIP Networking Conference. pp. 1–9. IEEE Computer Society (2016), https://doi.org/10.1109/IFIPNetworking.2016.7497232
Gieseking, M., Hecking-Harbusch, J., Yanich, A.: AdamWEB: A Web Interfacefor Petri Nets with Transits and Petri Games (2020). https://doi.org/10.6084/m9.figshare.13089800
Gieseking, M., Olderog, E., Würdemann, N.: Solving high-level Petrigames. Acta Informatica 57(3-5), 591–626 (2020), https://doi.org/10.1007/s00236-020-00368-5
Hecking-Harbusch, J., Metzger, N.O.: Efficient trace encodings of bounded synthesis for asynchronous distributed systems. In: Automated Technology for Verification and Analysis - 17th International Symposium, ATVA. Lecture Notes in Computer Science, vol. 11781, pp. 369–386. Springer (2019), https://doi.org/10.1007/978-3-030-31784-3_22
Hecking-Harbusch, J., Tentrup, L.: Solving QBF by abstraction. In: Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF. EPTCS, vol. 277, pp. 88–102 (2018), https://doi.org/10.4204/EPTCS.277.7
McKeown, N., Anderson, T.E., Balakrishnan, H., Parulkar, G.M., Peterson, L.L., Rexford, J., Shenker, S., Turner, J.S.: Openflow: enabling innovation in campus networks. Comput. Commun. Rev. 38(2), 69–74 (2008), https://doi.org/10.1145/1355734.1355746
Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part I. Theor. Comput. Sci. 13, 85–108 (1981), https://doi.org/10.1016/0304-3975(81)90112-2
Reisig, W.: Petri Nets: An Introduction, EATCS Monographs on Theoretical Computer Science, vol. 4. Springer (1985), https://doi.org/10.1007/978-3-642-69968-9
Sparkjava: http://sparkjava.com/ (2020)
University of Oldenburg: APT – Analyse von Petri-Netzen undTransitionssystemen. https://github.com/CvO-Theory/apt (2012)
Vue.js: https://vuejs.org/ (2020)
Vuetify: https://vuetifyjs.com/ (2020)
Wolf, K.: Petri net model checking with LoLA 2. In: Application and Theory of Petri Nets and Concurrency - 39th International Conference, PETRI NETS. Lecture Notes in Computer Science, vol. 10877, pp. 351–362. Springer (2018), https://doi.org/10.1007/978-3-319-91268-4_18
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
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.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Gieseking, M., Hecking-Harbusch, J., Yanich, A. (2021). A Web Interface for Petri Nets with Transits and Petri Games. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)