2010 | OriginalPaper | Chapter
Event-B Decomposition for Parallel Programs
Authors : Thai Son Hoang, Jean-Raymond Abrial
Published in: Abstract State Machines, Alloy, B and Z
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 split 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.