软件学报

作者：孙欢，王竟亦，王文海

单位：孙欢，浙江大学 控制科学与工程学院, 浙江 杭州 31005811,王竟亦，浙江大学 控制科学与工程学院, 浙江 杭州 31005802,王文海，浙江大学 控制科学与工程学院, 浙江 杭州 31005803

关键词：混成系统;混成通信顺序进程;精化关系;形式化验证;定理证明

基金：中央高校基本科研业务费专项资金资助(2025ZFJH02); 浙江省重点研发计划(2025C01083)

混成通信顺序进程(Hybrid Communicating Sequential Processes,简称HCSP)是一种广泛应用于混成系统建模的形式化语言.它结合了由逻辑驱动的状态跳转(典型于数字计算)和由微分方程驱动的连续演化(用于刻画物理过程),从而统一刻画了离散与连续行为.这种双重特性使其尤其适用于建模通常具有安全关键性的信息物理系统(Cyber-Physical Systems,简称CPSs).然而,由于混成系统实现复杂、同步行为错综交织,其验证在实际中面临显著挑战.为此,本文提出了一种用于验证从抽象模型到具体实现之间精化关系的逻辑体系——混成精化逻辑(Hybrid Refinement Logic,简称HRL).HRL通过按照系统的结构进行分解,并基于精化构造分层的证明过程,从而提升了验证的可复用性和模块化程度.此外,HRL还支持并行同步进程与顺序进程之间的精化验证,进一步降低了证明复杂性,有效减轻了验证负担.

来源：2026年第9期

《软件学报》期刊编辑部

查看软件学报杂志2026年第9期