Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909079334551552 |
|---|---|
| author | Munive, Jonathan Julián Huerta y Foster, Simon Gleirscher, Mario Struth, Georg Laursen, Christian Pardillo Hickman, Thomas |
| author_facet | Munive, Jonathan Julián Huerta y Foster, Simon Gleirscher, Mario Struth, Georg Laursen, Christian Pardillo Hickman, Thomas |
| contents | We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the Isabelle/HOL proof assistant. A user-friendly language specification based on a robust state model makes our framework flexible and adaptable to various engineering workflows. New additions to the framework increase both its expressivity and proof automation. Specifically, formalisations related to forward diamond correctness specifications, certification of unique solutions to ordinary differential equations (ODEs) as flows, and invariant reasoning for systems of ODEs contribute to the framework's scalability and usability. Various examples and an evaluation validate the effectiveness of our framework. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_12061 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL Munive, Jonathan Julián Huerta y Foster, Simon Gleirscher, Mario Struth, Georg Laursen, Christian Pardillo Hickman, Thomas Logic in Computer Science Mathematical Software We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the Isabelle/HOL proof assistant. A user-friendly language specification based on a robust state model makes our framework flexible and adaptable to various engineering workflows. New additions to the framework increase both its expressivity and proof automation. Specifically, formalisations related to forward diamond correctness specifications, certification of unique solutions to ordinary differential equations (ODEs) as flows, and invariant reasoning for systems of ODEs contribute to the framework's scalability and usability. Various examples and an evaluation validate the effectiveness of our framework. |
| title | Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL |
| topic | Logic in Computer Science Mathematical Software |
| url | https://arxiv.org/abs/2401.12061 |