Models & Optimisation and Mathematical Analysis Journal
Volume 2, Numéro 1, Pages 17-22
2014-12-20
Based Refinement Verification Platform For Qnoc Architectures
Authors : Daoud Hayat . Belarbi Mostefa .
Abstract
Formal models play an important role of the requirements that lead to models of the design for a network on chip which is a reconfigurable FPGA-based (Field Programmable Gate Array) technology for faulty tolerance System-on-Chip, where the main challenge was how to achieve a conceptual design of multiprocessor System On Chip (MPSoC). The use of formal methods with the progressive basis and the proof theory has become an essential step to design and validate this architecture. Event-B is a formal modelling language, which supports refinement as a based-formal concept of development to models and proves the industry of MPSoCs. The purpose of this article is to provide a formal verification of Network-On-Chip (NoC) architecture using the Event-B method. This process is delivered by a correct and validated formalization based on the correct-by-construction development approach.
Keywords
Network on chip, Switch, Adaptive-routing, machine, context, Model, specification, refinement, Formal proof, Correct-by-construction, Active Zone.
Les articles similaires
Hariche Abdelhamid
.
Belarbi Mostefa
.
Daoud Hayat
.
pages 8-13.
خلفان بن زهران بن محد الحجي
.
ص 124-136.
Soltane Mohamed
.
pages 015-036.
Messaoudi Kamel
.
Toumi Salah
.
Bourennane El-bay
.
pages 24-31.
Bensaâd Redjel Nadia
.
pages 472-483.
