混成精化逻辑
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP301

基金项目:

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


Hybrid Refinement Logic
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

孙欢,王竟亦,王文海.混成精化逻辑.软件学报,2026,37(9):1-13

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2025-09-03
  • 最后修改日期:2025-10-28
  • 录用日期:
  • 在线发布日期: 2025-12-24
  • 出版日期: 2026-09-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号