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.