Metody a algoritmy pro analýzu systémů s nekonečně mnoha stavy

Klasické metody vývoje softwarových systémů, kdy jejich bezchybnost ověřuje a garantuje člověk s žádnou nebo malou pomocí různých nástrojů, naráží na své limity. Neobjevená chyba v systému přitom může později přinést značné ekonomické ztráty či dokonce ztráty na životech.

Řešením tohoto problému je vývoj sofistikovaných nástrojů, které budou schopny automaticky nalézt chyby v zadaném modelu, případně dokonce automaticky nebo za asistence odborníka zadaný systém verifikovat, tedy zjistit, zda systém splňuje požadované vlastnosti (přesněji řečeno, zda formální model systému neobsahuje určité druhy chyb). Existuje již mnoho technik a nástrojů pro analýzu formálních modelů s konečně mnoha stavy. Konečné formální modely však často nelze použít pro věrný popis současných systémů. Jedná se kupříkladu o systémy skládající se z předem neomezeného množství paralelních komponent, používající předem neznámé a potenciálně neomezené množství paměti, o rekurzivní systémy nebo o systémy, jejichž paralelní komponenty komunikují přes buffery teoreticky neomezené velikosti. Proto je třeba zkoumat možnosti analýzy systémů s nekonečně mnoha stavy, a to jak na úrovni teoretické, tak i na úrovni návrhu a implementace praktických metod.


Hlavní výzkumné priority

  • Meze rozhodnutelnosti verifikačních problémů
  • Analýza dynamicky alokované paměti
  • Analýza systémů popsaných pomocí Message Sequence Charts

Informace pro studenty

Analýza systémů s nekonečně mnoha stavy je živou a atraktivní oblastí výzkumu, která je dobře prakticky motivovaná a pokrývá široké spektrum témat od čistě teoretických výzkumných problémů až návrh a vývoj nástrojů určených pro softwarový průmysl. Rádi v našem týmu uvítáme studenty bakalářského i magisterského studia, ať už se jedná o schopné programátory nebo jedince, kteří nemají problém s absolvováním teoreticky zaměřených předmětů. Daná oblast samozřejmě nabízí i vhodná témata pro doktorské studium. Bližší informace je možné získat mailem či osobně od kteréhokoliv člena naší skupiny.


Složení výzkumného týmu


Kontakt

Katedra teorie programování
prof. RNDr. Mojmír Křetínský, CSc.
Telefon: +420-549 49 4239
Email: mojmir(atsign)fi(dot)muni(dot)cz
http://www.fi.muni.cz/usr/kretinsky/