Formal Verification of Fault Tolerant NoC-based Architecture - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

Formal Verification of Fault Tolerant NoC-based Architecture

(1, 2) , (3) , (3) , (1) , (4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
iwmcsv5.pdf (412 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00763092 , version 1 (11-12-2012)

Identifiers

  • HAL Id : hal-00763092 , version 1

Cite

Manamiary Bruno Andriamiarina, Hayat Daoud, Mostefa Belarbi, Dominique Méry, Camel Tanougast. Formal Verification of Fault Tolerant NoC-based Architecture. First International Workshop on Mathematics and Computer Science (IWMCS2012), Mostefa BELARBI - University of Tiaret - Algeria, Dec 2012, Tiaret, Algeria. ⟨hal-00763092⟩
313 View
234 Download

Share

Gmail Facebook Twitter LinkedIn More