A CORRECTNESS PROOF OF A ONE-BIT SLIDING WINDOW PROTOCOL IN MU-CRL

Authors
BEZEM MA GROOTE JF
Citation
Ma. Bezem et Jf. Groote, A CORRECTNESS PROOF OF A ONE-BIT SLIDING WINDOW PROTOCOL IN MU-CRL, Computer journal, 37(4), 1994, pp. 289-307
Citations number
15
Categorie Soggetti
Computer Sciences","Computer Science Hardware & Architecture
Journal title
Computer journal → ACNP
ISSN journal
00104620
Volume
37
Issue
4
Year of publication
1994
Pages
289 - 307
Database
ISI
SICI code
0010-4620(1994)37:4<289:ACPOAO>2.0.ZU;2-7
Abstract
We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is give n in mu CRL, which is a process algebra extended with data. Due to the abundant parallelism in this protocol, the behaviour is quite complic ated. The complexity has been mastered by explicitly identifying invar iants and foci of cones in the protocol. Both concepts seem promising as tools for the verification of larger and more complex protocols.