Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail projektu
Období řešení: 01.01.2019 — 31.12.2021
Zdroje financování
Technologická agentura ČR - Program na podporu aplikovaného výzkumu a experimentálního vývoje EPSILON (2015-2025)
- plně financující (2019-01-01 - 2021-12-31)
O projektu
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.
Popis anglickyThe main scope of the project is on reducing cost of development of critical systems by leveraging tools for automated formal verification. In particular, the project concentrates on (1) transparent deployment of formal methods (formal verification will be used in a way requiring minimal modification of current processes), (2) automated semantic analysis of requirements (requirements written in natual language wil be automatically formalised and system engineers will be able to gain information about inconsistent, duplicate, unrealisable, or missing requirements), and (3) automated formal verification of system wrt. requirements (the developers will be able to verify if an implementation in C/C++ satisfies a given requirements with no need to create abstract models of a verified system). The new developed methods and tools will be included in industrial practice to allow revealing bugs sooner in development cycle.
Klíčová slovaformální verifikace; statická analýza; symbolická verifikace; dynamická analýza a testování; testování řízené modelem; automaty; specifikace požadavků; logiky;
Klíčová slova anglickyformal verification; static analysis; symbolic verification; dynamic analysis and testing; model-based testing; automata; requirement specification; logics;
Označení
TH04010192
Originální jazyk
čeština
Řešitelé
Kratochvíla Tomáš, Mgr. - hlavní řešitelVojnar Tomáš, prof. Ing., Ph.D. - spoluřešitel
Útvary
Ústav inteligentních systémů- spolupříjemce (27.03.2018 - 31.12.2021)Masarykova Univerzita v Brně- spolupříjemce (27.03.2018 - 31.12.2021)Red Hat Czech s.r.o.- spolupříjemce (27.03.2018 - 31.12.2021)Honeywell International s.r.o.- příjemce (27.03.2018 - 31.12.2021)
Výsledky
SMRČKA, A.; VAŠÍČEK, O.; FIEDOR, J.; VOJNAR, T.: Testos-Aufover; Testos-Aufover - Verification as a Service. https://pajda.fit.vutbr.cz/testos/testos-aufover/-/tree/v1.0. URL: https://pajda.fit.vutbr.cz/testos/testos-aufover/-/tree/v1.0. (software)Detail