Los enfoques para el diseño de redes en chip (NoC) tolerantes a fallos para su uso en tecnología reconfigurable de sistema en chip (SoC) utilizando tecnología de matriz de puertas programables en campo (FPGA) son desafiantes, especialmente en el diseño de sistemas multiprocesador en chip (MPSoC). Para lograr esto, el uso de enfoques formales rigurosos, basados en el diseño incremental y la teoría de pruebas, se ha convertido en un paso esencial en el proceso de validación. El método Event-B es un enfoque formal prometedor que se puede utilizar para desarrollar, modelar y probar con precisión arquitecturas de SoC y MPSoC. Este documento propone un enfoque de verificación formal para la arquitectura de NoC que incluye las restricciones de confiabilidad relacionadas con la elección de la ruta de enrutamiento de paquetes de datos y la estrategia impuesta para la desviación cuando se detectan enrutadores defectuosos. El proceso de formalización es incremental y se valida mediante el desarrollo correcto por construcción de la arquitectura de NoC. Utilizando los conceptos de coloreado de grafos y formalismo B-event, los resultados obtenidos han demostrado su eficiencia para determinar los errores y una solución para garantizar un funcionamiento rápido y confiable de la red en comparación con métodos similares existentes.