Hybrid Refinement Logic
Author:
Affiliation:

Clc Number:

TP301

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 03,2025
  • Revised:October 28,2025
  • Adopted:
  • Online: December 24,2025
  • Published: September 06,2026
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063