[zeromq-dev] Modelling ZeroMQ formally

[Bill Torpey]

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 <john.lang at mykolab.com> 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
> zeromq-dev at lists.zeromq.org
> https://lists.zeromq.org/mailman/listinfo/zeromq-dev