A Formal Approach to Requirements Analysis and Design

该项目通过将面向对象的分析和设计与形式化方法相结合来解决与需求分析和设计相关的困难。面向对象的图表方法的形式化正在开发中，关于其图表含义的推理规则的框架正在定义中。关系图被视为数据类型定义，这些规则允许自动检查定义的一致性。图形化方法包括定义对象建模技术的三种常用图形符号：(1)对象模型、(2)数据流图和(3)用于执行需求分析的状态图。因此，为这些符号定义的规则为需求分析提供了正式的基础，并允许将经过严格检查的图表用作正式规范。作图规则对一致性有相应的证明义务。自动化技术用于确定系统需求的一致性和完整性，如图所示。使用一组图的转换规则及其对应的形式化规范来派生设计，指导实现过程，并验证开发的代码。正在开发一个基于图形的原型环境，该环境封装了正规化过程以及现有的规范和程序开发工具。

This project addresses the difficulties associated with requirements analysis and design by combining object-oriented analysis and design with formal methods. A formalization of an object-oriented diagramming method is being developed, and a framework of rules for reasoning about the meaning of its diagrams is being defined. Diagrams are treated as data type definitions, and the rules enable the automated checking of the consistency of the definitions. The diagramming method comprises three commonly used graphical notations that define the Object Modeling Techniques; (1) object models, (2) data flow diagrams, and (3) state charts, which have been used to perform requirements analysis. As such, the rules defined for these notations provide a formal basis for requirements analysis and allow the rigorously checked diagrams to be used as formal specifications. Diagram composition rules have corresponding proof obligations regarding consistency. Automated techniques are used to determine the consistency and completeness of a system's requirements as depicted by the diagrams. A set of transformation rules for diagrams and their corresponding formal specifications are used to derive designs, guide the implementation process, and validate the developed code. A graphics-based prototype environment is being developed that encapsulates the formalization process and existing specification and program development tools.