Ústav inteligentních systémů



AUFOVER - Automatizace Formální Verifikace (TACR)

Název v angličtině:AuFoVer - Automated Formal Verification
Hlavní řešitel:Kratochvíla Tomáš (Honeywell)
Spoluřešitelé:Smrčka Aleš
Další řešitelé:Vojnar Tomáš
Agentura:Technologická agentura České republiky - Program na podporu aplikovaného výzkumu a experimentálního vývoje EPSILON (2015-2025)
Kód:TH04010192
Zahájení:2019-01-01
Ukončení:2021-12-31
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;
Anotace:
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.

Vaše IPv4 adresa: 34.239.162.61