Application of Timed-Arc Colored Petri Net for Network Update Synthesis
Authors
Christensen, Niels ; Glavind, Mark
Term
4. term
Education
Publication year
2019
Submitted on
2019-06-07
Pages
42
Abstract
Moderne netværk er komplekse distribuerede systemer. De ændrer ofte ruter, og disse opdateringer skal udføres konsistent på tværs af enheder. Selv om mange løsninger fokuserer på korrekthed, har der været mindre fokus på den tid, det tager at udrulle en ny konfiguration. For at automatisere, gøre opdateringer beviseligt korrekte og optimere dem, introducerer vi Timed-arc colored Petri nets (TACPN) med formel semantik. Petri-net er matematiske modeller af systemer med tilstande og hændelser; “farvede” net bærer dataværdier, og “timed-arc” net indeholder tidsbegrænsninger. TACPN kan modellere asynkron, samtidig adfærd, som er typisk for netværk. Vi foreslår en algoritme, der folder TACPN ud til et Timed-arc Petri-net, som derefter kan verificeres med eksisterende verifikationsværktøjer. Vi har også lavet en fuld implementering af TACPN i værktøjet TAPAAL, så man visuelt kan opbygge modeller. Vi giver en kodning af netværk i TACPN, der håndhæver sikkerhedspolitikken Waypoint Enforcement (WPE), som kræver, at trafik passerer udpegede kontrolpunkter (waypoints). I eksperimenter med virkelige netværkstopologier optimerer vi den værst tænkelige opdateringstid mellem to konfigurationer, samtidig med at WPE stadig overholdes.
Modern computer networks are complex distributed systems. They change routes frequently, and these updates must be applied consistently across devices. While many approaches focus on correctness, less attention has been paid to the time it takes to deploy a new configuration. To automate, prove correctness, and optimize these updates, we introduce Timed-arc colored Petri nets (TACPN) with formal semantics. Petri nets are mathematical models of systems with states and events; “colored” nets carry data values, and “timed-arc” nets include timing constraints. TACPN can model the asynchronous, concurrent behavior typical of networks. We propose an algorithm that unfolds a TACPN model into a Timed-arc Petri net, which can then be verified using existing verification engines. We also provide a complete TACPN implementation in the TAPAAL tool, enabling visual construction of models. We encode networks in TACPN that enforce the Waypoint Enforcement (WPE) security policy, which requires traffic to pass through designated waypoints. In experiments with real-world network topologies, we optimize the worst-case time to move from one configuration to another while ensuring WPE remains satisfied.
[This abstract was generated with the help of AI]
Keywords
Documents