HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914151677296640 |
|---|---|
| author | Jin, Xiangyu Zhan, Bohua Wang, Shuling Zhan, Naijun |
| author_facet | Jin, Xiangyu Zhan, Bohua Wang, Shuling Zhan, Naijun |
| contents | We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which is able to reason about continuous-time properties of differential equations, as well as communication and parallel composition of parallel HCSP processes with the help of parameterised trace assertions and their synchronization. The logic was formalised and proved to be sound in Isabelle/HOL, which constitutes a trustworthy foundation for the verification conducted by HHLPar. HHLPar implements the Hybrid Hoare Logic in Python and supports automated verification: On one hand, it provides functions for symbolically decomposing HCSP processes, generating specifications for separate sequential processes and then composing them via synchronization to obtain the final specification for the whole parallel HCSP processes; On the other hand, it is integrated with external solvers for handling differential equations and real arithmetic properties. We have conducted experiments on a simplified cruise control system to validate the performance of the tool. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_08936 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes Jin, Xiangyu Zhan, Bohua Wang, Shuling Zhan, Naijun Logic in Computer Science We present a tool called HHLPar for verifying hybrid systems modelled in Hybrid Communicating Sequential Processes (HCSP). HHLPar is built upon a Hybrid Hoare Logic for HCSP, which is able to reason about continuous-time properties of differential equations, as well as communication and parallel composition of parallel HCSP processes with the help of parameterised trace assertions and their synchronization. The logic was formalised and proved to be sound in Isabelle/HOL, which constitutes a trustworthy foundation for the verification conducted by HHLPar. HHLPar implements the Hybrid Hoare Logic in Python and supports automated verification: On one hand, it provides functions for symbolically decomposing HCSP processes, generating specifications for separate sequential processes and then composing them via synchronization to obtain the final specification for the whole parallel HCSP processes; On the other hand, it is integrated with external solvers for handling differential equations and real arithmetic properties. We have conducted experiments on a simplified cruise control system to validate the performance of the tool. |
| title | HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.08936 |