J. , Modeling in Event-B: System and Software Engineering, 2010.

J. Abrial, M. Butler, and S. Hallerstede, Rodin: an open toolset for modelling and reasoning in Event-B, International Journal on Software Tools for Technology Transfer, vol.12, issue.6, pp.447-466, 2010.

J. Abrial, D. Cansell, and &. 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.
URL : https://hal.archives-ouvertes.fr/inria-00099531

N. Cataño and &. Rivera, EventB2Java: A Code Generator for Event-B, Sanjai Rayadurgam & Oksana Tkachuk, pp.166-171, 2016.

Z. Cheng and D. Méry-&-rosemary-monahan, On Two Friends for Getting Correct Programs -Automatically Translating Event B Specifications to Recursive Algorithms in Rodin, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques -7th International Symposium, pp.821-838, 2016.

A. Edmunds and &. Butler, Tasking Event-B: An extension to Event-B for generating concurrent code, PLACES 2011, 2011.

A. Yanhong, . Liu, D. Scott, B. Stoller, and . Lin-&-michael-gorbovitski, From clarity to efficiency for distributed algorithms, ACM SIGPLAN Notices, vol.47, pp.395-410, 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.

D. Méry, Modelling by Patterns for Correct-by-Construction Process. In: Leveraging Applications of Formal Methods, Verification and Validation. Modeling -8th International Symposium, pp.399-423, 2018.

D. Méry, Verification by Construction of Distributed Algorithms, Theoretical Aspects of Computing -ICTAC 2019 -16th International Colloquium, pp.22-38, 2019.

, Transforming Event B Models into Verified C# Implementations, First International Workshop on Verification and Program Transformation, VPT 2013, vol.16, pp.57-73, 2013.

G. Tel, Introduction to distributed algorithms, 2000.

, Generating Distributed Programs from Event-B Models Nodes: partition(Nodes, P, Q) // Partition of the set of processes P: partition(P, {p}) // Partition of the classes of processes network_typing: network ? Nodes ? P (Nodes) // Network specification network_value: network = {proc· proc ? P|proc ? Q} ? {proc· proc ? Q|proc ? {p}} // States of the processes States: partition(States, {sr}, {wa}, Process states req2msg_typing: req2msg ? MessagePre f ixes Messages // Message types ans2msg_typing: ans2msg ? MessagePre f ixes × Z Messages // Message types Messages: partition(Messages, ran(req2msg), vol.9, p.2, 2016.

, Channels: Channels = Nodes × Nodes ? (Messages ? N × N × N)

/. , Algorithm specific constants (types of exchanged messages, process ressources) MessagePrefixes: partition(MessagePre f ixes, {request}, {answer}) //@P@Q availableResources_typing

, // Communication axioms (general to all algorithms) send: send ? Channels × (Nodes × Nodes) × Messages ? Channels receive: receive ? Channels × (Nodes × Nodes) × Messages ? Channels received: received ? Channels × (Nodes × Nodes) × Messages ? N inChannel: inChannel ? Channels × (Nodes × Nodes) × Messages ? N sent: sent ? Channels × (Nodes × Nodes) × (Messages) ? N reliable: reliable ? Channels ? BOOL emptyChannel: emptyChannel ? Channels axm9: emptyChannel = {x·x ? Nodes × Nodes|x ? {y·y ? Messages|y ? (0 ? 0 ? 0)}} axm10: inChannel = (? c ? x ? y·c ? Channels?x ? Nodes×Nodes?y ? Messages|pr j2

, Messages|pr j2(c(x)(y))) axm13: send = (? c ? x ? y·c ? Channels ? x ? Nodes × Nodes ? y ? Messages|c ? {x ? (c(x) ? {y ? (sent(c ? x ? y) + 1 ? inChannel(c ? x ? y) + 1 ? received(c ? x ? y))})}) axm14: dom(receive) = {c, x, y·c ? Channels ? x ? Nodes × Nodes ? y ? Messages ? inChannel(c ? x ? y) > 0|c ? x ? y} axm15: receive = (? c ? x ? y·c ? Channels ? x ? Nodes × Nodes ? y ? Messages ? inChannel(c ? x ? y) > 0|c ? {x ? (c(x) ? {y ? (sent(c ? x ? y) ? inChannel(c ? x ? y) ? 1 ? received(c ? x ? y) + 1)})}) axm16: reliable = (? c·c ? Channels|bool(?x, y·(x ? Nodes × Nodes ? y ? Messages ? sent, axm11: sent = (? c ? x ? y·c ? Channels ? x ? Nodes × Nodes ? y ? Messages|pr j1(pr j1(c(x)(y)))) axm12: received = (? c ? x ? y·c ? Channels ? x ? Nodes × Nodes ? y ?

=. Rue, axm17: theorem ?c, x, y·(c ? Channels ? x ? Nodes × Nodes ? y ? Messages ? (reliable(c) = T RUE ? reliable

, T RUE)) axm19: theorem reliable(emptyChannel) = T RUE axm20: theorem ?c, x1, x2, y1, y2·(c ? Channels ?x1 ? Nodes×Nodes?y1 ? Messages?x2 ? Nodes× Nodes ? y2 ? Messages ? received(send(c ? x1 ? y1) ? x2 ? y2) = received(c ? x2 ? y2)) axm21: theorem ?c, x1, x2, y1, y2·(c ? Channels ?x1 ? Nodes×Nodes?y1 ? Messages?x2 ? Nodes× Nodes ? y2 ? Messages ? x1 ? y1 = x2 ? y2 ? sent(send(c ? x1 ? y1) ? x2 ? y2) = sent(c ? x2 ? y2) ? inChannel(send(c ? x1 ? y1) ? x2 ? y2) = inChannel(c ? x2 ? y2)) axm22: theorem ?c, x1, x2, y1, y2·(c ? Channels ?x1 ? Nodes×Nodes?y1 ? Messages?x2 ? Nodes× Nodes?y2 ? Messages?x1 ? y1 = x2 ? y2?inChannel(c ? x1 ? y1) > 0?inChannel(receive(c ? x1 ? y1) ? x2 ? y2) = inChannel, axm18: theorem ?c, x, y·(c ? Channels ? x ? Nodes × Nodes ? y ? Messages ? (reliable(c) = T RUE ? inChannel(c ? x ? y) > 0 ? reliable(receive