Study on Formal Methods Applicable to Practical Software Development

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

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