Towards a Method for the Decomposition by Refinement in Event-B

摘要

Refinement consists of detailing the specification in order to get a more concrete model. However, this technique leads to large models. Hence, model decomposition is used to reduce model complexity. In this paper, we present the main methods of decomposition and their limitations. Then, we define the decomposition by refinement method that deals with these limitations. Thereafter, we proceed with the rules to follow in order to get a correct decomposed model.