Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要