@inproceedings{e23bbb35e48f4dc7bfe7d02bedff7887,
title = "Deadlock prevention in the {\AE}THEREAL protocol",
abstract = "The {\AE}THEREAL protocol enables both guaranteed and best effort communication in an on-chip packet switching network. We discuss a formal specification of {\AE}THEREAL and its underlying network in terms of the PVS specification language. Using PVS we prove absence of deadlock for an abstract version of our model.",
author = "B. Gebremichael and F.W. Vaandrager and M. Zhang and K.G.W. Goossens and E. Rijpkema and A. Radulescu",
year = "2005",
doi = "10.1007/11560548_28",
language = "English",
isbn = "978-3-540-29105-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "345--348",
editor = "D. Borrione and W. Paul",
booktitle = "Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbr{\"u}cken, Germany, October 3-6, 2005 : proceedings",
address = "Germany",
}