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

15 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 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
PublisherSpringer
Pages345-348
ISBN (Print)978-3-540-29105-3
DOIs
Publication statusPublished - 2005

Publication series

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

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

Cite this