[zeromq-dev] Modelling ZeroMQ formally

[John Lång]

Hi Bill,

Sounds like an interesting project! Sounds like you have already done 
interesting work on on it. I'll have a look at it on weekend.

Cheers,
John

Bill Torpey kirjoitti 7.3.2022 klo 21.34:
> 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
> _______________________________________________
> zeromq-dev mailing list
> zeromq-dev at lists.zeromq.org
> https://lists.zeromq.org/mailman/listinfo/zeromq-dev