在日前教育部公布的2011年度高等学校科学研究优秀成果奖(科学技术)的授奖项目中,我校软件学院何积丰院士领衔的研究团队完成的“基于模型的可信软件理论与开发方法”荣获自然科学一等奖。
可信软件研究是最近二十年兴起的一门前沿科学,是数学、计算机科学、软件工程等多学科紧密结合的交叉领域,研究方法涉及到数理逻辑、组合数学、计算方法、数学规划、代数、模型论、形式化方法、语义学、程序设计语言、编译、计算机网络等众多科学方向,研究对象覆盖软件理论、软件技术与原理、软件生产过程和管理、以及软件支撑平台等方面。可信软件理论与开放方法的研究和发展对未来软件产业、信息社会的发展具有决定性的作用。基于模型的理论和开发技术,是目前可信软件研究中的最重要和最成功的方法之一。何积丰院士领衔的研究团队在“973”、“863”、国家自然科学基金重大,科技部“核高基”重大科技专项等科研项目资助下,在基于模型的可信软件构造与验证方法、语义模型和语义一致的形式化理论、Web服务模型、基于模型的可信软件验证算法等方面取得了若干具有重要科学价值的创造性成果,主要包括:(1)突破了可信软件设计技术,创造性地建立了基于模型的可信软件构造与验证方法,提出并解决了建模、模型转换与精化、模型验证三个技术难题;(2)建立了语义模型和语义一致的形式化理论,揭示了变迁网络的模型检测与定理证明工具的统一性,为反应式系统的程序一致性理论奠定了基础;(3)建立了可信Web事务的模型和语义: 提出了Web事务处理的新语言,解决了Web事务处理模型的代数语义、指称语义和操作语义的连接问题,研究了Web事务的建模与验证,构建了Web事务的概率组合模型和精化模型;(4)给出了若干基于模型的软件验证新算法,用基于图论、计算机代数和并行计算的方法,在程序可达性和终止性等程序验证问题研究中获得若干新算法;在服务组合的编排、编制与验证研究中建立若干新算法,并研制了相应的工具集。
该项目共发表学术论文150多篇,其中SCI索引25篇,EI索引110篇,国际学术会议特邀报告12次。论文他引次数超过770次。该项目取得的系列研究结果,在基于模型的可信软件理论研究中开辟了一门具有严格数学基础的全新方向,在国际范围内启发了多个研究小组的研究思路,引领了若干有实际工业应用背景的工具集的开发。