Deadlock prevention in the ÆTHEREAL protocol

B. Gebremichael; F.W. Vaandrager; M. Zhang; K.G.W. Goossens; E. Rijpkema; A. Radulescu

doi:10.1007/11560548_28

Deadlock prevention in the ÆTHEREAL protocol

B. Gebremichael, F.W. Vaandrager, M. Zhang, K.G.W. Goossens, E. Rijpkema, A. Radulescu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

18 Citations (Scopus)

1 Downloads (Pure)

Abstract

The ÆTHEREAL protocol enables both guaranteed and best effort communication in an on-chip packet switching network. We discuss a formal specification of Æ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.

Original language	English
Title of host publication	Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings
Editors	D. Borrione, W. Paul
Place of Publication	Berlin
Publisher	Springer
Pages	345-348
ISBN (Print)	978-3-540-29105-3
DOIs	https://doi.org/10.1007/11560548_28
Publication status	Published - 2005

Publication series

Name	Lecture Notes in Computer Science
Volume	3725
ISSN (Print)	0302-9743

Access to Document

10.1007/11560548_28

Cite this

Gebremichael, B., Vaandrager, F. W., Zhang, M., Goossens, K. G. W., Rijpkema, E., & Radulescu, A. (2005). Deadlock prevention in the ÆTHEREAL protocol. In D. Borrione, & W. Paul (Eds.), Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings (pp. 345-348). (Lecture Notes in Computer Science; Vol. 3725). Springer. https://doi.org/10.1007/11560548_28

Gebremichael, B. ; Vaandrager, F.W. ; Zhang, M. et al. / Deadlock prevention in the ÆTHEREAL protocol. Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings. editor / D. Borrione ; W. Paul. Berlin : Springer, 2005. pp. 345-348 (Lecture Notes in Computer Science).

@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",

}

Gebremichael, B, Vaandrager, FW, Zhang, M, Goossens, KGW, Rijpkema, E & Radulescu, A 2005, Deadlock prevention in the ÆTHEREAL protocol. in D Borrione & W Paul (eds), Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings. Lecture Notes in Computer Science, vol. 3725, Springer, Berlin, pp. 345-348. https://doi.org/10.1007/11560548_28

Deadlock prevention in the ÆTHEREAL protocol. / Gebremichael, B.; Vaandrager, F.W.; Zhang, M. et al.
Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings. ed. / D. Borrione; W. Paul. Berlin: Springer, 2005. p. 345-348 (Lecture Notes in Computer Science; Vol. 3725).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Deadlock prevention in the ÆTHEREAL protocol

AU - Gebremichael, B.

AU - Vaandrager, F.W.

AU - Zhang, M.

AU - Goossens, K.G.W.

AU - Rijpkema, E.

AU - Radulescu, A.

PY - 2005

Y1 - 2005

N2 - The ÆTHEREAL protocol enables both guaranteed and best effort communication in an on-chip packet switching network. We discuss a formal specification of Æ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.

AB - The ÆTHEREAL protocol enables both guaranteed and best effort communication in an on-chip packet switching network. We discuss a formal specification of Æ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.

U2 - 10.1007/11560548_28

DO - 10.1007/11560548_28

M3 - Conference contribution

SN - 978-3-540-29105-3

T3 - Lecture Notes in Computer Science

SP - 345

EP - 348

BT - Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings

A2 - Borrione, D.

A2 - Paul, W.

PB - Springer

CY - Berlin

ER -

Gebremichael B, Vaandrager FW, Zhang M, Goossens KGW, Rijpkema E, Radulescu A. Deadlock prevention in the ÆTHEREAL protocol. In Borrione D, Paul W, editors, Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings. Berlin: Springer. 2005. p. 345-348. (Lecture Notes in Computer Science). doi: 10.1007/11560548_28

Deadlock prevention in the ÆTHEREAL protocol

Abstract

Publication series

Access to Document

Fingerprint

Cite this