An Introduction of A Formal Method in PBL : A Case Report

概要

論文の詳細を見る
In this paper, we report our PBL whose aim is to establish a guideline to introduce formal methods into software development in a company, one of the partners in business-academia collaboration to foster highly skilled ICT personnel. We selected VDM as a formal method, while it is hard for VDM beginners to verify VDM specifications using rigorous mathematical approaches. In this PBL, we tried to ensure the quality of VDM specification with validation using test called specification animation instead of mathematical verification. We also considered the problems of irregularity of VDM specification from the viewpoints of abstraction level in addition to granularity. Then, we proposed a process model in which we develop a formal specification in a style of pair programming, and decoupling the review team from the modeling team. Finally at the end of PBL, our client regarded us with high esteem.
2011-06-23