Formální verifikace a analýza

Správnost a spolehlivost jsou fundamentální požadaky, které na současné komplexní počítačové systémy klademe. Výzkum a vývoj metod a technik, které by eliminovaly či alespoň významně snížili počet závažných chyb v těchto systémech, je jedním z centrálních témat současné informatiky. Plně automatizované metody pro formální verifikaci a analýzu jsou však výpočetně velmi náročné a bez využití dodatečných technik je není možné aplikovat na realné průmyslové systémy.

Náš tým se zabývá výzkumem nových metod a technik pro automatizovanou formální verifikaci a analýzu, které staví na efektivním využití moderních počítačových architektur. Primárně se zaměřujeme na možnosti, které nabízejí vícejádrové architektury, rozsáhlé sítě vzájemně propojených pracovních stanic a externí disková pole. Naším cílem je vývoj takových postupů a nástrojů, které by vedly k plně počítačem podporované verifikaci a analýze velmi velkých systémů.


Hlavní výzkumné priority

  • Paralelní verifikace a analýza. Cílem v této oblasti je návrh nových paralelních a distribuovaných algoritmů a jejich experimentální vyhodnocení. Soustředíme se zejména na paralelizaci velice efektivní verifikační metody ověřování modelu (model-checking) temporálních vlastností pro konečně stavové systémy a kvalitativní i kvantitativní ověřování modelu temporálních vlastností pro Markovovy rozhodovací procesy.
  • Verifikace ve vnějších pamětech. Využití externích disků či jiných velkokapacitních zařízení do značné míry rozšiřuje aplikovatelnost formální verifikace na reálné systémy. Hledání algoritmů, které řeší verifikační problém s minimálním množstvím relativně drahých diskových operací (tzv. I/O efektivní algoritmy), je další zajímavou oblastí, kterou věnujeme soustředěnou pozornost.
  • Verifikační nástroje. Nedílnou součástí našeho výzkum je i vývoj potřebné počítačové podpory. Naším cílem je postupný vývoj obecné paralelní platformy DiVinE Library pro rychlé prototypování nových verifikačních technik a postupů a rovněž i kvalifikované experimentální vyhodnocování získaných algoritmů. Úspěšné techniky jsou následně zabudovávány do produkčních verifikačních nástrojů DiVinE Tool, DiVinE Multi-Core a ProbDiVinE.

Informace pro studenty

Správnost a spolehlivost programů a počítačových systémů je jednou z hlavních výzev současné informatiky s velmi atraktivními tématy, do jejichž řešení se mohou zapojit i studenti magisterského a bakalářského studia. Vedle teoretických přístupů, klademe i velký důraz na praktickou použitelnost našich výsledků. V našem týmu tak najdou uplatnění jak studenti, které baví teorie, tak i studenti, kteří za sebou rádi vidí užitečný a fungující program. Rádi uvítáme studenty, kteří chtějí pracovat v týmu, a dokáží se pro věci nadchnout. Bližší informace je možné získat na stránkách laboratoře ParaDiSe nebo od kteréhokoliv jejího člena osobně.

Výzkumný tým

ParaDiSe
Výzkum v oblasti formálních metod pro verifikaci a analýzu počítačových systémů je realizován v Laboratoři paralelních a distribuovaných systémů ParaDiSe. Zde je možné nalézt podrobné informace o dalších výzkumných aktivitách, seminářích, složení výzkumných týmů, řešených grantových projektech ap.


Kontakt

kontakt
prof. RNDr. Luboš Brim, CSc.
Telefon: +420-549 49 3647
Email: brim(at)fi.muni.cz
http://www.fi.muni.cz/usr/brim/
http://www.fi.muni.cz/paradise