Skip to Main content Skip to Navigation
New interface
Journal articles

Formal Proof of the Dependable Bypassing Routing Algorithm Suitable for Adaptive Networks on Chip QnoC Architecture

Abstract : Approaches for the design of fault tolerant Network-on-Chip (NoC) for use in System-on-Chip (SoC) reconfigurable technology using Field-Programmable Gate Array (FPGA) technology are challenging, especially in Multiprocessor System-on-Chip (MPSoC) design. To achieve this, the use of rigorous formal approaches, based on incremental design and proof theory, has become an essential step in the validation process. The Event-B method is a promising formal approach that can be used to develop, model and prove accurately SoC and MPSoC architectures. This paper proposes a formal verification approach for NoC architecture including the dependability constraints relating to the choice of the path routing of data packets and the strategy imposed for diversion when faulty routers are detected. The formalization process is incremental and validated by correct-by-construction development of the NoC architecture. Using the concepts of graph colouring and B-event formalism, the results obtained have demonstrated its efficiency for determining the bugs, and a solution to ensure a fast and reliable operation of the network when compared to existing similar methods.
Complete list of metadata

https://hal.univ-lorraine.fr/hal-01883115
Contributor : Camille Diou Connect in order to contact the contributor
Submitted on : Thursday, September 27, 2018 - 4:45:47 PM
Last modification on : Monday, January 24, 2022 - 11:36:15 AM

Intranet access

Identifiers

Collections

Citation

Hayat Daoud, Camel Tanougast, Mostefa Belarbi, Mikael Heil, Camille Diou. Formal Proof of the Dependable Bypassing Routing Algorithm Suitable for Adaptive Networks on Chip QnoC Architecture. Systems, 2017, 5 (1), pp.17. ⟨10.3390/systems5010017⟩. ⟨hal-01883115⟩

Share

Metrics

Record views

15