Study on Formal Methods Applicable to Practical Software Development

适用于实际软件开发的形式化方法研究

• 批准号: 21300009
• 负责人: ARAKI Keijiro
• 金额: $ 8.99万
• 依托单位: Kyushu University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2009
• 资助国家: 日本
• 起止时间: 2009 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21300009/
• 关键词: ソフトウェア工学; フォーメルメソッド適用; ソフトウェア開発プロセス; 形式仕様記述; 産学連携; 開発文書品質向上; フォーマルメソッド適用; 形式的システム記述; 非形式的システム記述; 形式手法導入ガイド; 形式手法適用支援ツール; 文書品質向上支援; 形式手法人材育成; 形式手法導入方法; 文書品質改善支援; ソフトウェア開発法プロセス; 導入方法

We present practically applicable guidelines to introduce formal methods to software development at Japanese companies through Industry-Academia collaboration in applying formal methods to real system development. Especially, we made trials to perform PBL(Project Based Learning) courses to adopt formal methods to the upper stages of system development process with technical supports on domain knowledge and project management from company engineers, and then we showed the effectiveness of PBL under Industry-Academia collaboration to transfer technology on formal methods to system development projects at Japanese companies.We also adopted formal methods in system development processes based on PSP(Personal Software Process) and TSP(Team Software Process), and show the reference models to introduce formal methods into traditional system development processes in system development projects. We present a framework to describe formal system models in VDM both for system analysis/validation and system implementation.We developed a prototype tool which supports system developers to describe formal system models from initial informal documents on system requirement, specification

我们提出了实用的指导方针，通过产学研合作将正式方法应用到实际的系统开发中，从而将正式方法引入日本公司的软件开发中。特别是，在公司工程师的领域知识和项目管理的技术支持下，尝试将基于项目的学习(PBL)课程应用于系统开发过程的较高阶段，展示了产学研合作下的PBL将形式化方法的技术转移到日本公司系统开发项目的有效性；还在基于PSP(个人软件过程)和TSP(团队软件过程)的系统开发过程中采用了形式化方法，并展示了在系统开发项目中将形式化方法引入传统系统开发过程的参考模型。我们提出了一种用于系统分析/验证和系统实现的VDM中形式化系统模型的描述框架。我们开发了一个原型工具，它支持系统开发人员从系统需求、规格说明的初始非正式文档中描述形式化的系统模型

项目成果

ドキュメントの品質と開発プロセスにおけるコミュニケーションでのフォーマルメソッドの有用性

记录质量以及开发过程中沟通中正式方法的有用性

• 发表时间: 2010
• 作者: 伊藤祥司;片桐孝洋;櫻井隆雄;猪貝光祥;大島聡史;黒田久泰;直野健;Hidehiko Masuhara;荒木啓二郎
• 通讯作者: 荒木啓二郎

形式手法に基くシステム開発

基于形式化方法的系统开发

• 发表时间: 2010
• 作者: Michael Perscheid;Michael Haupt;Robert Hirschfeld;高橋篤司;葛原茂樹;荒木啓二郎
• 通讯作者: 荒木啓二郎

Formal Methodsの課題と今後の展開

正式方法的问题和未来的发展

• 发表时间: 2010
• 作者: Yamamoto;Y.;Fukaya T.;荒木啓二郎
• 通讯作者: 荒木啓二郎

大学での科学・工学的アプローチ例

大学科学和工程方法的例子

• 发表时间: 2010
• 作者: Shoji Itoh;Masaaki Sugihara;日下部茂
• 通讯作者: 日下部茂

ソフトウェア開発における「モデル」雑感

关于软件开发中“模型”的各种想法

• 发表时间: 2010
• 作者: 金子朋子;山本修一郎;田中英彦;松林公蔵;荒木啓二郎
• 通讯作者: 荒木啓二郎