Formális módszerek

Az informatikai rendszerek bonyolultságának és a potenciális hibák kockázatának növekedésével mindinkább elvárás az, hogy a kritikus funkciók tervezése és megvalósítása bizonyítottan helyes (hibamentes) legyen. Ennek egyik jellegzetes megoldása a formális módszereket alkalmazó fejlesztés: formális modellek biztosítják a követelmények és tervek egyértelmű és precíz rögzítését, formális verifikációval vizsgálhatók a tervezői döntések és bizonyíthatók a tervek egyes tulajdonságai, az ellenőrzött tervek pedig alapját képezhetik az automatikus forráskód szintézisnek. A tárgy áttekintést ad az informatikai rendszerek formális modelljeinek megalkotásához és analíziséhez szükséges számításelméleti háttérről, ideértve a tervek és követelmények leírására szolgáló legfontosabb formalizmusokat, valamint a kapcsolódó verifikációs és validációs technikákat. A tárgy demonstrálja a formális módszerek alkalmazását a követelmény-specifikáció, a rendszer- és szoftvertervezés, a modell alapú verifikáció, valamint a forráskód szintézis területén. A tantárgy követelményeit eredményesen teljesítő hallgatók - megismernek és alkalmazni tudnak különböző formális módszereket, - képesek lesznek nem-formális rendszerleírások alapján formális modellt alkotni, - tisztában lesznek a formális verifikációs technikák előnyeivel és korlátaival, - megismernek formális módszereket támogató alapvető eszközöket.

Előadás.

 Pataricza András (szerk.): Formális módszerek az informatikában. Második kiadás, TypoTeX Kiadó, 2006.;  G. Behrmann, A. David, K. G. Larsen: A Tutorial on UPPAAL 4.0. http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf; Ajánlott irodalom:;  D. Peled: Software Reliability Methods. Springer Verlag, 2001.;  B. Berard et al.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer Verlag, 2010.;  E. M. Clarke, O. Grumberg, D. Peled:  Model Checking. MIT Press, 1999.;  W. Reisig, G. Rozenberg (eds.): Lectures on Petri Nets. Vol I-II, Springer Verlag, 1998.

Követelmények: A szorgalmi időszakban: A félévközi jegy megszerzésének követelménye két zárthelyi és egy házi feladat legalább elégséges szintű teljesítése. A házi feladat részei egy kisméretű informatikai rendszer modelljének elkészítése valamint az elvárt tulajdonságok modell alapú verifikációja. Ehhez kijelölt tananyag alapján önállóan meg kell ismerni a modellező nyelv és eszközkészlet specialitásait. A házi feladat kiadására a 4. oktatási héten kerül sor, a beadásához kapcsolódó bemutatók a 10. oktatási héttől ütemezhetők. A félévközi jegyet 35-35%-os súllyal a két zárthelyi osztályzata és 30%-os súllyal a házi feladat osztályzata határozza meg. A vizsgaidőszakban: - Pótlási lehetőségek: Bármelyik zárthelyi egyszeri pótlására van lehetőség. Házi feladatok határidőn túl a pótlási időszakban adhatók be, a késedelmes beadás 20% pontlevonással jár.