Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata

PELÁNEK, Radek, Kim G. LARSEN, Gerd BEHRMANN a Patricia BOUYER. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2006, roč. 8, č. 3, s. 204-215. ISSN 1433-2779.

Základní údaje

Originální název

Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata

Název česky

Využití horních a dolních mezí při zónových abstrakcích časových automatů

Autoři

PELÁNEK, Radek (203 Česká republika, garant), Kim G. LARSEN (208 Dánsko), Gerd BEHRMANN (208 Dánsko) a Patricia BOUYER (250 Francie)

Vydání

International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag GmbH, 2006, 1433-2779

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/06:00015564

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

model checking; timed automata; verification; abstraction; extrapolation

Štítky

Abstraction, extrapolation, Model checking, timed automata, verification

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to 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.

Česky

Časové automaty mají nekonečnou sémantiku. Pro účely verifikace se většinou používá abstrakce založená na zónách braných vzhledem k maximálním konstantám objevujícím se v časovém automatu. Ukazujeme, že rozlišením maximálních spodních a horním mezí lze dosáhnou významně hrubších abstrakcí. Dále předvádíme, jak může být informace o maximálních horních a dolních mezích využita pro kanonizaci matice rozdílů. Také experimentálně prokazujeme, že tato nová technika výrazně vylepší výkon nástroje UPPAAL.

---

Návaznosti

GA201/03/0509, projekt VaV	Název: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky