Topological Self-Stabilization with Name-Passing Process Calculi
Christina Rickmann, Christoph Wagner, Uwe Nestmann, Stefan Schmid · VBN Forskningsportal (Aalborg Universitet) · 2016
Topological self-stabilization is the ability of a distributed system to have its nodes themselves establish a meaningful overlay network. Independent from the initial network topology, it converges to the desired topology via forwarding, inserting, and deleting links to neighboring nodes. We adapt a linearization algorithm, originally designed for a shared memory model, to asynchronous message-passing. We use an extended localized pi-calculus to model the algorithm and to formally prove its essential self-stabilization properties: closure and weak convergence for every arbitrary initial configuration, and strong convergence for restricted cases.