中文摘要：

软件系统的规模和复杂程度不断提高而传统的需求分析方法难以确保软件的正确性和一致性，为软件系统的质量埋下了隐患。软件工程的实践表明，在开发过程中，错误发现得越早，修复得越早，付出的代价越小。为了确保软件的质量，可在软件开发的早期需求分析阶段，采用Event-B形式化方法描述软件的需求，并验证模型的正确性。以文件系统建模为例，该文讨论了如何利用Event-B方法，采用逐步精化的方式建立并验证模型，确保软件的正确性。

英文摘要：

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.