On Correctness of Dynamic Protocol Update

Replacing or adding network protocols at runtime is problematic – it must involve synchronization of the protocol switch with ongoing local and network communication. We define a formal mathematical model of dynamic protocol update (DPU) and use it to define two DPU algorithms. The algorithms are based on fully-synchronized and lazy strategies. The two strategies implement updates with respectively, strong and weak safety properties. Our model allowed us to express the properties and the DPU algorithms clearly and abstractly, aiding algorithm design and correctness proofs.

Published in:
Lecture Notes in Computer Science, 3535
Presented at:
FMOODS '05: the 7th IFIP WG 6.1 Conference on Formal Methods for Open Object-Based Distributed Systems, Athens, Greece, June 15-17, 2005

 Record created 2005-08-09, last modified 2018-01-27

Rate this document:

Rate this document:
(Not yet reviewed)