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

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
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 LARSEN Kim G. BEHRMANN Gerd BOUYER Patricia

Rok publikování 2006
Druh Článek v odborném periodiku
Časopis / Zdroj International Journal on Software Tools for Technology Transfer (STTT)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova model checking; timed automata; verification; abstraction; extrapolation
Popis Č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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.