TU Darmstadt / ULB / TUbiblio

Verification of Factorio Belt Balancers using Petri Nets

Leue, Andre (2021):
Verification of Factorio Belt Balancers using Petri Nets. (Publisher's Version)
Darmstadt, Technische Universität, DOI: 10.26083/tuprints-00017621,
[Bachelor Thesis]

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.

Item Type: Bachelor Thesis
Erschienen: 2021
Creators: Leue, Andre
Status: Publisher's Version
Title: Verification of Factorio Belt Balancers using Petri Nets
Language: English
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.

Place of Publication: Darmstadt
Collation: 52 Seiten
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Theory of Parallel Systems
Date Deposited: 31 May 2021 08:31
DOI: 10.26083/tuprints-00017621
Official URL: https://tuprints.ulb.tu-darmstadt.de/17621
URN: urn:nbn:de:tuda-tuprints-176215
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)
Show editorial Details Show editorial Details