IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00382701" target="_blank" >RIV/68407700:21730/24:00382701 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1007/s10817-024-09709-2" target="_blank" >https://doi.org/10.1007/s10817-024-09709-2</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10817-024-09709-2" target="_blank" >10.1007/s10817-024-09709-2</a>

Result language

angličtina

Original language name

IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale

Original language description

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), an open, compositional and extensible framework for the verification of cyber-physical systems. We extend a previous semantic approach with methods and techniques that increase its expressivity, proof automation, and scalability to the level of state-of-the-art deductive verification tools. Our contributions include a user-friendly specification language, a flexible hybrid store model, including vectors and matrices, and separation-logic-style rules for local reasoning with hybrid stores using a novel form of differentiation called framed Fréchet derivatives. The formalisation of correctness specifications with forward predicate transformers, the certification of flows as unique solutions to systems of ordinary differential equations, and invariant reasoning for such systems also contribute to the scalability and usability of our framework. In combination, these features make our framework flexible and adaptable to several verification workflows. A suite of examples and hybrid systems verification benchmarks validate our framework relative to other state-of-the-art approaches.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

R - Projekt Ramcoveho programu EK

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Journal of Automated Reasoning

ISSN

0168-7433

e-ISSN

1573-0670

Volume of the periodical

68

Issue of the periodical within the volume

4

Country of publishing house

CZ - CZECH REPUBLIC

Number of pages

50

Pages from-to

—

UT code for WoS article

001336815600001

EID of the result in the Scopus database

2-s2.0-85207058486