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

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

Kód
SP2022/123

Řešitel
Štolfa Svatopluk Ing., Ph.D.

Období řešení projektu
1. 1. 2022 - 31. 12. 2022

Předmět výzkumu
Předmět výzkumu v rámci projektu 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ích let 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. Navíc se budeme věnovat logicko-lingvistické analýze dynamického chování agentů, ať už softwarových nebo lidských s cílem zodpovídat nejen „Yes-No“ dotazy, ale rovněž „Wh-questions“ týkající se procesů a jejich aktérů. 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. Speciální důraz bude v tomto roce kladen na vývoj metody pro formalizaci a analýzu požadavků na software, a to za využití naším týmem vyvíjených formálních metod. Cílem je získání přehledu o úplnosti požadavků, dosažení možnosti kvalitnějšího provázání požadavků s dalšími fázemi vývoje software a následné možností automatického vytváření testovacích případů pro validaci a verifikaci. 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 3 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ů.

Členové řešitelského týmu
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. Zdeněk Velart, Ph.D.
Ing. Svatopluk Štolfa, Ph.D.
Ing. Michal Fait, Ph.D.
Ing. Adam Albert, Ph.D.
Bc. Tomáš Jindra
Bc. Petr Vychodil
Bc. Michal Maier
Bc. David Lukáš
Bc. Adam Zahatlan
Bc. Martin Gajdoš
Ing. Marek Spányik, MBA
Ing. Dušan Hlaváč
Ing. Martin Sovják
Ing. Tatiana Oškrobaná
Ing. Patrik Szewczyk
Bc. Tomáš Jemelka
Ing. Martin Kurfürst
Ing. Jan Kollárik
Ing. Šimon Slíva
Ing. Frederik Zajac
Bc. Marek Bauer
Bc. Tomáš Janák
Bc. Marek Šutý
Bc. Dominik Vašíček
Bc. Martin Pustka
Ing. Štěpán Chvatík
Ing. Jiří Besta
Ing. David Trebichalský
Bc. Petr West
Bc. Vojtěch Ferák
Bc. David Lajtoch
Bc. Marek Janouch
Ing. Dušan Janiš
Bc. Martin Šarlák
Ing. Vítězslav Kaňok
Bc. Daniel Merta
Ing. Ivo Pešák
Ing. Marta Oškrobaná
Bc. Martin Šmídl
Ing. Jakub Konvička
Bc. Miloš Kubáček

Specifikace výstupů projektu (cíl projektu)
Specifické cíle<br />Mezi specifické cíle projektu patří:<br />1.) Výzkum a vývoj praktické aplikace formálních metod v softwarovém inženýrství, aplikace<br />v automotive vývoji<br />- Metody převzetí řízení autonomního vozu v režimu levelu 3-4 řidičem – postupy a dopady na<br />vývoj systémů a software<br />- Metody a nástroje pro vývoj a sledování kvality vývoje elektronických a softwarových<br />systémů v automotive, metody a postupy aplikace funkční bezpečnosti a Cybersecurity<br />- Metodika znalostního modelování a nástroje pro aplikaci metodiky pro modelování, simulaci a<br />verifikaci procesů, metriky<br />2.) Aplikace formálních metod Transparentní Intensionální Logiky (TIL) a její komputační varianty<br />TIL-Script v oblasti získávání znalostí z textových korpusů<br />- Vývoj meta-teorie TIL, a to zejména z hlediska konzistence. Definice podsystémů TIL, které<br />jsou Henkinovsky úplné<br />- Zdokonalení logické formalizace vstupních textových sentencí získaných lingvistickou<br />analýzou textových korpusů<br />- Explikace atomických pojmů pomocí metod strojového učení<br />- Logické zpracování získaných explikací a určování textových zdrojů vhodných pro daný dotaz<br />- Implementace sekventového kalkulu jako extenzionální logiky hyperintensí<br />- Výpočet množiny komputačních znalostí, které daný agent může odvodit z báze explicitních<br />znalostí na základě své „inteligence“, tj. odvozovacích pravidel, která má zabudována<br />- Aplikace těchto metod v multiagentním systému<br />3.) Analýza vlastností a korektnosti programů, zejména různé transformace reprezentací programů<br />- Techniky implementace funkcionálních programovacích jazyků; využití poznatků z oblasti<br />překladačů, sémantiky programovacích jazyků a teorie typů při implementaci jazyka TIL-Script<br />- Transformace na kódech programů a dokazovaní jejich korektnosti<br />- Verifikace programů a ověřování korektnosti programů, zejména pak ověřování korektnosti<br />implementace různých datových struktur<br />Kromě definovaných cílů, tj. realizace zmíněných aktivit, budou dalším výsledkem tohoto grantu podklady pro<br />přípravu projektů a jejich podávání v rámci externích grantových agentur.<br />V průběhu řešení předpokládáme standardní publikační a jiné výstupy, které budou měřitelné v rámci<br />definovaných metodologií – články v impaktovaných časopisech, konference, metodiky a postupy, disertace a<br />diplomové práce k danému tématu a další. Během tohoto projektu hodlají řešitelé připravit nové a dopracovat<br />rozpracované či podané články do vybraných časopisů, které mají přidělen impaktní faktor a jsou vedeny<br />v databázi společnosti WoS a Scopus. Mezi časopisy, které bychom chtěli v budoucnu obeslat, budou patřit např.<br />tyto:<br />• Logic Journal of the IGPL, Oxford, ISSN 1367-0751<br />• Journal of Logic, Language and Information, Oxford, ISSN: 0925-8531<br />• Synthese, An International Journal for Epistemology, Methodology and Philosophy of Science, ISSN:<br />0039-7857 (Print) 1573-0964 (Online), Springer<br />• Organon F, Bratislava, ISSN 1335-0668<br />• International Journal of Uncertainty, Fuzziness & Knowledge-Based Systems (IJUFKS)<br />• Computación y Sistemas<br />• SAE Technical Papers<br />4<br />• Journal of Universal Computer Science<br />• Journal of Software: Evolution and process<br />Výběr konferencí, které chceme navštívit, se bude řídit těmito kritérii:<br />• Prestiž konference v oblasti znalostních přístupů a modelování softwarových procesů (snaha navázat další<br />kontakty s lidmi, kteří v této oblasti působí a mají špičkové výsledky),<br />• Finanční náročnost účasti na konferenci (snaha nečerpat zbytečně velké množství prostředků na<br />konference, které mají „levnější“ obdobu v jiných minimálně stejně kvalitních konferencích).<br />Konference vybereme na základě aktuálního harmonogramu na příští rok.