Hi John: Our ZeroMQ project (https://github.com/nyfix/OZ) uses PUB/SUB to provide discovery for network peers, as documented here: https://github.com/nyfix/OZ/blob/master/doc/Naming-Service.md
We added “heartbeating” to the protocol because we weren’t able to prove conclusively that the startup sequence was sufficient to guarantee that we could never miss a connection message, but intuitively it seems that the heartbeats are probably unnecessary. I’d certainly be interested in working with you to try to come up with a formal proof, either way. Best Regards, Bill Torpey > On Mar 7, 2022, at 1:10 PM, John Lång <[email protected]> wrote: > > Hello, > > I've been developing tooling for the Spin model checker (see > https://spinroot.com). I'd like to try out my tools in a real life case > study. Do you think it would be feasible to build an abstract model for some > aspect of the specification of ZeroMQ, e.g. the PUB-SUB mechanism? Is there > anyone who would be interested in becoming a co-author for a study? > > Best regards, > John Lång > > _______________________________________________ > zeromq-dev mailing list > [email protected] > https://lists.zeromq.org/mailman/listinfo/zeromq-dev _______________________________________________ zeromq-dev mailing list [email protected] https://lists.zeromq.org/mailman/listinfo/zeromq-dev
