Based Refinement Verification Platform For Qnoc Architectures

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.