Dr. Majzik István egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék

Az informatikai rendszerek bonyolultságának és a potenciális hibák kockázatának növekedésével mindinkább követelmény az, hogy a kritikus komponensek megvalósítása bizonyítottan helyes legyen. Ennek egyik jellegzetes megoldása a formális modelleken alapuló tervezés és megvalósítás: A formális modellek analízisével vizsgálhatóvá válnak a tervezői döntések, bizonyíthatóak egyes tulajdonságok. 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 legfontosabb matematikai leíró paradigmákat, a modellezési nyelveket, valamint a kapcsolódó analitikus és szimulációs vizsgálati módszereket. Demonstrálja ezek alkalmazását a rendszerszintű modellezés, valamint a szoftver helyességbizonyítás területén.

A tantárgy követelményeit eredményesen teljesítő hallgatók

• megismerik és alkalmazni tudnak egyes formális módszereket és technológiákat,
• képesek lesznek nem-formális rendszer leírások alapján matematikai modellt alkotni,
• megismerik a különböző helyességbizonyítási technikák előnyeit és hátrányait,
• tisztában lesznek a formális módszereket támogató alapvető eszközökkel.

• Informatikai rendszerek formális modellezése és analízise (a tantárgy összefoglaló bevezetése): A formális módszerek szerepe az informatikai rendszerek tervezésében: követelmény-specifikáció, modellezés, verifikáció (modellellenőrzés, helyességbizonyítás). Mérnöki és formális modellek kapcsolata, modell-transzformációk.
• Alapszintű formális modellek és szemantikák: Kripke-struktúrák, tranzíciós rendszerek, időzített automaták, automaták hálózata.
• Követelmények formalizálása temporális logikákkal: Lineáris temporális logika (LTL). Elágazó idejű temporális logikák (CTL, CTL*). Gyakorlati példák és alkalmazások (PSL).
• Formális verifikáció modellellenőrzéssel: Modellellenőrzés szimbolikus technikákkal. Gyakorlati alkalmazások: Egyszerű algoritmusok helyességének verifikálása (UPPAAL), tesztgenerálás modell ellenőrzővel.
• Informatikai rendszerek dinamikus viselkedésének modellezése állapottérképekkel: Állapottérképek szintaktikája és szemantikája. Tervezés állapottérképek alapján. Gyakorlati alkalmazások: UML állapottérképek, Yakindu Statechart Tools.
• Modellezés Petri hálókkal: Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok. Dinamikus tulajdonságok (elérhetőség, korlátosság, megfordíthatóság, visszatérő állapotok, élő tulajdonság). Elérhetőségi gráf. Strukturális tulajdonságok (invariánsok). Redukciós technikák. Gyakorlati alkalmazások: protokoll analízis.

• A szorgalmi időszakban:
  A félévközi jegy megszerzésének követelménye egy zárthelyi dolgozat és egy házi feladat legalább elégséges szintű teljesítése. A házi feladat részei egy kisméretű információs rendszer modelljének elkészítése valamint az elvárt tulajdonságok modell alapú analízise. A házi feladat kiadására a 4. oktatási héten kerül sor, a beadásához kapcsolódó beszámolók, ill. bemutatók a 10. oktatási héttől ütemezhetők. A félévközi jegyet 70%-os súllyal a zárthelyi osztályzata és 30%-os súllyal a házi feladat osztályzata határozza meg.
• A vizsgaidőszakban: -

A zárthelyi dolgozat egy alkalommal a szorgalmi időszakban pótolható vagy javítható. Sikertelen zárthelyi pótlására egy alkalommal a pótlási időszakban is 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.

A házi feladattal kapcsolatban a félév során konzultációs lehetőséget biztosítunk.

1. Pataricza András (szerk.): Formális módszerek az informatikában. TypoTeX Kiadó, 2005.

Ajánlott irodalom:

1. W. Reisig, G. Rozenberg (eds.): Lectures on Petri Nets. Vol I-II, Springer Verlag, 1998.
2. D. Peled: Software Reliability Methods. Springer Verlag, 2001.
3. E. M. Clarke, O. Grumberg, D. Peled:  Model Checking. MIT Press, 2000.
4. G. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991.