Studentská grantová soutěž

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

SP2024/108

Štolfa Svatopluk Ing., Ph.D.

01. 01. 2024 - 31. 12. 2024

Cílem projektu je 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, automatizované dokazování v systému Coq 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 tomto projektu bychom chtěli pokračovat zejména ve výzkumu a vývoji postupů a nutných znalostí a dovedností vývoje elektroniky a software v Automotive oblasti, kdy navazujeme na trendy v automotive (m.j. identifikované naším článkem „A literature review of drivers of change in automotive industry, Journal of Software: Evolution and Process). Rozpracováváme inovativní postupy vývoje systémů pro tyto vyšší stupně automatizace zahrnující integraci nejnovějších postupů zaměřených na nové architektury automobilu jako celku a inovativní praktické aplikace vyžadovaných standardů (např. z oblastí ASPICE, FS, Cybersecurity, ...) konkrétními výstupy jsou např. aplikace námi vyvíjených aplikačních SW vzorů v Cybersecurity; metody automatizované AI specifikace požadavků a provázání s designem, kódem a testy; metody určení kompletnosti trénovací množiny pro AI a další. Pokračujeme na výzkumu oblasti metrik pro měření procesů a produktu, hodnocení procesů, formální verifikace testování, a to vše za podpory našich vyvinutých a dále vyvíjených nástrojů vycházejících z teoretických poznatků našeho týmu. 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 v softwarovém inženýrství, zejména v automotive dovednostech a 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ů, zodpovídání dotazů nad textovými korpusy 3. Analýza vlastností algoritmů, dokazování korektnosti programů 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ů.

Ing. Svatopluk Štolfa, Ph.D.
prof. RNDr. Marie Duží, CSc.
doc. Ing. Zdeněk Sawa, Ph.D.
Ing. Jakub Štolfa, Ph.D.
Ing. Martin Kot, Ph.D.
Mgr. Marek Menšík, Ph.D.
Ing. David Ježek, Ph.D.
Ing. Jan Kožusznik, Ph.D.
Ing. Michal Fait, Ph.D.
Ing. Adam Albert
Ing. Marek Spányik, MBA
Ing. Jakub Konvička
Bc. Adam Krček
Ing. Vojtěch Grycz
Bc. Matěj Tomšů
Ing. Viliam Majerčík
Bc. Filip Hanslík
Bc. Michal Chylík
Bc. Stanislav Baričák
Bc. et Bc. Daniel Soukenka
Ing. Jakub Osmančík
Ing. Filip Sedlařík
Ing. Petr Kratochvíl
Bc. Lukáš Bukovčan
Bc. Daniel Buroň
Bc. Vojtěch Janásek
Bc. Andrzej Malysz
Bc. Daniel Závodský
Bc. Radovan Kavka
Bc. Nicola Műhr
Bc. Erik Hawlasek
Bc. Dominik Komosný
Bc. Jakub Minařík
Bc. Martin Hýl
Bc. Matěj Chmel

Mezi specifické cíle projektu patří:
1.) Výzkum a vývoj využití v softwarovém inženýrství, zejména v Automotive dovednostech a vývoji
- 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ů, V model vs SCRUM, metriky
- Znalosti a dovednosti v Automotive sektoru a jejich integrace
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 meta-teorie TIL, a to zejména z hlediska konzistence. Definice podsystémů TIL, které jsou Henkinovsky úplné včetně důkazu této úplnosti
- Zdokonalení logické formalizace vstupních textových sentencí získaných lingvistickou 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ývoj systému zodpovídání dotazů nad textovými korpusy
- Aplikace těchto metod v multiagentním systému, modelování dynamiky systému
3.) Formální model Transparentní Intensionální Logiky (TIL), dokazování korektnosti programů
- 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 komplikovaných datových struktur a grafových algoritmů
- Implementace formálního modelu Transparentní Intensionální Logiky (TIL) v systému Coq, implementace dedukčního systému založeného na přirozené dedukci v TIL v rámci tohoto formálního modelu
Kromě definovaných cílů, tj. realizace zmíněných aktivit, budou dalším výsledkem tohoto grantu podklady pro přípravu projektů a jejich podávání v rámci externích grantových agentur.
V průběhu řešení předpokládáme standardní publikační a jiné výstupy, které budou měřitelné v rámci definovaných metodologií, tj. články v impaktovaných časopisech, konference, metodiky a postupy, disertace a diplomové práce k danému tématu a další. Během tohoto projektu hodlají řešitelé připravit nové a dopracovat rozpracované či podané články do vybraných časopisů, které mají přidělen impaktní faktor a jsou vedeny v databázi společnosti WoS nebo Scopus.