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. © IFIP International Federation for Information Processing 2005.
Cite
CITATION STYLE
Gebremichael, B., Vaandrager, F., Zhang, M., Goossens, K., Rijpkema, E., & Rǎdulescu, A. (2005). Deadlock prevention in the ÆTHEREAL protocol. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3725 LNCS, pp. 345–348). https://doi.org/10.1007/11560548_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.