Advertisement

Deadlock Prevention in the Æthereal Protocol

  • Biniam Gebremichael
  • Frits Vaandrager
  • Miaomiao Zhang
  • Kees Goossens
  • Edwin Rijpkema
  • Andrei Rădulescu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

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.

References

  1. 1.
    Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida (April 1995)Google Scholar
  2. 2.
    Gangwal, O.P., Rădulescu, A., Goossens, K., Pestana, S.G., Rijpkema, E.: Building predictable systems on chip: An analysis of guaranteed communication in the æthereal network on chip. In: van der Stok, P. (ed.) Philips Research Book Series, ch. 1. Kluwer, Dordrecht (2005)Google Scholar
  3. 3.
    Gebremichael, B., Vaandrager, F., Zhang, M.: Formal models of guaranteed and best-effort services for network on chip. Technical Report ICIS-R05016, Radboud University Nijmegen (2005)Google Scholar
  4. 4.
    Goossens, K., Dielissen, J., Rădulescu, A.: The Æthereal network on chip: Concepts, architectures, and implementations. IEEE Design and Test of Computers 22(5) (September/October 2005); Special issue on Networks on ChipGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Biniam Gebremichael
    • 1
  • Frits Vaandrager
    • 1
  • Miaomiao Zhang
    • 1
  • Kees Goossens
    • 2
  • Edwin Rijpkema
    • 2
  • Andrei Rădulescu
    • 2
  1. 1.ICISRadboud UniversityNijmegenThe Netherlands
  2. 2.Philips Research LaboratoriesEindhovenThe Netherlands

Personalised recommendations