Formal Engineering Methods for Software Development

软件开发的形式化工程方法

• 批准号: 11694173
• 负责人: SHAO-YING Liu
• 金额: $ 5.7万
• 依托单位: Hosei University (2000-2001)Hiroshima City University (1999)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 1999
• 资助国家: 日本
• 起止时间: 1999 至 2001
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-11694173/
• 关键词: Formal engineering methods; SOFL; Formal method; Formal specification; Rigorous review; Specification testing; Software engineering; Software tools; Object-Oriented Design; 形式工学手法; ソフトウェア検証; 厳密なレビュー; 仕様テスト; 仕様分析; 形式的仕様; システム開発; ソフトウェア進化

We have achieved several important results on this project. Firstly, we have developed the SOFL specification language and method into a mature level and completed a book on the introduction to the latest development of SOFL. Secondly, we have developed a rigorous reviews technique by integrating formal proof and fault tree analysis, which supports systematically rigorous reviews of SOFL specifications and other kinds of formal specifications. Thirdly, we have developed an effective testing method for verifying and validating formal specifications, including both explicit and implicit specifications (e.g., with pre and post-conditions), by integrating program testing technique and formal proof approach. By this method formal specifications can be verified and validated before they are implemented. Fourthly, we have explored the power of formal refinement in capturing complete and accurate user requirements, which demonstrates the potential effectiveness in improving the productivity and reliability of software products, finally, we have investigated how formal methods can be used to define, predicate, and control software processes. Our results achieved on this project have contributed to the establishment of Formal Engineering Methods as a new research area.

我们在这个项目上取得了一些重要成果。首先，我们将SOFL规范语言和方法发展到了一个成熟的水平，并完成了一本介绍SOFL最新发展的书。其次，我们开发了一个严格的审查技术，通过集成形式化证明和故障树分析，它支持系统的严格审查SOFL规格和其他类型的形式规格。第三，我们开发了一种有效的测试方法来验证和确认形式规格说明，包括显式和隐式规格说明（例如，结合程序测试技术和形式化证明方法，通过这种方法，形式规格说明可以在实现之前进行验证和确认。第四，我们探讨了形式化精化在捕获完整和准确的用户需求方面的力量，这表明了形式化精化在提高软件产品的生产率和可靠性方面的潜在有效性，最后，我们研究了如何使用形式化方法来定义、预测和控制软件过程。我们在该项目中取得的成果有助于正式工程方法作为一个新研究领域的建立。

项目成果

Shaoying Liu: "Integrating UML and SOFL for Object Oriented Design"Proceedings of The Third International Conference on Computer and Information Technology (CIT2002), Aizu-Wakamatsu City, Japan, September 11-14. (to appear). (2002)

Shaoying Liu：“Integrating UML and SOFL for Object Oriented Design”第三届计算机与信息技术国际会议 (CIT2002) 论文集，日本会津若松市，9 月 11-14 日。

Takaaki Nakano, Shaoying Liu: "Improving Software Process Quality Using Formal Engineering Methods"Proceedings of Foundation of Software Engineering 2001 (FOSE2001), Kindai Science Press, November. 163-166 (2001)

Takaaki Nakano、Shaoying Liu：“使用形式工程方法提高软件过程质量”2001 年软件工程基础论文集 (FOSE2001)，近代科学出版社，11 月。

Hassan Gomaa, Shaoying Liu, Michael Shin: "Integration of Domain Modeling Method for Families of Systems with the SOFL Formal Specification Language"Proceedings of 6th IEEE International Conference on Engineering Complex Computer Systems, IEEE Cs Press. S

Hassan Gomaa、Shaoying Liu、Michael Shin：“系统族领域建模方法与 SOFL 形式化规范语言的集成”第六届 IEEE 国际复杂计算机系统工程会议论文集，IEEE Cs Press。

Shaoying Liu: "Software Development by Evolution"Proceedings of Second International Workshop on Principles of Software Evolution(IWPSE99). July. 12-16 (1999)

刘少英：《软件进化论开发》第二届国际软件进化原理研讨会论文集(IWPSE99)。

A Jeff Offutt, Yiwei Xiong, Shaoying Liu: "Criteria for Generating Specification-based Tests"Proceedings of Fifth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'99), IEEE Computer Society Press, Las Vegas, Nevada, USA, Oc

A Jeff Offutt、Yiwei Xiong、Shaoying Liu：“生成基于规范的测试的标准”第五届 IEEE 国际复杂计算机系统工程会议 (ICECCS99) 论文集，IEEE 计算机协会出版社，美国内华达州拉斯维加斯，Oc