Formal Methods and Intelligent Software Engineering Environments

我们已经朝着FM-ISEE项目的目标取得了实质性的进展，该项目的目标是开发一种比现有方法更强大、用户友好和实用的形式化方法来开发可伸缩的软件系统，并对构建支持该形式化方法的智能软件工程环境进行研究。在1997财政年度，我们取得了以下具体成果：1.设计并改进了实用的形式化方法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.