Research on rigorous verification techniques formal specification and design

严格验证技术形式化规范与设计研究

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

We have conducted intensive research to explore rigorous techniques for verifying formal specifications and designs of software systems, and achieved several important results. Firstly, we have combined formal verification and the fault tree analysis technique to establish a rigorous reviews method. By this method, proof obligations for various properties of a specification are automatically derived from the specification, and then a review plan is automatically generated and represented graphically. By reviewing the tasks in this graphical representation, we can check whether the specification has faults or not. Secondly, 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. Finally, we have built a prototype of software tool to support specification testing and conducted a case study to evaluate the effectiveness of our testing method.

我们进行了深入的研究，探索验证软件系统形式规格说明和设计的严格技术，并取得了几个重要成果。首先，我们将形式验证和故障树分析技术相结合，建立了一种严格的评审方法。通过这种方法，规范的各种属性的证明义务自动从规范中派生出来，然后自动生成审查计划并以图形表示。通过查看此图形表示中的任务，我们可以检查规范是否有错误。其次，通过将程序测试技术与形式证明方法相结合，开发了一种有效的形式化规范验证和验证方法，包括显式规范和隐式规范(如带有前置条件和后置条件)。通过这种方法，可以在正式规范实现之前对其进行验证和验证。最后，我们构建了一个支持规格说明测试的软件工具原型，并进行了一个案例研究来评估我们的测试方法的有效性。

项目成果

Shaoying Liu, Jin Song Dong: "Class and Module in SOFL"Proceedings of Second Asia-Pacific Conference on Quality Software IEEE Computer Society Press. December. 241-245 (2001)

刘少英，董劲松：《SOFL 中的类和模块》第二届亚太质量软件会议论文集 IEEE 计算机学会出版社。

Shaoying Liu: "Capturing Complete and Accurate Requirements by Refinement"Proceedings of 8th IEEE International Conference on Engineering of Complex Computer Systems, Greenbelt, Maryland, USA, December 2-4. (to appear). (2002)

Shaoying Liu：“通过细化捕获完整且准确的需求”第八届 IEEE 国际复杂计算机系统工程会议论文集，美国马里兰州格林贝尔特，12 月 2-4 日。

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. October. 119-129 (1999)

A Jeff.Offutt、Yiwei Xiong、Shaoying Liu：“生成基于规范的测试的标准”第五届 IEEE 国际复杂计算机系统工程会议论文集（ICECCS99），IEEE 计算机学会出版社。

Shaoying Liu: "Developing Quality Software Systems Using the SOFL Formal Engineering Method (invited paper)"Proceedings of 4th International Conference on Formal Engineering Methods (ICFEM2002), LNCS Springer-Verlag, Shanghai, China, October 21-25. (to ap

Shaoying Liu：“使用 SOFL 形式工程方法开发质量软件系统（特邀论文）”第四届形式工程方法国际会议 (ICFEM2002) 论文集，LNCS Springer-Verlag，中国上海，10 月 21-25 日。

Shaoying Liu, Jin Song Dong: "Class and Module in SOFL"Second Asia-Pacific Conference on Quality Software. Dec.10-11. 241-245 (2001)

Shaoying Liu，Jin Song Dong：“SOFL 中的类和模块”第二届亚太质量软件会议。