Horní a dolní meze při analýze časových automatů s použitím zónové abstrakce

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F04%3A00010716" target="_blank" >RIV/00216224:14330/04:00010716 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Popis výsledku v původním jazyce

Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions wrt. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds we can obtain significantly coarser abstractions. We show the soundness and completeness of the new abstractstions wrt. reachability and we experimentaly demonstrate their advantages. We demonstrate how information about lower and upper boudns can be usedto optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker UPPAAL.

Název v anglickém jazyce

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

Popis výsledku anglicky

Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions wrt. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds we can obtain significantly coarser abstractions. We show the soundness and completeness of the new abstractstions wrt. reachability and we experimentaly demonstrate their advantages. We demonstrate how information about lower and upper boudns can be usedto optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker UPPAAL.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automatizovaná verifikace paralelních a distribuovaných systémů</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2004

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

Tools and Algorithms for Construction and Analysis of Systems (TACAS 2004)

ISBN

3-540-21299-X

ISSN

—

e-ISSN

—

Počet stran výsledku

15

Strana od-do

312-326

Název nakladatele

Springer-Verlag

Místo vydání

Barcelona (Španělsko)

Místo konání akce

Barcelona

Datum konání akce

1. 1. 2004

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

WRD - Celosvětová akce

Kód UT WoS článku

—