Studentská grantová soutěž

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

SP2025/091

Štolfa Svatopluk Ing., Ph.D.

01. 01. 2025 - 31. 12. 2025

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. Tato implementace je prováděna překladem do jazyka Haskell. Systém TILje aplikován především 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. Věnujeme se rovněž 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 zejména pomocí AGILE metod, 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ů, což je v současnosti velký problém zejména v souvislosti nutnosti zavedení AGILNÍHO vývoje systémů v souvislosti s velkým důrazem na kvalitu vývoje definovanou zejména pro V-model způsobu vývoje (oblasti ASPICE, FS, Cybersecurity, AI, ...). Konkrétními výstupy jsou a budou např. rozvoj metodiky kontroly kvality agilně řízeného procesu vývoje, SW pro polo- či automatizovanou kontrolu kvality, 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ší. 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 za předpokladu publikační činnosti, vývoje licencovatelného SW a příp. patentů. 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. Adam Albert
Ing. Tomáš Stehlík
Ing. Marek Spányik, MBA
Bc. David Husička
Bc. Daniel Makovský
Bc. Jan Fojtík
Bc. Matěj Krzystek
Bc. Jan Kopidol
Bc. Jakub Koběrský
Bc. Dominik Kundra
Bc. Martin Korotwitschka
Bc. Jan Karkoška
Bc. Filip Hanslík
Bc. Filip Klopec
Bc. Dominik Komosný
Bc. Nicola Műhr
Bc. Radovan Kavka
Bc. Jakub Kupka
Bc. Matěj Tomšů
Bc. Omar Saleh
Bc. Andrzej Malysz
Bc. Marie Lašinská

Specifické cíle
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ů
- Verifikace transformací SQL dotazů.
- 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