Models & Optimisation and Mathematical Analysis Journal
Volume 1, Numéro 2, Pages 1-7
2012-12-17
Formal Verification Of Fault Tolerant Noc-base Architecture
Authors : Manamiary Bruno Andriamiarina . Daoud Hayat . Belarbi Mostefa . Méry Dominique . Tanougast Camel .
Abstract
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.
Keywords
Network on chip, Switch, Adaptive-routing, ma- chine, context, Model, specification, refinement, Formal proof, Correct-by-construction.
Les articles similaires
Boumalha Noureddine
.
Kouchih D.
.
Tadjine M.
.
Boucherit M. S.
.
pages 11-22.
Zouaneb Imane
.
Belarbi Mostefa
.
Chouarfia Abdellah
.
pages 10-16.
Hafs Toufik
.
Bennacer Layachi
.
Boughazi Mohamed
.
pages 30-41.
Boufenara Khjedidja
.
Labii Belkacem
.
pages 15-22.
