Abstract: The scale and complexity of software systems continue to increase and the traditional requirement analysis method is difficult to ensure the consistency and correctness of software, which is laying the trouble for the quality of a software system. Practice of the software engineering shows that in the software developing process, the earlier the errors are found and repaired, the less the cost is paid. In order to ensure the quality of software, on the early stage of software development, Event-B can be used to formally describe the software requirements and verify the correctness of the model. In the file system modeling as an example, this paper discusses how to use Event-B method and stepwise refinement to establish and validate the model, so as to ensure the correctness of software.