The complexity of requirements and complexity of operating environments make error detection in early stages of software system development difficult. This paper makes an argument for the use of formal modelling and verification in early stages of system development to identify and eliminate errors in a timely fashion. Precision is key to eliminating errors in requirements while abstraction is key to mastering requirements complexity. The paper outlines the way in which precision and abstraction may be achieved through modelling and how refinement allows the complexity to be managed through layering. The role of model validation and model verification in improving the quality of formal models and in improving the quality of the requirements is also outlined. The formalism used throughout is Event-B supported by the Rodin toolset.