A master thesis from Aalborg University
Application of Timed-Arc Colored Petri Net for Network Update Synthesis
Author(s)
Term
4. term
Education
Publication year
2019
Submitted on
2019-06-07
Pages
42 pages
Abstract
A modern network is a complex distributed system and provides many challenges. One challenge is route updates which happen often and need to be performed consistently. This is a complex issue where solutions are still being developed. However, there has not been much focus on the time used for deploying a new configuration. In order to automate provably correct and optimize network updates, we present Timed-arc colored Petri net (TACPN) with formal semantics, a model where it is possible to model asynchronous concurrent systems such as a network. We propose an algorithm to unfold TACPN into a Timed-arc Petri net, where the unfolded model can then be verified by known verification engines. To create the models visually we have created a full implementation of TACPN into the tool TAPAAL. We make an encoding of networks in TACPN, where the networks have to hold the security policy Waypoint Enforcement (WPE). We present results from experiments where we create real-world topologies into TACPN and optimize the worst case update time between two configurations, while WPE still holds.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.