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. ***