GitHub - jb567/tla-go-back-n: A TLA+ verification of the Go-Back-N ARQ protocol

jb567 / tla-go-back-n Public

Notifications You must be signed in to change notification settings
Fork 1
Star 2

A TLA+ verification of the Go-Back-N ARQ protocol

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 13 Commits
goBackN.toolbox		goBackN.toolbox
LICENSE		LICENSE
README		README
ass3.tla		ass3.tla
dataWire.tla		dataWire.tla
gbnReceiver.tla		gbnReceiver.tla
mpb.tla		mpb.tla
slidingSender.tla		slidingSender.tla
tcp.tla		tcp.tla

Repository files navigation

# TLA Verification of the TCP Go Back N protocol

This is a formal verification of the Go Back N ARQ Protocol using TLA+

## See Also

- [RFC 3366 - Advice to link designers on link Automatic Repeat reQuest (ARQ)](https://www.rfc-editor.org/rfc/rfc3366.txt)
- [RFC 813 - Window And Acknowledgement Strategy In TCP](https://tools.ietf.org/html/rfc813)