Incremental design of distributed systems with Event-B

It is shown how Event-B can be use to model and reason about distributed sys-tems from a high-level global view down to a detailed distributed architectural view. It is shown how refinement and decomposition can be used to introduce distribu-tion of state and control and to introduce message passing between components. Distribution is treated as a special case of concurrency. Techniques are presented for decomposing abstract atomic events into smaller atomic steps in refinement and for decomposing models into sub-models