Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916140455821312 |
|---|---|
| author | Wang, Shuling Ji, Zekun Zhan, Bohua Xu, Xiong Gao, Qiang Zhan, Naijun |
| author_facet | Wang, Shuling Ji, Zekun Zhan, Bohua Xu, Xiong Gao, Qiang Zhan, Naijun |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_15674 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formally Verified C Code Generation from Hybrid Communicating Sequential Processes Wang, Shuling Ji, Zekun Zhan, Bohua Xu, Xiong Gao, Qiang Zhan, Naijun Programming Languages 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. |
| title | Formally Verified C Code Generation from Hybrid Communicating Sequential Processes |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2402.15674 |