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