Modeling and Simulation of Computer Networks and Systems

Chapter 12

Towards correct and reusable Network-on-Chip architectures

Maryam Kamali¹, Luigia Petre², Kaisa Sere² and Masoud Daneshtalab³,    ¹University of Liverpool, Liverpool, UK,    ²Åbo Akademi University, Turku, Finland,    ³University of Turku, Turku, Finland

With network-on-chip (NoC) as the fundamental communication paradigm for many core architectures, we need to be able to evaluate its correctness. In this paper we propose a proving methodology for this, based on the Event-B formal method. Our approach is fundamentally reusable, thus addressing the increasing complexity of manycore architectures as well as alleviating the need for proving expertise. These matters are also facilitated by tool support, in the form of the Rodin tool platform ...