Formal Methods and Intelligent Software Engineering Environments

形式化方法和智能软件工程环境

• 批准号: 08044167
• 负责人: LIU Shaoying
• 金额: $ 7.68万
• 依托单位: Hiroshima City University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for international Scientific Research
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 1997
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08044167/
• 关键词: Formal Methods; Formal Specification; Software Engineering Environments; Software Verification; Software Testing; Rigorous Reviews; Formal Semantics; SOFL; 形式手法; 形式仕様; 支援環境; 形式意味

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.

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

项目成果

Shaoying Liu: "Evolution:A More Practical Approach than Refinement for Software Development" Proceedings of Third IEEE International Conference on Engineering of Complex Computer Systems. Sept.142-151 (1997)

Shaoying Liu：“进化：软件开发比细化更实用的方法”第三届 IEEE 复杂计算机系统工程国际会议论文集。

Chris Ho-Stuart and Shaoying Liu: ""A Formal Operational Semantics for SOFL"" Proceedings of 1997 Asia-pacific Software Engineering Conference, IEEE Computer Society Press, Hong Kong, December 2-5. 52-61 (1997)

Chris Ho-Stuart 和 Shaoying Liu：““SOFL 的正式操作语义””1997 年亚太软件工程会议论文集，IEEE 计算机学会出版社，香港，12 月 2-5 日。

Shaoying Liu: "A Formal Definition of FRSM and Applications" International Journal of Software Engineering and Knowledge Engineering. 8・3. (1998)

刘少英：“FRSM 的形式化定义及其应用”国际软件工程与知识工程杂志（1998 年）。

Shaoying Liu: ""Evolution : A More Practical Approach than Refinement for Software Development"" Proceedings of Third IEEE International Conference on Engineering of Complex Computer Systems, IEEE Computer Society Press, Villa Olmo, Como, Italy, September

Shaoying Liu：““进化：软件开发比细化更实用的方法””第三届 IEEE 国际复杂计算机系统工程会议论文集，IEEE 计算机协会出版社，意大利科莫奥尔莫别墅，9 月

Shaoying Liu: ""A Formal Definition of FRSM and Applications"" International Journal of Software Engineering and Knowledge Engineering. Vol.8, No.3. (1998)

Shaoying Liu：““FRSM 的正式定义及其应用””国际软件工程和知识工程杂志。