Fakulta informačních technologií VUT v Brně

Tento projekt je spolufinancován se státní podporou Technologické gentury ČR v rámci Programu na podporu aplikovaného výzkumu a experimentálního vývoje EPSILON (2015-2025)
www.tacr.cz
Výzkum užitečný pro společnost.

Detail projektu

Automatizace Formální Verifikace (TACR)

Období řešení: 01.01.2019 - 31.12.2021

Kód: TH04010192

Agentura: Technologická agentura České republiky

Program: Program na podporu aplikovaného výzkumu a experimentálního vývoje EPSILON (2015-2025)

Název anglicky
AuFoVer - Automated Formal Verification
Typ
grant
Klíčová slova
formální verifikace; statická analýza; symbolická verifikace; dynamická analýza a testování; testování řízené modelem; automaty; specifikace požadavků; logiky;
Abstrakt
Hlavními cíli projektu je redukce vývojových nákladů kritických systémů nasazením automatizovaných formálních verifikačních nástrojů. Projekt se zaměřuje na (1) transparentní nasazení formálních metod (formální verifikace se během vývoje systémů použije takovým způsobem, který bude vyžadovat pouze minimální úpravu stávajících vývojových postupů), (2) automatickou sémantickou analýzu požadavků (požadavky napsané v přirozeném jazyce budou automaticky formalizovány a systémoví inženýři budou mít možnost získat informace o nekonzistentních, duplicitních, nerealizovatelných, nebo chybějící požadavcích) a (3) automatickou formální verifikaci systémů oproti požadavkům (vývojáři softwaru budou moci ověřit, jestli implementace v C/C++ splňuje dané požadavky bez nutnosti vytváření abstraktních modelů dané implementace). Tyto nové metody a nástroje se následně začlení do vlastního průmyslového vývoje a případné chyby se tak odhalí dříve ve vývojovém cyklu.
Řešitelé
Kratochvíla Tomáš (Honeywell) , hlavní řešitel
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Červinka Radim, Bc. (FIT VUT)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Holík Lukáš, Mgr., Ph.D. (UITS FIT VUT)
Hruška Martin, Ing. (UITS FIT VUT)
Kraut Daniel, Ing. (FIT VUT)
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Malík Viktor, Ing. (UITS FIT VUT)
Pešková Daniela (FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Sečkařová Petra, Ing. (FIT VUT)
Sušovský Tomáš, Ing. (FIT VUT)
Šoková Veronika, Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Nahoru