IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název periodika

Journal of Automated Reasoning

ISSN

0168-7433

e-ISSN

1573-0670

Svazek periodika

68

Číslo periodika v rámci svazku

4

Stát vydavatele periodika

CZ - Česká republika

Počet stran výsledku

50

Strana od-do

—

Kód UT WoS článku

001336815600001

EID výsledku v databázi Scopus

2-s2.0-85207058486