Přeskočit na hlavní obsah
Přeskočit hlavičku
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
Období řešení projektu
01. 01. 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
Ing. Adam Albert
Bc. Marek Bauer
Bc. Jiří Besta
Ing. Štěpán Chvatík
prof. RNDr. Marie Duží, CSc.
Ing. Michal Fait
Bc. Vojtěch Ferák
Bc. Martin Gajdoš
Bc. Dušan Hlaváč
Ing. Lukáš Imrišík
Bc. Tomáš Janák
Bc. Dušan Janiš
Bc. Marek Janouch
Bc. Tomáš Jemelka
Ing. David Ježek, Ph.D.
Bc. Tomáš Jindra
Bc. Vítězslav Kaňok
Bc. Jan Kollárik
Ing. Martin Kot, Ph.D.
Ing. Jan Kožusznik, Ph.D.
Bc. Martin Kurfürst
Bc. David Lajtoch
Bc. David Lukáš
Bc. Michal Maier
Mgr. Marek Menšík, Ph.D.
Bc. Daniel Merta
Bc. Tatiana Oškrobaná
Bc. Martin Pustka
Bc. Martin Šarlák
doc. Ing. Zdeněk Sawa, Ph.D.
Ing. Marcel Ševec
Bc. Šimon Slíva
Bc. Martin Sovják
Ing. Marek Spányik
Ing. Svatopluk Štolfa, Ph.D.
Ing. Jakub Štolfa, Ph.D.
Bc. Marek Šutý
Bc. Patrik Szewczyk
Bc. David Trebichalský
Bc. Dominik Vašíček
Bc. Petr Vychodil
Bc. Petr West
Bc. Adam Zahatlan
Bc. Frederik Zajac
Specifikace výstupů projektu (cíl projektu)
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.

Rozpočet projektu - uznané náklady

Návrh Skutečnost
1. Osobní náklady
Z toho
0,- 0,-
1.1. Mzdy (včetně pohyblivých složek) 0,- 0,-
1.2. Odvody pojistného na veřejné zdravotně pojištění a pojistného na sociální zabezpečení a příspěvku na státní politiku zaměstnanosti 0,- 0,-
2. Stipendia 233450,- 233450,-
3. Materiálové náklady 0,- 0,-
4. Drobný hmotný a nehmotný majetek 356958,- 356958,-
5. Služby 150000,- 150000,-
6. Cestovní náhrady 310000,- 310000,-
7. Doplňkové (režijní) náklady max. do výše 10% poskytnuté podpory 116712,- 116712,-
8. Konference pořádané VŠB-TUO k prezentaci výsledků studentského grantu (max. do výše 10% poskytnuté podpory) 0,- 0,-
9. Pořízení investic 0,- 0,-
Plánované náklady 1167120,-
Uznané náklady 1167120,-
Celkem běžné finanční prostředky 1167120,- 1167120,-
Zpět na seznam