Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
Shuling Wang, Zekun Ji, Bohua Zhan, Xiong Xu, Qiang Gao, Naijun Zhan
TL;DR
The paper targets formally verified code generation from HCSP, a formalism for hybrid systems that combines continuous evolution and synchronized communications. It introduces a rigorous C code target using POSIX threads, supported by a formal semantics for POSIX-C and a two-step proof: HCSP is approximately bisimilar to its discretization, and the discretized HCSP is exactly bisimilar to the generated C code, under robust safety assumptions. The approach discretizes ODEs with a 4-stage Runge–Kutta method, defines a novel approximate bisimulation relation that accommodates interleaving concurrency, and demonstrates the method on an Automatic Cruise Control system, showing high fidelity to the HCSP model while providing formal correctness guarantees. The work advances practice by enabling verifiable, efficient, and scalable code generation for safety-critical CPS, with potential for broader industry application.
Abstract
Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communication, and parallel composition. Code generation is needed to convert HCSP models into code that can be executed in practice, and the correctness of this conversion is essential to ensure that the generated code accurately reflects the formal model. In this paper, we propose a code generation algorithm from HCSP to C with POSIX library for concurrency. The main difficulties include how to bridge the gap between the synchronized communication model in HCSP and the use of mutexes for synchronization in C, and how to discretize evolution along ODEs and support interrupt of ODE evolution by communication. To prove the correctness of code generation, we define a formal semantics for POSIX C, and build transition system models for both HCSP and C programs. We then define an approximate bisimulation relation between traces of transition systems, and show that under certain robustness conditions for HCSP, the generated C program is approximately bisimilar to the original model. Finally, we evaluate the code generation algorithm on a detailed model for automatic cruise control, showing its utility on real-world examples.