Formal Methods and Intelligent Software Engineering Environments

我们已经朝着FM-ISEE项目的目标取得了实质性的进展，该目标是开发一种比现有的更强大、用户友好和实用的形式化方法来开发可靠的软件系统，并对构建一个支持形式化方法的智能软件工程环境进行研究。在1997财政年度，我们取得了以下具体成果：设计并改进了实用的形式化方法SOFL。将现有的形式化方法Z和所提出的SOFL分别应用于复杂信息系统，并对结果进行了比较和评价。“形式化工程方法”的提出和发展是为了提供一种新的、实用的方法，将形式化方法广泛地应用于工业。与形式化方法相比，形式化工程方法提供了三个方面的进步：(1)整合图形符号、自然语言和规范的形式化符号；(2)强调演进方法而不是现有的细化方法来转换规范；(3)用严格的评审代替正式的证明来进行系统的验证和确认。研究了规格测试和基于规格的测试技术。这两种技术旨在解决不同的问题。前者的目的是验证和确认形式规范，后者的目的是确保基于规范实施的程序满足规范和用户需求。为了帮助构建SOFL的编译器和支持环境，定义了SOFL的公理语义和操作语义。构建了SOFL的图形用户界面原型和规格测试支持工具原型。基于以上研究，在国内外期刊上发表论文8篇。

We have made substantial progress towards the goals of the FM-ISEE project taht are to develop a more powerful, user-friendly and practical formal method for developing raliable software systems than those currently existing, and to conduct research on the construction of an intelligent software engineering environment to support the formal methods. In the fiscal year of 1997 we have achieved the following specific results :1. The practical formal method SOFL is designed and improved.2. Both the existing formal method Z and the proposed SOFL are applied to complicated information systems and the results are compared and evaluated.3. "Formal Engineering Methods" are proposed and developed to provide an new, Practical approach to applying formal methods in industry at large. compared with formal methods, formal engineering methods offer three progresses : (1) integrate graphical notation, natural languages, and formal notation for specifications ; (2) emphasize evolution approach rather than the existing refinement approach for transforming specifications ; and (3) substitute formal proofs with rigorous reviews for system verification and validation.4. Specification testing and specification-based testing techniques are investigated. These two techniques are intended to solve different problems. The former aims to verify and validate formal specifications while the latter aimes to ensure that the programs implemented based on the specifications satisfy the specifications and the user requirements.5. To help the construction of a complier and support environment for SOFL,the axiomatic semantics and operational semantics of SOFL are defined.6. The prototypes of the graphical user interface and spedification testing support tool for SOFL are built. Eight (8) papers are published in the refereed journals and internationals based on the above research.