球友会qy

中国科研实验室软件研究所天基综合信息系统全国重点实验室与法国国家信息与自动化研究所（INRIA）展开合作，首次提出了混成π-演算（Hybrid π-Calculus, HpC）。研究团队针对车联网、列控系统等动态环境中移动通信与混成行为耦合的难题，将图灵奖取得者Robin Milner等人提出的π-演算推广至混成系统领域。相关成果论文HpC: A Calculus for Hybrid and Systems被计算机科学和程序设计语言领域顶级学术会议OOPSLA 2025接收。共同第一作者为球友会qy助理研究员徐雄和INRIA高级研究员Jean-Pierre Talpin。

混成和移动系统作为一类复杂的信息物理融合系统，当前主要采用形式化方法，以严格的数学理论为基础，为计算系统进行形式规约、建模和验证，从而保障系统设计（尤其是安全攸关系统）的正确性和可靠性。然而，现有的形式化方法对于处理移动通信和混成行为的深度耦合问题，仍然面对较大挑战。

针对上述问题，研究团队提出了混成π-演算及其互模拟等相关理论，为移动计算环境下安全攸关信息物理融合系统的研究给予了理论基础。混成π-演算继承了π演算的“names are first-class citizens”原则，支持将通信通道作为消息在其他通道上传递（即高阶通信）。在此基础上，研究团队引入微分方程，描述物理环境的陆续在演化及其与离散进程的交互，实现了移动通信与混成行为的统一形式化表达。

混成π-演算语法

团队基于提出的混成π-演算，可以对移动通信和混成行为深度耦合的列控系统分区交接协议进行形式化建模。同时顺利获得建模，证明了理想模型与受物理扰动（如风力、轨道阻力）的模型之间存在近似互模 拟关系，验证了该列控系统分区交接协议的设计满足健壮性要求。

列控系统分区交接协议示意图

论文链接：http://doi.org/10.1145/3720478