论文部分内容阅读
在传统的软件开发过程中，通常采用非形式化或半形式化方法作为软件需求描述的手段，但是非形式化方法和半形式化方法都无法避免自然语言描述方式为软件需求描述带来的缺陷和错误，所以传统的软件开发方式无法在需求分析阶段确保软件需求的正确性。传统的软件需求建模方式，如UML建模的目的是在需求分析阶段描述软件系统的功能，并不提供验证软件需求描述正确性的方式，然而形式化的软件需求描述方式却提供了在需求阶段确保软件需求描述正确性的方法。形式化方法以严格的数学理论为基础，应用数学的手段来设计、模拟和分析软件系统，建立像数学公式那样精确的软件系统模型，再以模型验证作为检测软件系统模型正确性的手段，通过验证的软件系统模型具有准确性、确定性的特点，从而避免了软件系统在需求阶段的缺陷和错误，达到了确保软件系统质量的目的。为了避免非形式化方法和半形式化方法为软件需求描述带来的二义性和不一致性，本文采用Event-B形式化规约语言作为建立软件系统模型的描述语言，首先阐述了在Rodin平台下，利用Event-B形式化规约语言建立软件模型的步骤和方法，然后讲述了基于Rodin平台验证模型的全过程，主要内容包括以下几个方面：1.研究了传统软件工程方法为软件开发带来的弊端以及形式化软件需求描述方法的特点和形式化方法的研究现状。2.研究了Event-B模型的结构和精化技巧，首先介绍了Event-B模型的两个主要组成部分context和machine的特点以及二者之间的联系，然后讲述了常用的精化技巧，包括事件精化和状态精化，最后简要介绍了Rodin平台的功能。3.研究以树型文件系统为例构建并验证Event-B模型的步骤和方法，首先建立一个树型文件系统的抽象模型，然后再利用逐步精化的方式采用各种精化技巧依次向抽象模型中添加树型文件系统的属性和功能，达到扩大和丰富模型的目的。4.研究基于Rodin平台的Event-B模型的验证方式，讲述了与Event-B模型验证密切相关的证明义务、推理规则和证明策略等内容以及树型文件系统模型的证明过程，帮助形式化软件开发人员更好的理解模型证明和Rodin平台。5.结束语部分总结了本文的研究成果和对未来工作的展望。本文基于Event-B形式化方法，以树型文件系统的软件需求获取为实例详细地展示了用Event-B作为形式化方法基于Rodin平台建立树型文件系统模型的过程中如何描述树型文件系统的功能和属性，并验证建立的树型文件系统模型的正确性，阐述了用Event-B形式化方法描述软件需求建立并验证模型的全过程。