[zeromq-dev] Modelling ZeroMQ formally

[John Lång]

Well, I didn't have so much time to familiarize with this library, but I 
read the description and got it compile. I think I need to learn more 
about OpenMAMA, but this OZ library seems like an interesting and 
important real life system to be modelled.

As I'm working full time on other things, I have maybe 10 to 15 hours 
per week to invest into this project. Maybe I can arrange something with 
my employer so that I could spend more time on this project. I hope I 
can get help from others, too. I'd appreciate if we could discuss the 
specifications of OZ over Zoom or something. I'd like to introduce my 
tools as well.

Feel free to send me email so that we can discuss the details.

John

John Lång kirjoitti 8.3.2022 klo 18.48:
> 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