Abstract:


Event-B Development of the FindP Program


Thai Son Hoang and Jean-Raymond Abrial




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.