报告题目： Formal Engineering Methods for Software Quality Assurance and Their Future Development
报告人： 刘少英 教授
主持人： 缪炜恺
报告时间：6月27日（周二）16:00—17:30 
报告地点：中北校区数学馆201

报告人简介：

1982 年 1 月毕业于西安交通大学， 1992 年从英国曼彻斯特大学获得计算机科学博士学位，现为日本法政大学计算机科学教授。 主要研究领域包括软件工程， 软件开发的形式化工程方法， 软件设计方法，程序验证， 软件测试，以及智能软件工程环境。从 1994 年以来，已领导和主持由日本文部科学省，国立信息研究所（NII），大川情报科学财团，以及日本信号， NTT Data和三菱电机等日本政府， 财团和大企业分别资助的 20 个以上的研究项目， 创立和发展了“软件开发的形式化工程方法”，研制开发了 SOFL 形式化工程开发语言和方法，由 Springer 出版专著一本， 编著由 IEEE CS Press 和 Springer LNCS 系列出版的论文集 10 本，在包括 IEEE Transactions on Software Engineering, IEEE Transactions on Reliability, Journal of Systems and Software 等国际学术期刊和国际会议发表 160 多篇论文。 曾被`Journal of Systems and Software 评为 1993 年至1996 年期间的在系统和软件工程领域的世界 top 15 名学者之一， 1996 年获得由 IEEE 国际会议授予的”优秀论文奖“， 2010 年 6 月被英国计算机协会授予 Fellow, 2017 年 6 月获得 IEEE 可靠性协会日本分会的 2016 年论文奖。 曾多次担任 ICFEM， ICECCS 等国际会议的大会主席和程序委员会主席， 以及数目繁多的国际会议的 PC 委员。 现任 IEEE Transactions on Reliability 和 Software Testing，Verification and Reliability(STVR)期刊的 Associate Editor。 是 IEEE 高级会员， 日本软件科学会会员。个人主页：http://cis.k.hosei.ac.jp/~sliu/

报告摘要：

        Conventional software engineering on the basis of informal or semi-formal methods is facing tremendous challenges in ensuring software quality and productivity. Formal methods have attempted to address those challenges by introducing mathematical notation and calculus to support formal specification, refinement, and verification in software development. The theoretical contributions of formal methods to the discipline of software engineering are significant. However, in spite of their potential in improving the controllability of software process and reliability, formal methods are generally difficult to apply to large-scale and complex systems in practice because of many constraints (e.g., limited expertise, complexity, changing requirements, and theoretical limitations).

         We have developed “Formal Engineering Methods’’ (FEM) as a research area since 1989 to study how formal methods can be effectively integrated into conventional software engineering technologies and process models so that formal techniques can be tailored, revised, or extended to fit the need for improving software productivity and quality in practice (e.g., through the enhancement of the usability of formalism and the tool supportability of the relevant methods). We have also developed a specific FEM called Structured Object-Oriented Formal Language (SOFL) that offers rigorous but practical techniques for system modeling, transformation, and verification, including a three-step formal specification approach, transformation from structured specification to object-oriented implementation, and specification-based inspection and testing. The effective combination of these three techniques can significantly enhance software productivity and quality. The SOFL method has also achieved a good balance among simplicity, visualization, and precision to allow engineers to easily use the method. In this talk, I will first give a brief introduction to FEM and then focus on the issue of how SOFL is used for software quality assurance, and finally explain the future development directions in the field.