Výzkum užitečný pro společnost.
Detail projektu
Automatizace formální verifikace
Období řešení: 1. 1. 2019 – 31. 12. 2021
Typ projektu: grant
Kód: TH04010192
Agentura: Technologická agentura ČR
Program: Program na podporu aplikovaného výzkumu a experimentálního vývoje EPSILON (2015-2025)
formální verifikace; statická analýza; symbolická verifikace; dynamická analýza
a testování; testování řízené modelem; automaty; specifikace požadavků; logiky;
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.
Smrčka Aleš, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
2021
- Testos-Aufover - Verifikace jako služba, software, 2021
Autoři: SMRČKA, A.; VAŠÍČEK, O.; FIEDOR, J.; VOJNAR, T.