基于Event-B的形式化建模关键技术研究  

Research on Formally Modeling Based Event-B

作　　者：吴劲[1] 陈志慧[1] 

机构地区：[1]电子科技大学计算机科学与工程学院,成都610054

出　　处：《电子科技大学学报》2014年第3期405-408,共4页Journal of University of Electronic Science and Technology of China

基　　金：中央高校基本科研业务费(ZYGX2011J072);国家科技重大专项(2011ZX03002-002-03);国家自然科学基金重点项目(61133016);四川省科技计划项目(2013GZ0022)

摘　　要：软件系统的规模和复杂程度不断提高而传统的需求分析方法难以确保软件的正确性和一致性,为软件系统的质量埋下了隐患。软件工程的实践表明,在开发过程中,错误发现得越早,修复得越早,付出的代价越小。为了确保软件的质量,可在软件开发的早期需求分析阶段,采用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.

关 键 词：Event-B形式化方法 形式化建模 精化 需求分析 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]