M. B. Andriamiarina, H. Daoud, M. Belarbi, D. Méry, and C. Tanougast, Formal Verification of Fault Tolerant NoC-based Architecture, First International Workshop on Mathematics and Computer Science (IWMCS2012), 2012.
URL : https://hal.archives-ouvertes.fr/hal-00763092

M. B. Andriamiarina and D. Méry, Stepwise development Of Distributed Vertex Coloring Algorithms (Full Report), 2011.
URL : https://hal.archives-ouvertes.fr/inria-00606254

M. B. Andriamiarina, D. Méry, and N. K. Singh, Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms, Lecture Notes in Computer Science, vol.7940, pp.268-284, 2013.
DOI : 10.1007/978-3-642-38613-8_19
URL : https://hal.archives-ouvertes.fr/hal-00819256

K. M. Chandy and L. Lamport, Distributed snapshots: determining global states of distributed systems, ACM Transactions on Computer Systems, vol.3, issue.1, pp.63-75, 1985.
DOI : 10.1145/214451.214456

S. D. Chawade, M. A. Gaikwad, and R. M. Patrikar, Article : Review of xy routing algorithm for network-on-chip architecture, International Journal of Computer Applications, vol.43, pp.20-23, 2012.

I. Chlamtac, M. Conti, and J. J. Liu, Mobile ad hoc networking: imperatives and challenges, Ad Hoc Networks, pp.13-64, 2003.
DOI : 10.1016/S1570-8705(03)00013-1
URL : http://ece.uprm.edu/~lukejie/icom6505_100_spring_2008/chlamtac03mobile.pdf

T. S. Hoang, H. Kuruma, D. Basin, and J. Abrial, Developing topology discovery in event-b. Sci Csp theorems for communicating b machines, Comput. Program. Formal Asp. Comput, vol.74, issue.174, pp.11-12879, 2005.

G. Scollo, Formal Description of the OSI Session Layer : Transport Service, Formal Description Technique Lotos : Results of the Esprit Sedos Project, 1989.

N. Sidorova and M. Steffen, Verifying Large SDL-Specifications Using Model Checking, SDL 2001 : Meeting UML, pp.403-420, 2001.
DOI : 10.1007/3-540-48213-X_25

C. Snook and M. Butler, UML-B, ACM Transactions on Software Engineering and Methodology, vol.15, issue.1, pp.92-122, 2006.
DOI : 10.1145/1125808.1125811

C. Snook and M. Butler, Uml-b and event-b : An integration of languages and tools, Proceedings of the IASTED International Conference on Software Engineering, SE '08, pp.336-341, 2008.

G. Tel, Introduction to distributed algorithms, 1994.
DOI : 10.1017/CBO9781139168724

I. Traor-'e, An outline of pvs semantics for uml statecharts, J. UCS, vol.6, issue.11, pp.1088-1108, 2000.

M. Wenzel, L. C. Paulson, and T. Nipkow, The Isabelle Framework, Theorem Proving in Higher Order Logics, pp.33-38, 2008.
DOI : 10.1007/978-3-540-74591-4_26

J. Abrial, The B-book : Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

J. Abrial, Modeling in Event-B : System and Software Engineering, 2010.
DOI : 10.1017/CBO9781139195881

J. Abrial, M. Butler, S. Hallerstede, and L. Voisin, An open extensible tool environment for eventb, Proceedings of the 8th International Conference on Formal Methods and Software Engineering, ICFEM'06, pp.588-605, 2006.

J. Abrial and T. S. Hoang, Using Design Patterns in Formal Methods: An Event-B Approach, Lecture Notes in Computer Science, vol.5160, pp.1-2, 2008.
DOI : 10.1007/978-3-540-85762-4_1

M. B. Andriamiarina, D. Méry, and N. K. Singh, Revisiting snapshot algorithms by refinement-based techniques, 13th International Conference on Parallel and Distributed Computing, Applications and Technologies, PDCAT 2012, pp.343-349, 2012.
DOI : 10.1109/pdcat.2012.119
URL : https://hal.archives-ouvertes.fr/hal-00734131

M. B. Andriamiarina, D. Méry, and N. K. Singh, Analysis of Self-??? and P2P Systems Using Refinement, Lecture Notes in Computer Science, vol.8477, pp.117-123, 2014.
DOI : 10.1007/978-3-662-43652-3_9
URL : https://hal.archives-ouvertes.fr/hal-01018125

K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz, Verifying Safety Properties with the TLA???+??? Proof System, Automated Reasoning, pp.142-148, 2010.
DOI : 10.1007/978-3-642-14203-1_12
URL : https://hal.archives-ouvertes.fr/inria-00534821

D. Déharbe, P. Fontaine, Y. Guyot, L. Voisin, B. Vdm et al., SMT Solvers for Rodin, Lecture Notes in Computer Science, vol.7316, pp.194-207, 2012.
DOI : 10.1007/978-3-642-30885-7_14

T. S. Hoang, A. Furst, and J. Abrial, Event-b patterns and their tool support, Software Engineering and Formal Methods, International Conference on, pp.210-219, 2009.
DOI : 10.1109/sefm.2009.17
URL : https://www.research-collection.ethz.ch/bitstream/20.500.11850/69827/1/eth-5538-01.pdf

L. Lamport, The TLA Toolbox

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

G. T. Leavens, J. Abrial, D. Batory, M. Butler, A. Coglio et al., Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering , GPCE '06, pp.221-235, 2006.
DOI : 10.1145/1173706.1173740

M. Leuschel and M. J. Butler, ProB: an automated analysis toolset for the B method, International Journal on Software Tools for Technology Transfer, vol.49, issue.3, pp.185-203, 2008.
DOI : 10.1007/978-1-4615-1391-9_11

H. Hoang, ContrairementàContrairementà ce que nous proposons, Hoang et Hudon ne distinguent pas la séparation entre les spécifications temporelles, expriméesexpriméesà l'aide de propriétés de vivacité et de conditions d'´ equité, et les spécifications Event-B. Le raisonnement sur les propriétés temporelles est inclus dans les modèles Event-B. Demanì ere assez similairè a ce que nous proposons, leur méthodologie nécessite la redéfinitionredéfinitionà chaqué etape raffinement des hypothèses d'´ equité, pour préserver les propriétés de vivacité Une des différences principales se situe aussi sur le fait que nous avons choisi de baser notre méthodologie sur la logique TLA, plus générale qu'UNITY, qui représente seulement un fragment de la logique temporelle [22]. Nous proposons ici une approche explicite basée sur la logique TLA, pour la prise en compte des propriétés de vivacité et d'´ equité. L'approche habituelle en Event-B est de supposer qu'un ordonnanceur choisitéquitablementchoisitéquitablement parmi lesévénementslesévénements activables, ` a tout moment. Ce genre d'ordonnanceur peutêtrepeutêtre mis en place dans les modèlesmodèlesà l'aide de compteurs, d'indicateurs permettant de définir des priorités pour lesévénementslesévénements [6, 11]. Nous nous intéressons aussì a la possibilité de la réutilisation des services (ou de certaines parties de ces services) identifiés lors d'anciens développements : ces services ou certaines phases/´ etapes de ces services peuventêtrepeuventêtre réutilisés, notamment pour construire de nouveaux systèmes [8], par instanciation puis spécialisation (ajout de détails par raffinement) par rapport auprobì emé etudié. Il s'agit ici d'une notion proche de celle des patrons de conception proposée par Abrial et al [5, 18], car notre objectif est non seulement de réutiliser lesélémentsleséléments de modèles Event-B modélisant ces services, ) et en utilisant les outils fournis par la plateforme Rodin pour l'instanciation de ces patrons

]. M. Bibliographie1, L. Abadi, and . Lamport, The existence of refinement mappings, Theor. Comput. Sci, vol.82, issue.2, pp.253-284, 1991.

J. Abrial, Extending b without changing it (for developing distributed systems), st Conference on the B method, pp.169-190, 1996.

J. Abrial, Modeling in Event-B : System and Software Engineering, 2010.
DOI : 10.1017/CBO9781139195881

J. Abrial, D. Cansell, and D. Méry, A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol, Formal Aspects of Computing, vol.14, issue.3, pp.215-227, 2003.
DOI : 10.1007/s001650300002
URL : https://hal.archives-ouvertes.fr/inria-00099531

J. Abrial and T. S. Hoang, Using Design Patterns in Formal Methods: An Event-B Approach, Lecture Notes in Computer Science, vol.5160, pp.1-2, 2008.
DOI : 10.1007/978-3-540-85762-4_1

J. Abrial and L. Mussat, Introducing dynamic constraints in B, B98, pp.83-128, 1998.
DOI : 10.1007/BFb0053357

M. B. Andriamiarina, Stepwise development of distributed algorithms, FM 2011 : Doctoral Symposium, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00606204

M. B. Andriamiarina, D. Méry, and N. K. Singh, Revisiting snapshot algorithms by refinement-based techniques, 13th International Conference on Parallel and Distributed Computing, Applications and Technologies, PDCAT 2012, pp.343-349, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00734131

M. B. Andriamiarina, D. Méry, and N. K. Singh, Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms, Johnsen and Petre, pp.268-284
DOI : 10.1007/978-3-642-38613-8_19
URL : https://hal.archives-ouvertes.fr/hal-00819256

D. Bert, Preuve de propriétés d'´ equité en B : ´ etude du protocole du bus SCSI-3, Approches Formelles dans l'Assistance au Développement de Logiciels, pp.221-241, 2001.

D. Cansell and D. Méry, The event-B Modelling Method: Concepts and Case Studies, Logics of Specification Languages, Monographs in Theoretical Computer Science, pp.33-140, 2008.
DOI : 10.1007/978-3-540-74107-7_3
URL : https://hal.archives-ouvertes.fr/inria-00579550

D. Cansell, D. Méry, and S. Merz, Diagram refinements for the design of reactive systems, J. UCS, vol.7, issue.2, pp.159-174, 2001.

K. M. Chandy, Parallel Program Design, 1988.
DOI : 10.1007/978-1-4613-9668-0_6

M. Dominique, Modèles et Algorithmes -Modélisation et Vérification de Systèmes, 2014.

T. Hoang and J. Abrial, Reasoning about Liveness Properties in Event-B, Formal Methods and Software Engineering, pp.456-471, 2011.
DOI : 10.1016/0020-0190(81)90106-X

S. Hudon and T. S. Hoang, Systems Design Guided by Progress Concerns, pp.16-30
DOI : 10.1007/978-3-642-38613-8_2

L. Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, vol.21, issue.7, pp.558-565, 1978.
DOI : 10.1145/359545.359563

L. Lamport, Verification and specification of concurrent programs, A Decade of Concurrency, pp.347-374, 1993.
DOI : 10.1007/3-540-58043-3_23

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

D. Méry, Refinement-based guidelines for algorithmic systems, International Journal of Software and Informatics, vol.3, issue.2-3, pp.197-239, 2009.

D. Méry and M. Poppleton, Formal Modelling and Verification of Population Protocols, pp.208-222
DOI : 10.1007/978-3-642-38613-8_15

D. Méry and N. K. Singh, Analysis of DSR Protocol in Event-B, Proceedings of the 13th international conference on Stabilization, safety, and security of distributed systems, pp.401-415, 2011.
DOI : 10.1007/11943952_7

S. S. Owicki and L. Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems, vol.4, issue.3, pp.455-495, 1982.
DOI : 10.1145/357172.357178

R. Silva, Refactoring Framework. http://rodin-b-sharp.sourceforge, 2009.

A. S. Tanenbaum, Computer networks (4, 2002.

G. Tel, Introduction to distributed algorithms, 1994.
DOI : 10.1017/CBO9781139168724

P. Présentation-du, R. Anycast, and .. Des-rps, 78 5.3.2.2 Premier raffinement : Routeur Désigné (DR), 78 5.3.2.1 Modèle abstrait du protocole Anycast, p.143

J. Abrial and T. S. Hoang, Using Design Patterns in Formal Methods: An Event-B Approach, Lecture Notes in Computer Science, vol.5160, pp.1-2, 2008.
DOI : 10.1007/978-3-540-85762-4_1

S. Bhattacharyga, An overview of Source-Specific Multicast (SSM)

B. Fenner, M. Handley, H. Holbrook, and I. Kouvelas, Protocol Indepent Multicast -Sparse Mode (PIM-SM) :Protocol Specification

M. Handley, I. Kouvelas, T. Speakman, and L. Vicisano, Protocol Indepent Multicast -Dense Mode (PIM-DM) :Protocol Specification

D. Hardy, G. Malléus, and J. Méreur, Réseaux : Internet, téléphonie, multimédia. Convergences et complémentarités, 2002.

T. S. Hoang, H. Kuruma, D. Basin, and J. Abrial, Developing topology discovery in event-b, Science of Computer Programming, vol.74, pp.11-12879, 2009.

J. Kang, J. Sucec, V. Kaul, S. Samtani, and M. A. Fecko, Robust PIM-SM Multicasting Using Anycast RP in Wireless Ad Hoc Networks, 2009 IEEE International Conference on Communications, pp.5139-5144, 2009.
DOI : 10.1109/ICC.2009.5199425

D. Méry, Refinement-based guidelines for algorithmic systems, International Journal of Software and Informatics, vol.3, issue.2-3, pp.197-239, 2009.

D. Meyer and D. Fenner, Multicast source discovery protocol MSDP

J. Rehm, Gestion du temps par le raffinement, Thèse, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00441312

.. Patrons-de-conception-pour-le-routage, 159 6.2.1.1 Plan de développement, p.177

J. Abrial, Modeling in Event-B : System and Software Engineering, chapter, 2009.
DOI : 10.1017/CBO9781139195881

J. Abrial and T. S. Hoang, Using Design Patterns in Formal Methods: An Event-B Approach, Lecture Notes in Computer Science, vol.5160, pp.1-2, 2008.
DOI : 10.1007/978-3-540-85762-4_1

C. Alexander, S. Ishikawa, and M. Silverstein, A pattern language : towns, buildings, construction, 1977.

D. Cansell, D. Méry, and J. Rehm, Time Constraint Patterns for Event B Development
DOI : 10.1007/11955757_13
URL : https://hal.archives-ouvertes.fr/hal-00149163

S. D. Chawade, M. A. Gaikwad, and R. M. Patrikar, Article : Review of xy routing algorithm for network-on-chip architecture, International Journal of Computer Applications, vol.43, pp.20-23, 2012.

W. J. Dally and B. Towles, Route packets, not wires: on-chip interconnection networks, Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232), pp.684-689, 2001.
DOI : 10.1109/DAC.2001.935594

E. W. Dijkstra, Self-stabilizing systems in spite of distributed control, Communications of the ACM, vol.17, issue.11, pp.643-644, 1974.
DOI : 10.1145/361179.361202

P. C. French and R. W. Taylor, A self-reconfiguring processor, IEEE Workshop on FPGAs for Custom Computing Machines, pp.50-59, 1993.

E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns : Elements of Reusable Objectoriented Software, 1995.

M. Kamali, L. Petre, K. Sere, and M. Daneshtalab, Formal Modeling of Multicast Communication in 3D NoCs, 2011 14th Euromicro Conference on Digital System Design, pp.634-642, 2011.
DOI : 10.1109/DSD.2011.86

C. C. Marquezan and L. Z. Granville, Self-* and P2P for Network Management -Design Principles and Case Studies, Briefs in Computer Science, 2012.

D. Méry, Refinement-based guidelines for algorithmic systems, International Journal of Software and Informatics, vol.3, issue.2-3, pp.197-239, 2009.

A. Nayebi, S. Meraji, A. Shamaei, and H. Sarbazi-azad, XMulator: A Listener-Based Integrated Simulation Platform for Interconnection Networks, First Asia International Conference on Modelling & Simulation (AMS'07), pp.128-132, 2007.
DOI : 10.1109/AMS.2007.112

M. Palesi, R. Holsmark, S. Kumar, and V. Catania, Application Specific Routing Algorithms for Networks on Chip, IEEE Transactions on Parallel and Distributed Systems, vol.20, issue.3, pp.316-330, 2009.
DOI : 10.1109/TPDS.2008.106

S. Rajesh, V. K. , S. Srivatsan, R. Harini, and A. Shanthi, Fault tolerance in multicore processors with reconfigurable hardware unit, 15th international conference on high performance computing, pp.166-171, 2008.

J. Rehm, Gestion du temps par le raffinement, Thèse, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00441312

R. P. Sidhu, A. Mei, and V. K. Prasanna, String matching on multicontext fpgas using selfreconfiguration, Proceedings of the 1999 ACM/SIGDA Seventh International Symposium on Field Programmable Gate Arrays, FPGA '99, pp.217-226, 1999.

R. P. Sidhu, S. Wadhwa, A. Mei, and V. K. Prasanna, A Self-Reconfigurable Gate Array Architecture, Lecture Notes in Computer Science International Journal of Computer Science and Network Security, vol.1896, issue.7, pp.106-120, 2000.
DOI : 10.1007/3-540-44614-1_12

C. Tavernier, Circuits logiques programmables, Microcontrôleurs et environnement. Dunod, 1996.

W. Zhang, L. Hou, J. Wang, S. Geng, and W. Wu, Comparison Research between XY and Odd-Even Routing Algorithm of a 2-Dimension 3X3 Mesh Topology Network-on-Chip, 2009 WRI Global Congress on Intelligent Systems, pp.329-333, 2009.
DOI : 10.1109/GCIS.2009.110

M. B. Andriamiarina, D. Méry, and N. K. Singh, Revisiting snapshot algorithms by refinement-based techniques, Computer Science and Information Systems, vol.11, issue.1, pp.251-270, 2014.
DOI : 10.2298/CSIS130122007A
URL : https://hal.archives-ouvertes.fr/hal-00734131

K. M. Chandy and L. Lamport, Distributed snapshots: determining global states of distributed systems, ACM Transactions on Computer Systems, vol.3, issue.1, pp.63-75, 1985.
DOI : 10.1145/214451.214456

A. D. Kshemkalyani, M. Raynal, and M. Singhal, An introduction to snapshot algorithms in distributed computing, Distributed Systems Engineering, p.224, 1995.
DOI : 10.1088/0967-1846/2/4/005

T. Lai and T. H. Yang, On distributed snapshots, Information Processing Letters, vol.25, issue.3, pp.153-158, 1987.
DOI : 10.1016/0020-0190(87)90125-6

C. Morgan, Global and logical time in distributed algorithms, Information Processing Letters, vol.20, issue.4, pp.189-194, 1985.
DOI : 10.1016/0020-0190(85)90048-1

G. Tel, Introduction to distributed algorithms, 1994.
DOI : 10.1017/CBO9781139168724

Z. Yang and T. A. Marsland, Global snapshots for distributed debugging : An overview, 1992.

.. Détails-et-début-de-localisation-des-phases, 308 8.3.4.3 Redéploiement d'un service : abstraction L'instance « token owner » et lesétatslesétats d'un service, p.341

E. W. Dijkstra, Self-stabilizing systems in spite of distributed control, Communications of the ACM, vol.17, issue.11, pp.643-644, 1974.
DOI : 10.1145/361179.361202

S. Dolev, Self Stabilization, Journal of Aerospace Computing, Information, and Communication, vol.1, issue.6, 2000.
DOI : 10.1038/scientificamerican0603-54
URL : https://hal.archives-ouvertes.fr/inria-00627780

C. C. Marquezan and L. Z. Granville, Self-* and P2P for Network Management -Design Principles and Case Studies, Briefs in Computer Science, 2012.

. Dans-le-cadre-de-event-b, Abrial et al [3, 11], un patron de conception comme un développement Event-B formalisant desprobì emes typiques récurrent : un patron de conception est donc composé d'un modèle de spécification abstrait et de modèles raffinant cette spécification abstraite. La problématique réside ici dans la réutilisation de développements formels existants (des patrons de conception) dans un développement plus large dont certainsélémentscertainséléments correspondent aux probì emes auxquel s'adresse les patrons. Cette problématique nous poussè a compléter notre définition d'un patron de conception, rejoignant ainsi le point de vue présenté par d'Abrial et al [3, 11] : un patron de conception Event-B n'est pas seulement constitué de modèles (contextes, machines, constantes, variables, invariants, ´ evénements, mais aussi de la correction de ces derniers et des preuves de cette correction

?. Pattern2-introduit-le-réseau-reliant-les-processus-entre-eux, Un paquet envoyé par une source peut traverser plusieurs routeurs adjacents les uns aux autres, avant d'? etre reçu par son (ses) destinataire(s ) Nous modélisons aussi la mobilité du réseau : les liens existant entre deux processus voisins peuvent dispara??tredispara??tre

. En-résumé, finalement assez abstrait, répondant auprobì eme du routage, plus précisément, ` a l'acheminement d'un paquet dans un réseau entre sa source et son (ses) destinataire(s) Nous ne modélisons pas les tables de routages, ou les techniques de misesàmisesà jour de ces dernì eres, qui, selon notre expérience

. La-principale-difficulté-consiste-icì-a-renommer, soit ceux du développement formel duprobì eme, ce qui est réalisablè a l'aide du greffon « Refactoring Framework ». Une possible solution est de donner au greffon « Pattern » la possibilité d'effectuer des « matchings » (correspondances) au niveau des contextes des patron etprobì eme, comme réalisé au niveau des machines et de permettre, le caséchéantcaséchéant, de renommer desélémentsdeséléments de ces contextes Nous avons aussi remarqué que certains invariants et propriétés de sûreté, notamment ceux définis dans les raffinements du patron de conception pour le routage (lors de l'introduction du réseau), n'´ etaient pas recopiés dans les raffinements des modèles du NoC, générésgénérés`générésà partir du patron. Nous avons donc dû les incorporer manuellement aux raffinements générés et décharger ainsi des obligations de preuves, opérations qui selon nous, auraient pû etré evitées. Nous proposons comme solution d'intégrer toutes les propriétés de sûreté/d'invariance définies par le patron et de les corriger et/ou supprimer, si cela s'avérait nécessaire. En résumé, nous avons pu expérimenter la réutilisation de modèles formels Event-B et des preuves associées. Un supportàsupportà l'aide d'outils de cette technique de développement formel existe, notammentànotammentà travers le greffon « Pattern ». Desprobì emes (décrits précédemment), probablement liéesliéesà la jeunesse de l'outil (en version 1.0.3), existent, mais peuventêtrepeuventêtre contournés et/ou résolus en complétant l'utilisation de « Pattern, Nous tenons aussì a remarquer que lors de nos expérimentations, le greffon « Pattern » n'´ etait pas compatible avec ladernì ere version de la plateforme Rodin (version 3.0). Nous avons donc mené nos expérimentations sur la version 2

. Notre-objectif-est-ici-d, identifier les aspects d'un développement formel d'algorithme et de système répartis pouvant produire et/ou faire augmenter le nombre d'obligations de preuvesàpreuvesà décharger manuellement par l'utilisateur. Nous donnons pour chacun des cas d'´ etudes, deux analyses des obligations de preuves engendrées par la plateforme Rodin, et déchargées automatiquement ou manuellement : ? Lapremì ere est l'analyse des obligations de preuves

B. Atelier, «. Du-greffon, and . Smt-plugin, Conclusion Nous avons expérimenté, dans le cadre de la réduction du nombre d'obligations de preuvesàpreuvesà décharger manuellement, l'utilisation de solveurs SMT pour compléter les prouveurs offerts par la plateforme Rodin : lesétudeslesétudes de cas vues durant cette thèse nous permettent d'affirmer que cette utilisation conjointe des solveurs SMT et des prouveurs procure des gains de preuves automatiques, allant d'environ 27%à 27%à 100%. Nous pouvons par conséquent dire que dans notre cas, l'utilisation des solveurs SMT aide au développement formel de systèmes et algorithmes répartis en Event-B et ces solveurs arrivent généralementàmentà automatiser les déchargements des obligations de preuves liéesliéesà la localisation, aux raffinements de données (e.g. transformation d'un ensemble en fonction), ainsi qu, ? La seconde est l'analyse des obligations de preuves, quand des solveurs SMT (ici veriT

. De-la-plateforme-rodin-et-de-ses-greffons, ». Pattern, R. Framework, ». , and «. Smt-plugin, Notre objectif principal via l'utilisation de ces outils est la réduction des efforts de modélisation et du nombre des obligations de preuves, ` a décharger manuellement, lors de la modélisation d'algorithmes et systèmes répartis Notrepremì ere expérimentation a ´ eté axée sur la réutilisation d'anciens développements formels, principalement les modèles (contextes, machines et raffinements), leurs corrections et les preuves liées liéesà cesdernì eres. Nous avons basé notre approche sur les patrons de conception en Event-B : il s'agit de développements formels (modèles, raffinement et preuves), résolvant, totalement ou en partie, des probì emes récurrents/communs, et qui sont ensuite instanciés (réutilisations des modèles, raffinements et preuves, après adaptations) dans des développements plus larges, Conclusion Nous nous sommes intéressésintéressésà des expérimentations sur des modèles Event-B, p.le NoC

]. Bibliographie and . Abrial, The B-book : Assigning Programs to Meanings, 1996.

J. Abrial, Modeling in Event-B : System and Software Engineering, chapter, 2009.
DOI : 10.1017/CBO9781139195881

J. Abrial and T. S. Hoang, Using Design Patterns in Formal Methods: An Event-B Approach, p.399
DOI : 10.1007/978-3-540-85762-4_1

C. Alexander, S. Ishikawa, and M. Silverstein, A pattern language : towns, buildings, construction, 1977.

C. Barrett and C. Tinelli, CVC3, Proceedings of the 19 th International Conference on Computer Aided Verification (CAV '07), pp.298-302, 2007.
DOI : 10.1007/978-3-540-73368-3_34

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, Proc. Conference on Automated Deduction (CADE), Lecture Notes in Computer Science, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

D. Déharbe, P. Fontaine, Y. Guyot, L. Voisin, B. Vdm et al., SMT Solvers for Rodin, Lecture Notes in Computer Science, vol.7316, pp.194-207, 2012.
DOI : 10.1007/978-3-642-30885-7_14

E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns : Elements of Reusable Objectoriented Software, 1995.

C. C. Marquezan and L. Z. Granville, Self-* and P2P for Network Management -Design Principles and Case Studies, Briefs in Computer Science, 2012.

D. Méry, Refinement-based guidelines for algorithmic systems, International Journal of Software and Informatics, vol.3, issue.2-3, pp.197-239, 2009.

J. Rehm, Gestion du temps par le raffinement, Thèse, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00441312

R. Silva and . Framework, [19] C. Systems. Anycast RP, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01708281

?. Un-algorithme-de-routage, Anycast RP [6], proposé et mis au point par CISCO Systems. Il s'agit d'un algorithme complexe, dont le développement complet a nécessité une douzaine d'´ etapes de raffinement, de l'abstractionàabstractionà la version locale de l'algorithme

J. Abrial, Modeling in Event-B : System and Software Engineering, 2010.
DOI : 10.1017/CBO9781139195881

M. B. Andriamiarina, Stepwise development of distributed algorithms, FM 2011 : Doctoral Symposium, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00606204

M. B. Andriamiarina and D. Méry, Stepwise development of distributed vertex colouring algorithms (abstract), 2011 Grande Region Security and Reliability Day, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00606201

M. B. Andriamiarina, D. Méry, and N. K. Singh, Revisiting snapshot algorithms by refinement-based techniques, 13th International Conference on Parallel and Distributed Computing, Applications and Technologies, PDCAT 2012, pp.343-349, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00734131

M. B. Andriamiarina, D. Méry, and N. K. Singh, Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms, Johnsen and Petre [13], pp.268-284
DOI : 10.1007/978-3-642-38613-8_19
URL : https://hal.archives-ouvertes.fr/hal-00819256

N. Bjørner, A. Browne, M. Colón, B. Finkbeiner, Z. Manna et al., Verifying temporal properties of reactive systems : A step tutorial, Formal Methods in System Design, vol.16, issue.3, pp.227-270, 2000.
DOI : 10.1023/A:1008700623084

D. Cansell, D. Méry, and S. Merz, Diagram refinements for the design of reactive systems, J. UCS, vol.7, issue.2, pp.159-174, 2001.

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

Z. Manna and A. Pnueli, Temporal verification diagrams, TACS, pp.726-765, 1994.
DOI : 10.1007/3-540-57887-0_123

D. Méry, Refinement-based guidelines for algorithmic systems, International Journal of Software and Informatics, vol.3, issue.2-3, pp.197-239, 2009.

D. Méry and M. Poppleton, Formal Modelling and Verification of Population Protocols, pp.208-222
DOI : 10.1007/978-3-642-38613-8_15

D. Méry and N. K. Singh, Automatic code generation from event-B models, Proceedings of the Second Symposium on Information and Communication Technology, SoICT '11, pp.179-188, 2011.
DOI : 10.1145/2069216.2069252

S. S. Owicki and L. Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems, vol.4, issue.3, pp.455-495, 1982.
DOI : 10.1145/357172.357178

J. Rehm, Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method, International Journal on Software Tools for Technology Transfer, vol.187, issue.3, 2009.
DOI : 10.1007/s10009-009-0130-5
URL : https://hal.archives-ouvertes.fr/hal-00184837