Incremental Design of Distributed Systems with Event-B
Michael J. Butler · NATO science for peace and security series. D, Information and communication security · 2009
It is shown how Event-B can be use to model and reason about distributed systems 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 distribution 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.