This pure-join model of Chord and this full model of Chord, both in Alloy, will be discussed in the paper "Invariant-based verification of routing protocols: The case of Chord" (in preparation).
Almost all work on modeling networks has been performed in pursuit of performance and reliability. It is now time to look at networks from the perspective of those who must design, build, deploy, and maintain networked applications.
In the application layer of networks, many application servers are middleboxes in the paths of messages from source to destination. Applications require, as a basic coordination mechanism, a way to route messages through the proper servers. "Requirements for routing in the application layer" elaborates and justifies the requirements for such a coordination mechanism. It presents what is known about satisfying these requirements, and what questions still need to be answered (Pamela Zave; Proceedings of the Ninth International Conference on on Coordination Models and Languages, Springer-Verlag LNCS 4467, pages 19-36, 2007). Here is the talk given at the conference.
"Compositional binding in network domains" considers network services that bind identifiers in the course of delivering messages, and also persistent, point-to-point connections made in the context of such bindings. Five patterns represent the different ways that identifier binding can be accomplished. A formal Alloy model incorporating the patterns is used to compare the properties of the patterns, to define desirable network properties related to identifier binding, and to establish sufficient conditions for guaranteeing them. The results provide new insights into connections between mobile endpoints (Pamela Zave; Proceedings of the Fourteenth International Symposium on Formal Methods, Springer-Verlag LNCS 4085, pages 332-347, 2006).
"A formal model of addressing for interoperating networks" concerns designing network address spaces for interoperation among administrative domains. A formal model in Alloy is used to clarify the problems and explore solutions. Basic connectivity requirements are proposed, and two different sets of constraints are shown to satisfy them (Pamela Zave; Thirteenth International Symposium of Formal Methods Europe, Springer-Verlag LNCS 3582, pages 318-333, 2005). Here is the primary Alloy model and the requirements and checks that it satisfies. The secondary Alloy model has a slightly different set of constraints than the primary one, as explained in the paper.