creators_name: Hoang, Thai Son creators_name: Abrial, Jean-Raymond creators_id: htson@inf.ethz.ch creators_id: jabrial@inf.ethz.ch type: conference_item datestamp: 2010-02-05 10:39:21 lastmod: 2010-02-05 10:39:21 metadata_visibility: show title: Event-B Decomposition for Parallel Programs ispublished: inpress subjects: deploy_method_comp full_text_status: none pres_type: paper abstract: We present here a case study developing a parallel program. The approach that we use combines refinement and decomposition techniques. This involves in the first step to abstractly specify the aim of the program, then subsequently introduce shared information between sub-processes via refinement. Afterwards, decomposition is applied to separate the resulting model into sub-models for different processes. These sub-models are later independently developed using refinement. Our approach aids the understanding of parallel programs and reduces the complexity in their proofs of correctness. date: 2010-02 date_type: published event_title: ABZ2010 event_type: conference refereed: TRUE citation: Hoang, Thai Son and Abrial, Jean-Raymond (2010) Event-B Decomposition for Parallel Programs. In: ABZ2010. (In Press)