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

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

SP2023/065

Štolfa Svatopluk Ing., Ph.D.

01. 01. 2023 - 31. 12. 2023

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ů.

Ing. Svatopluk Štolfa, Ph.D.
Mgr. Marek Menšík, Ph.D.
Ing. Martin Kot, Ph.D.
doc. Ing. Zdeněk Sawa, Ph.D.
Ing. David Ježek, Ph.D.
Ing. Jan Kožusznik, Ph.D.
Ing. Jakub Štolfa, Ph.D.
prof. RNDr. Marie Duží, CSc.
Ing. Adam Albert
Ing. Marek Spányik, MBA
Ing. Ivo Pešák
Bc. David Lajtoch
Ing. Marta Oškrobaná
Bc. Vojtěch Ferák
Ing. Filip Peterek
Bc. Patrik Meixner
Ing. Šimon Slíva
Bc. Marek Bauer
Ing. Vítězslav Kaňok
Bc. Marek Svatoš
Ing. Patrik Szewczyk
Bc. Denis Lokaj
Bc. Miloš Kubáček
Bc. Michal Maier
Bc. Tomáš Janák
Bc. Jiří Hájíček
Bc. Jakub Lapihuska
Bc. Filip Klopec
Ing. Jakub Konvička
Bc. Martin Šmídl
Bc. Matěj Chmel
Ing. Jakub Osmančík
Bc. et Bc. Daniel Soukenka
Ing. Petr Kratochvíl
Ing. Filip Sedlařík
Bc. Matěj Tomšů
Ing. Viliam Majerčík
Ing. Jiří Besta

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 meta-teorie TIL, a to zejména z hlediska konzistence. Definice podsystémů TIL, které
jsou Henkinovsky úplné
- 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ý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, která má zabudována
- 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
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í – č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 a Scopus. Mezi časopisy, které bychom chtěli v budoucnu obeslat, budou patřit např.
tyto:
• Logic Journal of the IGPL, Oxford, ISSN 1367-0751
• Journal of Logic, Language and Information, Oxford, ISSN: 0925-8531
• Synthese, An International Journal for Epistemology, Methodology and Philosophy of Science, ISSN:
0039-7857 (Print) 1573-0964 (Online), Springer
• Organon F, Bratislava, ISSN 1335-0668
• International Journal of Uncertainty, Fuzziness & Knowledge-Based Systems (IJUFKS)
• Computación y Sistemas
• SAE Technical Papers
4
• Journal of Universal Computer Science
• Journal of Software: Evolution and process
Výběr konferencí, které chceme navštívit, se bude řídit těmito kritérii:
• Prestiž konference v oblasti znalostních přístupů a modelování softwarových procesů (snaha navázat další
kontakty s lidmi, kteří v této oblasti působí a mají špičkové výsledky),
• Finanční náročnost účasti na konferenci (snaha nečerpat zbytečně velké množství prostředků na
konference, které mají „levnější“ obdobu v jiných minimálně stejně kvalitních konferencích).
Konference vybereme na základě aktuálního harmonogramu na příští rok.