基于rCOS的形式化方法需求分析与验证

Requirements analysis and validation is one of important problems in software engineering. This project will apply rCOS formal method to building the requirements models of software systems, as well the consistency validation among requirements. A functional requirement, i.e., a use case in UML, can be defined as a sequence of system operations, which is described in a system operation diagram. And each use case can be formally defined as a pair of pre and post conditions. We will extend the current research results on theory, and develop the related software tools for supporting the incremental and iterative RUP development process. Extending and Applying developed AutoPA tool(based on OCL), we can automatically generate the corresponding prototype in Java from the given formal requirements model. Through the prototyping, customers can validate whether the specified requirements are consistent with what they really need. Thus, we can obtain the correct and reliable formal requirements model during requirements analysis phase. Currently, there is still no successful result on this research problem. The proposed research will make theory close a big step to practice in software engineering, which is very valuable and meaningful.

需求分析和验证是软件工程中的重要课题之一。本课题将应用rCOS形式化方法支持软件系统需求模型建立及其一致性验证。功能需求,即UML中的用例(use case)可以定义成为由一组按UML系统时序图控制的系统操作(system operations)构成, 而每个系统操作又可形式化成一对前后置条件。我们将扩充已有的理论并开发相关的软件支持工具,用以支持RUP迭代增量统一开发过程的形式化需求模型生成,及需求之间一致性的检查。扩充和利用已开发的基于OCL的原型(prototype)自动生成工具AutoPA，快速生成系统需求模型的原型Java代码。从而用户可以确认需求功能是否是其所需。如此可在需求分析阶段,得到正确可靠的形式化的需求规范。目前这方面的研究还在摸索实验阶段。此研究可使理论向实际软件工程靠近一大步,是非常有价值和意义的。

需求分析和验证是软件工程中的重要课题之一。本课题将应用rCOS形式化方法支持软件系统需求模型建立及其一致性验证。功能需求,即UML中的用例(use case)可以定义成为 由一组按UML系统时序图控制的系统操作(system operations)构成, 而每个系统操作又形式化成一对前后置条件。我们扩充了已有的理论并开发相关的软件支持工具,用以支持RUP迭代增量统一开发过程的形式化需求模型生成,及需求之间一致性的检查。开发完成需求建模和验证工具RM2PT，快速生成系统需求模型的原型 Java代码。从而用户可以确认需求功能是否是其所需。.通过研究从UML状态图到B形式规范的转换规则,提出了一种基于XMI的状态图到B形式化规范的自动转换方法,并使用J ava语言实现了自动转换工具 UML２B. 如此可在需求分析阶段得到正确可靠的形式化的需求规范。本项目给出了一个列车控制系统需求分析的实例研究。目前需求分析和验证的研究还在摸索实验阶段,此研究可使理论向实际软件工程靠近一大步,是非常有价值和意义的。