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

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

SP2020/62

Štolfa Svatopluk Ing., Ph.D.

01. 01. 2020 - 31. 12. 2020

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 a rozšiřuje výzkumné aktivity z předchozího roku. Formálními metodami myslíme zejména metody Transparentní intensionální logiky a její komputační varianty, což je jazyk TIL-Script. 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. 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šíř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. 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 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. Využití inferenčního stroje TIL-Script je pak využíváno a plánováno i pro aplikaci znalostního modelování v softwarovém inženýrství, získávání komputačních znalostí z textových korpusů a v teorii komputačních znalostí.

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. Svatopluk Štolfa, Ph.D.
Ing. Michal Fait, Ph.D.
Bc. Ing. Tomáš Krása
Ing. Adam Albert
Ing. Vojtěch Patschka
Bc. Ondřej Rusz
Bc. Lukáš Blahut
Bc. Tomáš Král
Ing. Martina Vápeníková
Ing. Lukáš Kotržena
Bc. Tomáš Dedek
Bc. Filip Hanslík
Bc. Filip Stolár
Ing. Tomáš Anlauf
Bc. Tomáš Jindra
Ing. Jiří Lagan
Bc. Jiří Fišer
Bc. Lukáš Ciahotný
Bc. Roman Černý
Ing. Lukáš Stankovič
Ing. Tomáš Kovačik
Bc. David Lukáš
Bc. František Šumšala
Bc. Ing. Jakub Holaza
Bc. Lukáš Hanusek
Bc. Mikuláš Mascautanu
Bc. Pavol Majchrák
Bc. David Bohunovský
Bc. Ing. Tomáš Mariňák
Bc. Adam Kořínek
Bc. Jan Bauer
Ing. Marek Spányik, MBA
Ing. Martin Sovják
Ing. Tatiana Oškrobaná
Ing. Jan Kollárik
Bc. Juraj Kubala
Ing. Martin Huber
Bc. Lukáš Zářecký
Bc. Dominika Halúsková

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 pro praktickou aplikaci formálních metod v oblasti vývoje software pro automotive
- Metodika znalostního modelování a nástroje pro aplikaci metodiky pro modelování, simulaci a verifikaci procesů, metriky
- Vzory pro vývoj elektronických a softwarových systémů v automotive
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 a zdokonalování inferenčního stroje pro TIL-Script
- Zpracování vstupních konstrukcí získaných analýzou textových korpusů
- Specifikace 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.
- 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ů podaných v rámci externích grantových agentur. Projektový tým se zúčastní mimo jiné i řešení projektu GAČR Hyperintensionální usuzování nad texty přirozeného jazyka, číslo GA18-23891S, který byl zahájen v lednu 2018.
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ší.