Zaručená terminace ve verifikaci nelineárních robustních hybridních systémů v diskrétním čase

Kód výsledku v IS VaVaI

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

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Guaranteed Termination in the Verification of LTL Properties of Non-Linear Robust Discrete Time Hybrid Systems

Popis výsledku v původním jazyce

We present a novel approach to the automatic verification and falsification of LTL requirements of non-linear discrete-time hybrid systems. The verification tool uses an interval-based constraint solver for non-linear robust constraints to compute incrementally refined abstractions. Although the problem is in general undecidable, we prove termination of abstraction refinement based verification and falsification of such properties for the class of non-linear robust discrete-time hybrid systems. We argue, that?in industrial practice?safety critical control applications give rise to hybrid systems that are robust. We give first results on the application of this approach to a variant of an aircraft collision avoidance protocol

Název v anglickém jazyce

Guaranteed Termination in the Verification of LTL Properties of Non-Linear Robust Discrete Time Hybrid Systems

Popis výsledku anglicky

We present a novel approach to the automatic verification and falsification of LTL requirements of non-linear discrete-time hybrid systems. The verification tool uses an interval-based constraint solver for non-linear robust constraints to compute incrementally refined abstractions. Although the problem is in general undecidable, we prove termination of abstraction refinement based verification and falsification of such properties for the class of non-linear robust discrete-time hybrid systems. We argue, that?in industrial practice?safety critical control applications give rise to hybrid systems that are robust. We give first results on the application of this approach to a variant of an aircraft collision avoidance protocol

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

International Journal of Foundations of Computer Science

ISSN

0129-0541

e-ISSN

—

Svazek periodika

18

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

SG - Singapurská republika

Počet stran výsledku

24

Strana od-do

63-86

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—