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.