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.