Specifying an P2P protocol
I want to make a formal specification for a kademlia-based P2P protocol. The purpose of the specification is not ensuring some dynamic properties, but rather having something more tangible than a text description.
Is TLA+ a good choice? What other specification languages should I consider (maybe Alloy)? Also, if TLA+ is fine, I would like to have some advices on how to write the specification.
Note that the protocol includes some rather complicated subprotocols, like onion routing.
Posted Aug 6, 2019, 10:33 AM UTC
23
TLA^+ has been used very successfully to specify protocols. If you use old Reddit, as a civilized person should (if not, replace the
wwwin the address withold), you'll see some useful resources in the panel on the right (particularly TLA^+ Examples, and the Dr. TLA^+ Series). You will also find other examples by browsing the posts in this sub.