Detail projektu

Pokročilé metody automatické verifikace parametrických a nekonečně stavových systémů

Období řešení: 1. 9. 2003 - 1. 9. 2006

Typ projektu: grant

Kód: GP102/03/D211

Agentura: Grantová agentura České republiky

Program:

Název anglicky
Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems
Typ
grant
Klíčová slova

formální verifikace, model checking, parametrizované a nekonečně stavové systémy, paralelní systémy

Abstrakt

Neustálý růst složitosti počítačových systémů spolu s růstem nároků na jejich spolehlivost jsou příčinou, proč je v současnosti věnována značná pozornost vývoji automatizovaných metod a nástrojů pro rigorózní verifikaci jejich korektnosti. Mezi systémy, jimž je věnována zvláštní pozornost, patří protokoly počítačových a telekomunikačních sítí, paralelní software řídicích a operačních systémů, hardwarové komunikační protokoly apod. Zatímco pro případ, že uvažované systémy mají konečný stavový prostor, již byla vyvinuta řada poměrně efektivních verifikačních metod, automatická verifikace nekonečně stavových a parametrických systémů je mnohem méně rozpracovaná. Řada typů těchto systémů významných pro praxi není pokryta žádnými verifikačními metodami, případně metody, které jsou dostupné, nejsou příliš efektivní. Na základě zkušeností navrhovatele se současnými možnostmi a omezeními těchto metod předkládaný projekt usiluje o jejich rozvoj směrem k vyšší efektivitě a širší aplikovatelnosti. Důraz bude přitom kladen zejména na metody symbolické verifikace využívající automaty a převodníky pro práci s množinami stavů. Budou zkoumány možnosti použití nových typů automatů a také nové techniky pro efektivní manipulaci stávajících i nově uvažovaných typů automatů. Kromě zmíněných metod symbolické verifikace budou rozvíjeny rovněž metody řezů a automatizované abstrakce. Cílem projektu je přitom nejen teoretický výzkum, ale také prototypová implementace alespoň těch nejslibnějších z navržených metod.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT) , spoluřešitel
Publikace

2013

2007

2006

2005

2004

2003

Nahoru