Requirement Analysis for Event-B Modeling

Event-B, a system level modeling language, models a system using a formalism based on a set theoretical first order logic. Refinement plays an important part for reducing system complexity in Event-B modeling. A poor refinement strategy may lead to plaguing errors. System components are the most important factor for building a good refinement strategy. We view that requirement analysis is vital to get a good refinement strategy. This paper discusses finding system components by analyzing system requirements as a preliminary step for modeling. We explain our requirement analysis method.