{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T04:11:15Z","timestamp":1760242275356,"version":"build-2065373602"},"reference-count":46,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2017,2,22]],"date-time":"2017-02-22T00:00:00Z","timestamp":1487721600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems"],"abstract":"<jats:p>Approaches for the design of fault tolerant Network-on-Chip (NoC) for use in System-on-Chip (SoC) reconfigurable technology using Field-Programmable Gate Array (FPGA) technology are challenging, especially in Multiprocessor System-on-Chip (MPSoC) design. To achieve this, the use of rigorous formal approaches, based on incremental design and proof theory, has become an essential step in the validation process. The Event-B method is a promising formal approach that can be used to develop, model and prove accurately SoC and MPSoC architectures. This paper proposes a formal verification approach for NoC architecture including the dependability constraints relating to the choice of the path routing of data packets and the strategy imposed for diversion when faulty routers are detected. The formalization process is incremental and validated by correct-by-construction development of the NoC architecture. Using the concepts of graph colouring and B-event formalism, the results obtained have demonstrated its efficiency for determining the bugs, and a solution to ensure a fast and reliable operation of the network when compared to existing similar methods.<\/jats:p>","DOI":"10.3390\/systems5010017","type":"journal-article","created":{"date-parts":[[2017,2,22]],"date-time":"2017-02-22T11:36:58Z","timestamp":1487763418000},"page":"17","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Proof of the Dependable Bypassing Routing Algorithm Suitable for Adaptive Networks on Chip QnoC Architecture"],"prefix":"10.3390","volume":"5","author":[{"given":"Hayat","family":"Daoud","sequence":"first","affiliation":[{"name":"Laboratory of Informatics and Mathematics (LIM), University of Tiaret, Tiaret 14000, Algeria"},{"name":"Laboratoire de Conception, Optimisation et Mod\u00e9lisation des Syst\u00e8mes (LCOMS), ASEC Team, Universit\u00e9 de Lorraine, Metz 57070, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5399-1683","authenticated-orcid":false,"given":"Camel","family":"Tanougast","sequence":"additional","affiliation":[{"name":"Laboratoire de Conception, Optimisation et Mod\u00e9lisation des Syst\u00e8mes (LCOMS), ASEC Team, Universit\u00e9 de Lorraine, Metz 57070, France"}]},{"given":"Mostefa","family":"Belarbi","sequence":"additional","affiliation":[{"name":"Laboratory of Informatics and Mathematics (LIM), University of Tiaret, Tiaret 14000, Algeria"}]},{"given":"Mikael","family":"Heil","sequence":"additional","affiliation":[{"name":"Laboratoire de Conception, Optimisation et Mod\u00e9lisation des Syst\u00e8mes (LCOMS), ASEC Team, Universit\u00e9 de Lorraine, Metz 57070, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6887-1895","authenticated-orcid":false,"given":"Camille","family":"Diou","sequence":"additional","affiliation":[{"name":"Laboratoire de Conception, Optimisation et Mod\u00e9lisation des Syst\u00e8mes (LCOMS), ASEC Team, Universit\u00e9 de Lorraine, Metz 57070, France"}]}],"member":"1968","published-online":{"date-parts":[[2017,2,22]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1109\/TVLSI.2013.2240324","article-title":"Smart Reliable Network-on-Chip","volume":"22","author":"Killian","year":"2014","journal-title":"IEEE Trans. Very Large Scale Integr. Syst."},{"key":"ref_2","unstructured":"Leonidas, T., Sere, K., and Plosila, J. (2012). Modeling Communication in Multi\u2013Processor Systems\u2013on\u2013Chip Using Modular Connectors. Innovations in Embedded and Real-Time Systems Engineering for Communication. IGI Glob., 219\u2013240."},{"key":"ref_3","unstructured":"Guang, L., Plosila, J., Isoaho, J., and Tenhunen, H. (2010). Innovations in Embedded and Real-Time Systems Engineering for Communication, IGI Publishing."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1016\/j.sysarc.2013.06.001","article-title":"Formal approach to agent-based dynamic reconfiguration in Networks-On-Chip","volume":"59","author":"Ostroumov","year":"2013","journal-title":"J. Syst. Archit."},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Verbeek, F., and Schmaltz, J. (2012). Easy Formal Specification and Validation of Unbounded Networks-on-Chips Architectures. ACM Trans. Design Autom. Electron. Syst., 17.","DOI":"10.1145\/2071356.2071357"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"548324","DOI":"10.1155\/2009\/548324","article-title":"A Formal Approach to the Verification of Networks on Chip","volume":"2009","author":"Borrione","year":"2009","journal-title":"EURASIP J. Embed. Syst."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Aydi, Y., Tligue, R., Elleuch, M., Abid, M., and Dekeyser, J. (2009, January 13\u201316). A Multi Level Functional Verification of Multistage Interconnection Network for MPSOC. Proceedings of the 16th IEEE International Conference on Electronics, Circuits, and Systems, Yasmine Hammamet, Tunisia.","DOI":"10.1109\/ICECS.2009.5410896"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Van den Broek, T., and Schmaltz, J. (2009, January 15\u201318). Towards A Formally Verified Network-on-Chip. Proceedings of the 2009 Formal Methods in Computer-Aided Design, (FMCAD 2009), Austin, TX, USA.","DOI":"10.1109\/FMCAD.2009.5351124"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/s00165-007-0049-0","article-title":"A functional formalization of on chip communications","volume":"20","author":"Schmaltz","year":"2008","journal-title":"Form. Asp. Comput."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/s10617-005-1184-6","article-title":"Embedded System Design Using Formal Model Refinement: An Approach Based on the Combined Use of UML and the B Language","volume":"9","author":"Voros","year":"2004","journal-title":"Design Autom. Embed. Syst."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"61","DOI":"10.4018\/jertcs.2010040104","article-title":"Service-Oriented Development of Fault Tolerant Communicating Systems: Refinement Approach","volume":"1","author":"Laibinis","year":"2010","journal-title":"Int. J. Embed. Real-Time Commun. Syst."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Verbeek, F., and Schmaltz, J. (2010, January 8\u201312). Formal Specification of Networks-on-Chips:Deadlock and Evacuation. Proceedings of the Design, Automation Test Europe Conference & Exhibition, Dresden, Germany.","DOI":"10.1109\/DATE.2010.5457089"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Helmy, A., Pierre, L., and Jantsch, A. (2010, January 14\u201316). Theorem Proving Techniques for the Formal Verification of NoC Communications with Non-minimal Adaptive Routing. Proceedings of the IEEE 13th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, Vienna, Austria.","DOI":"10.1109\/DDECS.2010.5491781"},{"key":"ref_14","unstructured":"Yang, S.-A., and Baras, J.S. (2003). IFAC Workshop\u2014Modeling and Analysis of Logic Controlled Dynamic Systems, Elsevier."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"1154","DOI":"10.1109\/TC.2003.1228511","article-title":"A fault-tolerant and deadlock-free routing protocol in 2D meshes based on odd-even turn model","volume":"52","author":"Wu","year":"2003","journal-title":"IEEE Trans. Comput."},{"key":"ref_16","unstructured":"Park, D., Nicopoulos, C., Kim, J., Vijaykrishnan, N., and Das, C. (2006, January 25\u201328). Exploring fault-tolerant network-on-chip architectures. Proceedings of the International Conference on Dependable Systems and Networks (DSN 2006), Philadelphia, PA, USA."},{"key":"ref_17","unstructured":"Cansell, D., Tanougast, C., and Beviller, Y. (2004, January 28\u201330). Integration of the proof process in the design of microelectronic architecture for bitrate measurement instrumentation of transport stream program MPEG-2 DVB-T. Proceedings of the IEEE International Workshop on Rapid System Prototyping, Geneva, Switzerland."},{"key":"ref_18","unstructured":"Jarzabek, S., Schmidt, D.C., and Veldhuizen, T.L. (2006, January 22\u201326). Roadmap for enhanced languages and methods to aid verification. Proceedings of the 5th International Conference on Generative Programming and Component Engineering, Portland, OR, USA."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/s001650300002","article-title":"A mechanically proved and incremental development of IEEE 1394 tree identify protocol","volume":"14","author":"Abrial","year":"2003","journal-title":"Form. Asp. Comput."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"726","DOI":"10.1145\/265943.265960","article-title":"Verifying parameterzed networks","volume":"19","author":"Clarke","year":"1997","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Bharadwaj, R., Felty, A., and Stomp, F. (1995, January 11\u201313). Formalizing Inductive Proofs of Network Algorithms. Proceedings of the 1995 Asian Computing Science Conference, Springer-Verlag, London, UK.","DOI":"10.1007\/3-540-60688-2_54"},{"key":"ref_22","unstructured":"Curzon, P. (July, January 27). Experiences formally verifying a network component. Proceedings of the IEEE Conference on Computer Assurance, Gaithersburg, MD, USA."},{"key":"ref_23","unstructured":"Gordon, M., and Melham, T. (1993). Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press."},{"key":"ref_24","unstructured":"Chenard, J.S., Bourduas, S., Azuelos, N., Boul\u2019e, M., and Zilic, Z. (2007, January 16\u201320). Hardware Assertion Checkers in On-line Detection of Network-on-Chip Faults. Proceedings of the Desig Automation and Test in Europe, Worshop on Diagnostic Services in Networks-on-Chips, Nice, France."},{"key":"ref_25","unstructured":"IEEE Available online: http:\/\/ieeexplore.ieee.org\/document\/1524461\/."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1297666.1297670","article-title":"Automata-based assertion-checker synthesis of PSL properties","volume":"13","author":"Boule","year":"2008","journal-title":"ACM Trans. Des Autom. Electron. Syst."},{"key":"ref_27","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D.A. (1999). Model Cheking, The MIT Press."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Ogras, U., Hu, J., and Marculescu, R. (2005, January 18\u201321). Key Research Problems in NoC Design: A Holistic Perspective. Proceedings of the International Conference on Hardware\/Software Codesign and System Synthesis (CODES+ISSS\u20322005), New York, NY, USA.","DOI":"10.1145\/1084834.1084856"},{"key":"ref_29","unstructured":"Goossens, K. (2005, January 7\u20139). Formal Methods for Networks on Chips. Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD\u203205), Saint Malo, France."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1109\/MDT.2005.108","article-title":"Design, Synthesis, and Test of Networks on Chips","volume":"22","author":"Pande","year":"2005","journal-title":"IEEE Design Test Comput."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1132952.1132953","article-title":"A survey of research and practices of Network-on-chip","volume":"38","author":"Bjerregaard","year":"2006","journal-title":"ACM Comput. Surv."},{"key":"ref_32","unstructured":"Jantsch, A. (2006, January 28\u201330). Models of Computation for Networks on Chip. Proceedings of the Sixth International Conference on Application of Concurrency to System Design (ACSD\u203206), Turku, Finland."},{"key":"ref_33","unstructured":"Nielsen, S.F., and Sparso, J. (2001, January 12\u201313). Analysis of low-power SoC interconnection networks. Proceedings of the IEEE 19th Norchip Conference, Kista, Sweden."},{"key":"ref_34","unstructured":"Grecu, C., Ivanov, A., Saleh, R., Sogomonyan, E., and Pande, P. (2006, January 10\u201312). On-line Fault Detection and Location for NoC Interconnects. Proceedings of the International On-Line Testing Symposium (IOLTS\u203206), Lake of Como, Italy."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1109\/MDT.2005.104","article-title":"Analysis of Error Recovery Schemes for Networks on Chips","volume":"22","author":"Murali","year":"2005","journal-title":"IEEE Design Test Comput."},{"key":"ref_36","unstructured":"Schafer, M., Hollstein, T., Zimmer, H., and Glesner, M. (2005, January 6\u201310). Deadlock-free routing and Component placement for irregular mesh-based networks-on-chip. Proceedings of the 2005 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD\u203205), San Jose, CA, USA."},{"key":"ref_37","unstructured":"Gebremichael, B., Vaandrager, F.W., Zhang, M., Goossens, K., Rijpkema, E., and Radulescu, A. (2005, January 3\u20136). Deadlock Prevention in the \u00c6thereal protocol. Proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u203205), Saarbr\u00fccken, Germany."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.3166\/tsi.27.1065-1084","article-title":"La validation de mod\u00e8les Event-B avec le plug-in ProB pour RODIN","volume":"27","author":"Bendisposto","year":"2008","journal-title":"TSI"},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Sayar, I., and Bhiri, M.-T. (2014, January 3). From an abstract specification in event-B toward an UML\/OCL model. Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE 2014), Hyderabad, India.","DOI":"10.1145\/2593489.2593494"},{"key":"ref_40","unstructured":"Jastram, M. Available online: https:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/pdf\/rodin-doc.pdf."},{"key":"ref_41","unstructured":"Andriamiarina, M.B., Daoud, H., Belarbi, M., M\u00e9ry, D., and Tanougast, C. (2012, January 16\u201317). Formal verification of fault tolerant NoC-based architecture. Proceedings of the First International Workshop on Mathematics and Computer Science (IWMCS 2012), Tiaret, Algeria."},{"key":"ref_42","doi-asserted-by":"crossref","unstructured":"M\u00e9tivier, Y., Robson, J.M., Saheb-Djahromi, N., and Zemmari, A. (2009, January 15\u201318). Brief Annoucement: Analysis of an Optimal Bit Complexity Randomised Distributed Vertex Colouring Algorithm (Extended Abstract). Proceedings of 13th International Conference on Principles of Distributed Systems (OPODIS 2009), N\u00eemes, France.","DOI":"10.1007\/978-3-642-10877-8_28"},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.ipl.2008.01.002","article-title":"Complexity analysis of a decentralised graph colouring algorithm","volume":"107","author":"Duffy","year":"2008","journal-title":"Inf. Process. Lett."},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"Nickerson, B.R. (1990, January 20\u201322). Graph colouring register allocation for processors with multi-register operands. Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation (PLDI\u203290), White Plains, NY, USA.","DOI":"10.1145\/93542.93552"},{"key":"ref_45","doi-asserted-by":"crossref","unstructured":"Schneider, J., and Wattenhofer, R. (2010, January 25\u201328). Anew technique for distributed symmetry breaking. Proceedings of the 29th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC\u203210), Zurich, Switzerland.","DOI":"10.1145\/1835698.1835760"},{"key":"ref_46","first-page":"80","article-title":"Anew exam scheduling algorithm using graph coloring","volume":"5","author":"Malkawi","year":"2008","journal-title":"Int. Arab J. Inf. Technol."}],"container-title":["Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2079-8954\/5\/1\/17\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T18:28:52Z","timestamp":1760207332000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2079-8954\/5\/1\/17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,22]]},"references-count":46,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2017,3]]}},"alternative-id":["systems5010017"],"URL":"https:\/\/doi.org\/10.3390\/systems5010017","relation":{},"ISSN":["2079-8954"],"issn-type":[{"type":"electronic","value":"2079-8954"}],"subject":[],"published":{"date-parts":[[2017,2,22]]}}}