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 | |
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 | |
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: |