| 摘要: |
| 混成通信顺序进程(hybrid communicating sequential processes, HCSP)是一种广泛应用于混成系统建模的形式化语言. 它结合了由逻辑驱动的状态跳转(典型于数字计算)和由微分方程驱动的连续演化(用于刻画物理过程), 从而统一刻画了离散与连续行为. 这种双重特性使其特别适用于建模通常具有安全关键性的信息物理系统(cyber-physical system, CPS). 然而, 由于混成系统实现复杂、同步行为错综交织, 其验证在实际中面临显著挑战. 为此, 提出一种用于验证从抽象模型到具体实现之间精化关系的逻辑体系——混成精化逻辑(hybrid refinement logic, HRL). HRL通过按照系统的结构进行分解, 并基于精化构造分层的证明过程, 从而提升验证的可复用性和模块化程度. 此外, HRL还支持并行同步进程与顺序进程之间的精化验证, 进一步降低了证明复杂性, 能有效减轻验证负担. |
| 关键词: 混成系统 混成通信顺序进程 精化关系 形式化验证 定理证明 |
| DOI：10.13328/j.cnki.jos.007601 |
| 分类号:TP301 |
| 基金项目:中央高校基本科研业务费专项资金(2025ZFJH02); 浙江省重点研发计划(2025C01083) |
|
| Hybrid Refinement Logic |
|
SUN Huan, WANG Jing-Yi, WANG Wen-Hai
|
|
College of Control Science and Engineering, Zhejiang University, Hangzhou 310027, China
|
| Abstract: |
| Hybrid communicating sequential process (HCSP) is a formal modeling language widely used for hybrid systems. It integrates logic-driven state transitions, typical of digital computation, with continuous evolution governed by differential equations that capture physical dynamics. This dual nature makes HCSP particularly suitable for modeling safety-critical cyber-physical system (CPS). However, practical verification of hybrid systems remains challenging due to their complex implementations and intricate synchronization behaviors. This study introduces hybrid refinement logic (HRL), a formal logic framework for verifying the refinement relation between abstract models and concrete implementations. HRL promotes modular and reusable verification by structuring proofs hierarchically according to the structure of the system. To further reduce verification complexity, HRL also supports refinement reasoning between parallel synchronous processes and sequential processes, significantly alleviating the proof burden. |
| Key words: hybrid system (HS) hybrid communicating sequential process (HCSP) refinement relationship formal verification theorem proving |
