Studentská grantová soutěž - předchozí roky

Aplikace formálních metod v oblastech modelování znalostí a softwarovém inženýrství IV

SP2021/87

Štolfa Svatopluk Ing., Ph.D.

01. 01. 2021 - 31. 12. 2021

Specifické cíle Mezi specifické cíle projektu patří: 1.) Výzkum a vývoj praktické aplikace formálních metod v softwarovém inženýrství, aplikace v automotive vývoji - Metody převzetí řízení autonomního vozu v režimu levelu 3-4 řidičem – postupy a dopady na vývoj systémů a software - Metody a nástroje pro vývoj a sledování kvality vývoje elektronických a softwarových systémů v automotive, metody a postupy aplikace funkční bezpečnosti a Cybersecurity - Metodika znalostního modelování a nástroje pro aplikaci metodiky pro modelování, simulaci a verifikaci procesů, metriky 2.) Aplikace formálních metod Transparentní Intensionální Logiky (TIL) a její komputační varianty TIL-Script v oblasti získávání znalostí z textových korpusů - Vývoj a zdokonalování inferenčního stroje pro TIL-Script - Zpracování vstupních konstrukcí získaných analýzou textových korpusů - Explikace atomických pojmů pomocí metod strojového učení - Logické zpracování získaných explikací a určování textových zdrojů vhodných pro daný dotaz - Implementace sekventového kalkulu jako extenzionální logiky hyperintensí - Výpočet množiny komputačních znalostí, které daný agent může odvodit z báze explicitních znalostí na základě své „inteligence“, tj. odvozovacích pravidel. - Aplikace těchto metod v multiagentním systému 3.) Analýza vlastností a korektnosti programů, zejména různé transformace reprezentací programů - Techniky implementace funkcionálních programovacích jazyků; využití poznatků z oblasti překladačů, sémantiky programovacích jazyků a teorie typů při implementaci jazyka TIL-Script - Transformace na kódech programů a dokazovaní jejich korektnosti - Verifikace programů a ověřování korektnosti programů, zejména pak ověřování korektnosti implementace různých datových struktur

Mgr. Marek Menšík, Ph.D.
Ing. Martin Kot, Ph.D.
prof. RNDr. Marie Duží, CSc.
doc. Ing. Zdeněk Sawa, Ph.D.
Ing. David Ježek, Ph.D.
Ing. Jan Kožusznik, Ph.D.
Ing. Jakub Štolfa, Ph.D.
Ing. Michal Fait, Ph.D.
Ing. Svatopluk Štolfa, Ph.D.
Bc. Ing. Tomáš Krása
Ing. Adam Albert
Bc. Filip Stolár
Ing. Jiří Lagan
Bc. Lukáš Ciahotný
Bc. Roman Černý
Ing. Lukáš Stankovič
Ing. Tomáš Kovačik
Bc. Ing. Jakub Holaza
Bc. Lukáš Hanusek
Bc. Ing. Tomáš Mariňák
Bc. Jan Bauer
Bc. Martin Gajdoš
Ing. Marek Spányik, MBA
Bc. Tomáš Jemelka
Bc. Jan Kollárik
Bc. Martin Pustka
Ing. Josef Micak
Ing. Adam Šárek
Ing. Jiří Besta
Ing. David Trebichalský
Ing. Marta Oškrobaná
Ing. Ivo Pešák
Bc. Petr West
Bc. Vojtěch Ferák
Bc. Adam Śmieja
Bc. Marek Janouch
Bc. Adam Kiovský
Bc. Juraj Kubala
Ing. Martin Huber
Bc. Dušan Janiš
Bc. Martin Šarlák

Cílem projektu je, jak již sám název napovídá, aplikace formálních metod v oblasti modelování znalostí a softwarového inženýrství. Projekt navazuje na výzkumné aktivity z předchozího roku a rozšiřuje je. Formálními metodami myslíme zejména metody Transparentní intensionální logiky a její komputační varianty, což je jazyk TIL-Script, a rovněž metody strojového učení, formální konceptuální analýzy apod. Aplikovali jsme a dále budeme aplikovat teorii typů a sémantiku funkcionálních programovacích jazyků při implementaci inferenčního stroje pro TIL-Script. Tyto metody aplikujeme na zpracování přirozeného jazyka, kde explikací atomických pojmů pomocí metod strojového učení získáváme další informace, které nám umožňují nejen zodpovídat na dotazy adekvátně, ale také slouží pro porovnání výsledků explikací, vyhledání vhodných textových zdrojů a případně i odhalování fake news. Budeme rovněž pokračovat v práci na analýze vlastností programů, zejména budeme zkoumat různé transformace reprezentací programů, tak, abychom ukázali jejich korektnost. V neposlední řadě pak budeme rozvíjet nástroje, podporující tyto metody.
V návaznosti na rozvoj formálních metod a přístupů se zaměřujeme také na další rozvoj a vývoj praktické aplikace znalostního modelování zejména v oblasti softwarového inženýrství. V minulých letech jsme se úspěšně zabývali rozvojem metod týkajících se odhadů budoucího chování procesu a sběru a přístupu k dolování dat o procesech, rozšiřovali jsme teoretické základy formálního modelování, jejichž využití bylo demonstrováno v oblasti softwarových procesů a v neposlední řadě jsme se zabývali také vývojem prototypových nástrojů umožňujících a demonstrujících efektivní transfer teoretických poznatků do praxe. Tyto směry bychom chtěli i dále podporovat a také dále rozšiřovat o nové oblasti aplikace týkající se zejména verifikace softwarového díla ve všech fázích jeho vývoje s ohledem na aplikaci v oblasti automotive, kde masivní nasazení software a elektroniky v posledních letech způsobuje obrovský tlak na kvalitu výsledného softwarového produktu a tedy i na správné postupy při tomto vývoji. Vyvíjíme metody a nástroje pro sledování kvality softwarového díla.
Nedílnou součástí projektu je pak také rozšiřování a formování našeho výzkumného týmu podporou studentů, kteří se podílejí a budou podílet na dalším výzkumu a vývoji a přispějí svými výsledky do publikačních výstupů.
Aplikační oblasti projektu jsou:
1. Výzkum a vývoj praktické aplikace formálních metod v softwarovém inženýrství, aplikace v automotive vývoji
2. Výzkum, vývoj a aplikace formálních metod TIL v oblasti získávání znalostí z textových korpusů
3. Aplikace metod teorie typů a sémantiky funkcionálních programovacích jazyků při analýze vlastností programů a důkazu jejich korektnosti
Tyto aplikační domény sdílejí společné teoretické základy z oblasti logiky a znalostního modelování, a tím napomáhají přímé implementaci teoretických výsledků do praxe. Teoretické výsledky budeme aplikovat v oblasti znalostního modelování v softwarovém inženýrství, pro získávání komputačních znalostí z textových korpusů, a vyhledávání vhodných textových zdrojů při zodpovídání dotazů.