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.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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
Změnil Změnil: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Změněno: 21. 11. 2006 14:01.
Anotace
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.
Anotace č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 VaVNázev: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Standardní projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 19. 2. 2020 07:59