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

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.

Based B Extraction Of Qnoc Architecture Properties

Hariche Abdelhamid .  Belarbi Mostefa .  Daoud Hayat . 
pages 8-13.


A Real-time Simulation Platform For The H.264 Codec Modules

Messaoudi Kamel .  Touiza Maamar .  Bourennane Elbay .  Toumi Salah .  Labbani Ouassila . 
pages 78-83.