TU Darmstadt / ULB / TUbiblio

Verification of Factorio Belt Balancers using Petri Nets

Leue, Andre (2021)
Verification of Factorio Belt Balancers using Petri Nets.
Technische Universität Darmstadt
doi: 10.26083/tuprints-00017621
Bachelorarbeit, Erstveröffentlichung, Verlagsversion

Kurzbeschreibung (Abstract)

Factorio is a game focusing on the design and management of increasingly complex logistics systems. Part of these logistic systems is the mass transportation of different items on transport belts, which provides a vast amount of different problems to solve. In this bachelor thesis we will focus on one of them, namely the load distribution between multiple belts with so called Belt Balancers. We will use Petri Nets to propose a modular system to model such a Belt Balancer and describe Belt Balancer properties commonly used in the Factorio community with linear temporal logic. Additionally we describe methods to manually and automatically verify those with PROMELA. Unfortunately we are not able to actually run those verifications for reasonably sized Belt Balancers due to internal limitations of the SPIN interpreter.

Typ des Eintrags: Bachelorarbeit
Erschienen: 2021
Autor(en): Leue, Andre
Art des Eintrags: Erstveröffentlichung
Titel: Verification of Factorio Belt Balancers using Petri Nets
Sprache: Englisch
Publikationsjahr: 2021
Ort: Darmstadt
Kollation: 52 Seiten
DOI: 10.26083/tuprints-00017621
URL / URN: https://tuprints.ulb.tu-darmstadt.de/17621
Kurzbeschreibung (Abstract):

Factorio is a game focusing on the design and management of increasingly complex logistics systems. Part of these logistic systems is the mass transportation of different items on transport belts, which provides a vast amount of different problems to solve. In this bachelor thesis we will focus on one of them, namely the load distribution between multiple belts with so called Belt Balancers. We will use Petri Nets to propose a modular system to model such a Belt Balancer and describe Belt Balancer properties commonly used in the Factorio community with linear temporal logic. Additionally we describe methods to manually and automatically verify those with PROMELA. Unfortunately we are not able to actually run those verifications for reasonably sized Belt Balancers due to internal limitations of the SPIN interpreter.

Status: Verlagsversion
URN: urn:nbn:de:tuda-tuprints-176215
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Theorie Paralleler Systeme
Hinterlegungsdatum: 31 Mai 2021 08:31
Letzte Änderung: 08 Jun 2021 11:45
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen