Integrating Informal and Formal Techniques: An Evolutionary Approach to Systems Development

形式化方法由定义良好的规范语言和严格定义的一组规则组成，这些规则可用于对用该语言表达的规范进行推理。规范语言用于描述预期的系统行为。为了促进对软件开发的形式化方法的使用，特别是对高保证系统的使用，这个项目的目标是产生一组集成的技术，支持在软件开发的所有阶段使用形式化方法。为了达到这个目的，一些新的技术和工具正在被开发出来，以支持软件工程中形式化方法的应用。这些工具包括支持从正式规范中正确推导程序的工具，正式指定需求分析和设计信息的工具，基于正式规范确定软件重用的工具，对现有软件进行逆向工程以获得正式描述的工具，以及静态地分析需求规范的完整性和一致性的工具。可以使用自动化技术检查正式规范的一致性和完整性。然而，在项目的初始阶段，直接构造正式的规范可能是困难的。相反，许多开发人员发现创建图来为他们的系统建模更直观。作为一种弥合正式和非正式软件开发方法之间差距的方法，本研究调查了一种常用的建模符号的形式化，称为对象建模技术。该符号包括三个互补的图：对象（实体-关系）图、状态图和数据流图。这三个图分别为给定系统的体系结构（静态）、行为（动态）以及数据流和服务建模。形式化研究的结果将使从图中自动生成形式化规范成为可能。下一步是研究和开发三个模型集成的形式化语义。最后，研究了可应用于图和相应规范的设计转换。＊＊＊

A formal method consists of a well-defined specification language and a rigorously defined set of rules that can be used to reason about the specifications expressed in that language. The specification language is used to describe the intended system behavior. In order to facilitate the use of formal methods for software development, particularly for high-assurance systems, the objective of this project is to produce a set of integrated techniques that support the use of formal methods for all phases of software development. Towards this end, several new techniques and tools are being developed that support the application of formal methods for software engineering. These include tools to support correct program derivation from formal specifications, to formally specify requirements analysis and design information, to determine software reuse based on formal specifications, to reverse engineer existing software to obtain formal descriptions, and to statically analyze requirements specifications for completeness and consistency. Formal specifications can be checked for consistency and completeness using automated techniques. However, during the initial phases of a project, it may be difficult to construct formal specifications directly. In contrast, many developers find it more intuitive to create diagrams to model their systems. As a means to bridge the gap between formal and informal approaches to software development, this research investigates the formalization of a commonly used modeling notation, known as the Object Modeling Technique. The notation comprises three complementary diagrams: object (entity-relation) diagrams, state diagrams, and data flow diagrams. These three diagrams, respectively, model the architecture (static), behavior (dynamic), and data flow and services of a given system. The results of the formalization studies will enable the automated generation of formal specifications from diagrams. The next step is to investigate and develop formal semantics for the integration of the three models. Finally, design transformations are studied that can be applied to the diagrams and the corresponding specifications. ***