Four Formal Models of IEEE 1394 Link Layer
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909152938295296 |
|---|---|
| author | Garavel, Hubert Luttik, Bas |
| author_facet | Garavel, Hubert Luttik, Bas |
| contents | We revisit the IEEE 1394 high-performance serial bus ("FireWire"), which became a success story in formal methods after three PhD students, by using process algebra and model checking, detected a deadlock error in this IEEE standard. We present four formal models for the asynchronous mode of the Link Layer of IEEE 1394: the original model in muCRL, a simplified model in mCRL2, a revised model in LOTOS, and a novel model in LNT. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_18723 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Four Formal Models of IEEE 1394 Link Layer Garavel, Hubert Luttik, Bas Logic in Computer Science Hardware Architecture Programming Languages We revisit the IEEE 1394 high-performance serial bus ("FireWire"), which became a success story in formal methods after three PhD students, by using process algebra and model checking, detected a deadlock error in this IEEE standard. We present four formal models for the asynchronous mode of the Link Layer of IEEE 1394: the original model in muCRL, a simplified model in mCRL2, a revised model in LOTOS, and a novel model in LNT. |
| title | Four Formal Models of IEEE 1394 Link Layer |
| topic | Logic in Computer Science Hardware Architecture Programming Languages |
| url | https://arxiv.org/abs/2403.18723 |