Formální analýza komponentových systémů

Princip komponentového vývoje softwarových systémů je velice jednoduchý -- nakoupit komponenty, které plní potřebnou funkčnost, a jejich propojením získat požadovaný systém. Tento princip nakonec všichni známe a používáme, například při sestavování vlastního počítače. Komponentový vývoj s sebou nese množství výhod, ať už v konfigurovatelnosti systému, rychlosti jeho sestavení, či výsledné ceně.

Jakmile se však posuneme do světa software, stává se komponentový vývoj náročnější. Softwarové komponenty mohou být velice složité, a pokud chceme propojit komponenty různých výrobců, můžeme mít pochybnosti o tom, zda spolu budou spolupracovat korektně. I pokud se nám podaří vytvořit korektní systém, bude nás v budoucnu zajímat, zda můžeme některou z komponent nahradit novou verzí, aniž by byla korektnost narušena.

Jednou z možností kontroly sestaveného systému je jeho otestování. Avšak pokud test chybu neobjeví, není to pro nás záruka, že v systému chyba není. A to je nedostačující, pokud může mít chyba v systému vážné dopady. Spolehlivou alternativou ověřování korektnosti systémů je formální analýza a verifikace, které se věnuje náš tým.

Společně hledáme postupy a cesty, jak pomoci ve vytváření spolehlivých komponentových systémů. Vytváříme formální modely komponent a vyvíjíme automatické metody, které nám pomáhají zodpovědět otázky o jejich chování a o chování sysémů z nich složených.


Hlavní výzkumné priority

  • Nástroje pro návrh a modelování komponentových systémů
  • Ověřování vlastností interakce komponentových systémů
  • Jazyky pro popis vlastností interakcí

Informace pro studenty

Problematika studia komponentových systémů je velice široká. V týmu si proto najdou své místo jak studenti magisterského, tak i studenti bakalářského studia. Uplatní se zde jak studenti se zájmem o metody softwarového inženýrství, tak i studenti se zájmem o formální metody verifikace. Bližší informace je možné získat od kteréhokoliv člena naší skupiny nebo na stránce http://anna.fi.muni.cz/paradise/.


Kontakt

Katedra informačních technologií
prof. RNDr. Ivana Černá, CSc.
Telefon: +420-549 49 1041
Email: cerna(atsign)fi(dot)muni(dot)cz
http://www.fi.muni.cz/usr/cerna/
http://anna.fi.muni.cz/paradise/