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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com