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 proceedingConference contributionAcademicpeer-review

18 Citations (Scopus)
1 Downloads (Pure)


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 languageEnglish
Title of host publicationCorrect hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings
EditorsD. Borrione, W. Paul
Place of PublicationBerlin
ISBN (Print)978-3-540-29105-3
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Deadlock prevention in the ÆTHEREAL protocol'. Together they form a unique fingerprint.

Cite this