Study on Formal Methods Applicable to Practical Software Development

我们提出了实际适用的指导方针，通过产学合作将正式方法应用于真实的系统开发，将正式方法引入日本公司的软件开发。特别是，我们尝试进行PBL（基于项目的学习）课程，采用正式的方法，以系统开发过程的上层阶段与技术支持的领域知识和项目管理，从公司工程师，然后我们展示了PBL在工业中的有效性，学术界合作，将形式方法的技术转移到日本公司的系统开发项目中。我们还在系统开发中采用了形式方法基于PSP（PersonalSoftwareProcess）和TSP（TeamSoftwareProcess）的系统开发过程，给出了在系统开发项目中将形式化方法引入传统系统开发过程的参考模型。本文提出了一个用于系统分析/验证和系统实现的形式化系统模型描述框架，并开发了一个原型工具，支持系统开发人员从初始的非正式文档描述系统的需求、规格说明和模型

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