Verifikace bezpečnosti hybridních systémů používající upřesňování abstrakcí a propagaci podmínek

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F07%3A00084109" target="_blank" >RIV/67985807:_____/07:00084109 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Safety Verification of Hybrid Systems by Constraint Propagation-based Abstraction Refinement

Popis výsledku v původním jazyce

This paper deals with the problem of safety verification of nonlinear hybrid systems.We start from a classical method that uses interval arithmetic to check whether trajectories can move over the boundaries in a rectangular grid. We put this method intoan abstraction refinement framework and improve it by developing an additional refinement step that employs interval-constraint propagation to add information to the abstraction without introducing new grid elements. Moreover, the resulting method allowsswitching conditions, initial states, and unsafe states to be described by complex constraints, instead of sets that correspond to grid elements. Nevertheless, the method can be easily implemented, since it is based on a well-defined set of constraints,on which one can run any constraint propagation-based solver. Tests of such an implementation are promising.

Název v anglickém jazyce

Safety Verification of Hybrid Systems by Constraint Propagation-based Abstraction Refinement

Popis výsledku anglicky

This paper deals with the problem of safety verification of nonlinear hybrid systems.We start from a classical method that uses interval arithmetic to check whether trajectories can move over the boundaries in a rectangular grid. We put this method intoan abstraction refinement framework and improve it by developing an additional refinement step that employs interval-constraint propagation to add information to the abstraction without introducing new grid elements. Moreover, the resulting method allowsswitching conditions, initial states, and unsafe states to be described by complex constraints, instead of sets that correspond to grid elements. Nevertheless, the method can be easily implemented, since it is based on a well-defined set of constraints,on which one can run any constraint propagation-based solver. Tests of such an implementation are promising.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2007

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

ACM Transactions on Embedded Computing Systems

ISSN

1539-9087

e-ISSN

—

Svazek periodika

6

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

23

Strana od-do

—

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—