Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F09%3A00333922" target="_blank" >RIV/67985807:_____/09:00333922 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate

Popis výsledku v původním jazyce

We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a, trajectory to an unsafe state. The approach is to approximate how close a point is to being an initial point, of an error trajectory using a real-valued quality function, and then to use numerical optimisation to search for all optimum of this function. The function is computed by running simulations, where information coming from abstractions computed by a verification algorithm is exploited to determine whether a simulation looks promising and should be continued or cancelled. This information becomes more reliable as the abstraction becomes more refined. We thus interleave falsification and verification attempts.

Název v anglickém jazyce

Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate

Popis výsledku anglicky

We present an algorithm for falsifying safety properties of hybrid systems, i.e., for finding a, trajectory to an unsafe state. The approach is to approximate how close a point is to being an initial point, of an error trajectory using a real-valued quality function, and then to use numerical optimisation to search for all optimum of this function. The function is computed by running simulations, where information coming from abstractions computed by a verification algorithm is exploited to determine whether a simulation looks promising and should be continued or cancelled. This information becomes more reliable as the abstraction becomes more refined. We thus interleave falsification and verification attempts.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GC201%2F08%2FJ020" target="_blank" >GC201/08/J020: Verifikace hybridních systémů využitím spolupráce s řešením omezujících podmínek</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2009

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 statě ve sborníku

Tests and Proofs

ISBN

978-3-642-02948-6

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

—

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Zurich

Datum konání akce

2. 7. 2009

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000272046300012