近日，重庆研究院高性能计算应用研究中心副研究员刘江作为第一作者的研究成果《多项式动力系统的半代数不变式计算》（Computing Semi-Algebraic Invariants for Polynomial Dynamical Systems）荣获“IEEE/ACM嵌入式软件国际会议”（IEEE/ACM International Conference on Embedded Software）时间检验奖（EMSOFT Test of Time Award）。

EMSOFT是IEEE/ACM Embedded Systems Week（ESWEEK）三大核心会议之一，也是嵌入式软件领域具有重要国际影响力的顶级会议，为该领域前沿研究交流的主要阵地。ESWeek自2019年起设立“Test of Time Awards”奖项，表彰旗下CASES、CODES+ISSS、EMSOFT中已产生重大且持久影响的论文，被誉为“ESWeek最负盛名的奖项”。其中，EMSOFT Test of Time Award专门表彰发表于EMSOFT，经过约十年以上时间检验，仍对嵌入式软件领域具有重要学术价值与深远影响力的里程碑式论文。

该获奖成果发表于2011年在中国台北举行的第11届ACM嵌入式软件国际会议（EMSOFT 2011）。论文三位作者均来自中国科学院，合作者包括中国科学院软件研究所詹乃军研究员（现为北京大学计算机学院博雅特聘教授）和赵恒军博士（现为西南大学计算机与信息科学学院副教授）。这是EMSOFT Test of Time Award首次授予署名单位均在中国、且全部获奖作者均为中国学者的论文。

论文关注的是多项式动力系统（PDS）中“半代数不变式”的自动发现与验证问题。动力系统广泛存在于物理仿真、控制工程和嵌入式软件所描述的实际过程中；不变式则刻画了系统在演化过程中始终不会越过的“安全边界”。

图1  不变式概念

如果能够自动找到并证明这样的不变式，就能为安全攸关系统的可靠性提供严格的数学保障。该论文的核心贡献在于：为带有定义域和初始条件的多项式动力系统建立了一套可靠且完备的半代数不变式判定准则，并由此给出了一种基于模板假设与半代数约束求解的不变式生成方法。

图2  主要结果

成果中“相对完备性”的结论意味着，只要不变式存在于预先给定的模板形式中，该方法就能将其找到。半代数不变量的计算直接决定了能否在连续演化与离散跳变耦合的复杂系统中，严格证明系统永远不会进入危险状态。

该工作从理论上回答了“如何系统性地判定与构造多项式动力系统安全区域”这一基础性问题，为后续非线性混成系统的形式化验证提供了严格的数学工具，它为安全攸关的嵌入式与混成系统（如自动驾驶、智能交通、医疗监护设备）的形式化验证奠定了关键理论基石，已被后续研究拓展至非多项式动力系统、非自治动力系统与兼具离散跃迁的混成系统，持续推动着我国在可信嵌入式软件与信息物理系统领域的基础研究保持引领性、原创性、前瞻性发展。