王义,欧洲科学院院士,IEEE Fellow,2138com太阳集团院长、教授。主要从事实时计算机系统建模、设计与验证方面的研究。主持了多项欧盟研究基金、瑞典自然科学基金、瑞典战略基金、及瑞典技术开发委员会基金、中国自然科学重点基金支持的多项重点重大科研项目。迄今发表论文150余篇,总引用次数12294次,H-index为55,单篇最高引用2425余次。
其主要学术贡献包括:
(1)实时系统验证:UPPAAL系统的创始人
在实时系统模型检测领域做出了若干原创性的理论贡献,创造性地使用诸如状态空间削减、时间约束表达等多种全新的理论方法来有效地解决状态空间爆炸问题。带领学生开发了著名的模型检测工具UPPAAL。经过22年努力,UPPAAL系统已经是实时计算机系统的标准分析工具。UPPAAL系统被广泛应用于汽车、通信、航空和航天等领域中电子系统的设计与验证。关于UPPAAL的第一篇论文,在1972年以来软件领域发表的七万余篇论文中被评为最有影响的十篇论文之一。由于创立UPPAAL系统,王义教授与瑞典Pettersson教授共同获得2013年的CAV奖(CAV奖被认为计算机系统验证领域的最高奖)。
(2)实时系统调度理论
解决了单处理器调度可行性判定的复杂度问题(实时调度理论根本问题),相关论文获得2015年IEEE实时系统年会(RTSS)和欧洲实时系统年会(ECRTS)最佳论文奖。2002年首次提出用时间自动机技术解决资源调度问题(TACAS 2002)。为了降低分析复杂度,2011年把图的概念引入调度模型(RTAS 2011),并创造性地用动态规划技术解决了复杂实时系统的可调度分析问题。在混合关键系统方面的一项工作获得2012年欧洲实时系统年会杰出论文奖,并被IEEE实时系统技术委员会选为实时系统经典论文之一。在多核计算机系统资源调度领域也做出了重要理论贡献,与学生合作将单处理机调度中著名的Liu & Layland资源利用率界限及其它参数化资源利用率界推广到多处理机调度,解决了多处理器调度中四十年悬而未决的著名理论难题。提出了多核处理器上实时任务集响应时间上界的分析方法,此结果获得2009年IEEE实时系统年会(RTSS)最佳论文奖。这些成果为多核处理器在高性能低功耗实时系统中的应用奠定了理论基础。
(3)实时系统理论模型
王义教授上个世纪九十年代初期创立了时间进程代数TCCS,对实时系统理论的研究产生了深远的影响。他提出的连续时间模型及操作语义早在九十年代就被写入实时系统教科书,并被应用于ISO国际标准组织电信系统描述语言标准E-LOTOS。
王义教授获得的各类学术奖励包括:
1) CAV Award 2013(for the development of UPPAAL)
2) 顶级国际会议RTSS 2015最佳论文奖
3) 顶级国际会议ECRTS 2015杰出论文奖
4) 著名国际会议DATE 2013最佳论文奖
5) 顶级国际会议RTSS 2009最佳论文奖
6) 顶级国际会议RTAS 2011、RTSS 2010、RTAS 2010最佳论文提名
7) ETAPS 2002 Best Tool Paper Award,欧洲软件年会最佳工具奖