Re: [tlaplus] TLA+ for parser correctness

[Alex Porter <aporter8013@xxxxxxxxx>]

If I understand correctly, you want to validate the contents of a message received over the network. TLA+ is more for doing system level design of distributed systems and algorithms. If you want something like a formally verified parser, see EverParse (https://project-everest.github.io/everparse/). 

On Sat, May 11, 2024, 10:39 PM moshe kravchik <moshe.kravchik@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/22e98309-b774-4865-8663-7c3f99f6f9aan%40googlegroups.com.

-- 
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/CADgQdyJDtUEkqURrU7dWw9iV96aM_y-UV%3DznQ%3DYODjvijmz2cw%40mail.gmail.com.