Re: [tlaplus] TLA+ for parser correctness

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

https://github.com/tlaplus/Examples/blob/master/specifications/tcp/tcp.tla is my TLA+ spec of the abstract state machine defined in RFC 9293 (TCP).

M

> On May 12, 2024, at 2:24 PM, Aman Shaikh <amanshaikh75@xxxxxxxxx> wrote:
> 
> Hi Moshe
> 
> I have used TLA+ for network protocols - BGP to be specific, so yes, TLA+ can be used for verifying properties of a network protocol. But it depends on what exactly you're trying to achieve. Can you elaborate on what kind of properties you want to check?
> 
> aman
> 
> On Sunday, May 12, 2024 at 11:19:03 AM UTC-4 Markus Kuppe wrote:
> "Code for network protocol messages" is a bit vague, but if your main interest lies in securely parsing data transmitted over networks, you might find https://project-everest.github.io/everparse/ to be useful. 
> 
> > On May 11, 2024, at 10:39 PM, moshe kravchik <moshe.k...@xxxxxxxxx> wrote: 
> > 
> > This is a question to the TLA+ experts. I need to write code for network protocol messages' correctness and validity. I want to make sure I get everything correct. Is TLA+/PlusCal the right tool for the job? Are there any examples of applying it to similar tasks? 

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C2AA3ABB-1BBD-471D-A084-D4589700B54A%40lemmster.de.