Models & Optimisation and Mathematical Analysis Journal
Volume 1, Numéro 2, Pages 1-7

Formal Verification Of Fault Tolerant Noc-base Architecture

Authors : Manamiary Bruno Andriamiarina . Daoud Hayat . Belarbi Mostefa . Méry Dominique . Tanougast Camel .


Approaches to design fault tolerant Network-on- Chip (NoC) for System-on-Chip(SoC)-based reconfigurable Field- Programmable Gate Array (FPGA) technology are challenges on the conceptualisation of the Multiprocessor System-on-Chip (MPSoC) design. For this purpose, the use of rigorous formal approaches, based on incremental design and proof theory, has become an essential step in a validation architecture. The Event- B formal method is a promising formal approach that can be used to develop, model and prove accurately the domain of SoCs and MPSoCs. This paper gives a formal verification of a NoC architecture, using the Event-B methodology. The formalisation process is based on an incremental and validated correct-by- construction development of the NoC architecture.


Network on chip, Switch, Adaptive-routing, ma- chine, context, Model, specification, refinement, Formal proof, Correct-by-construction.

Fault Tolerant Control Of Induction Motor Drives Subject To Rotor Resistance Adaptation

Boumalha Noureddine .  Kouchih D. .  Tadjine M. .  Boucherit M. S. . 
pages 11-22.

Formal Approach For Gpu Architecture Schedulability

Zouaneb Imane .  Belarbi Mostefa .  Chouarfia Abdellah . 
pages 10-16.