Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics

Név:	Beosztás:	Tanszék:
dr. Majzik István	egyetemi docens	MIT
dr. Bartha Tamás	egyetemi docens	MIT
Dr. Pataricza András	egyetemi tanár	MIT

A kötelező előtanulmányi rend az adott szak honlapján és képzési programjában található.

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, valamint automatizálható a kódszintézis. 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, a hardver tervezés, valamint a szoftver helyességbizonyítás és szintézis területén.

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

• megismerik és alkalmazni tudják a különböző 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 tabló módszerrel, valamint szimbolikus technikákkal. Bináris döntési diagramok használata. Korlátos modell ellenőrzés. 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, szoftver forráskód generálás, biztonságkritikus rendszerek tervezése (SCADE).
• Modellezés Petri hálókkal: Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok. Tulajdonság modellek (elérhetőség, korlátosság, élő tulajdonság). Elérhetőségi gráf, invariánsok. Redukciós technikák. Lineáris algebra alkalmazása az analízisben. Színezett Petri hálók. Gyakorlati alkalmazások: Adatbázis kezelő konzisztencia vizsgálata, protokoll analízis.
• Modellezés adatfolyam hálókkal: Adatfolyam hálók szintaktikája és szemantikája. Modellfinomítás, a finomítás konzisztenciájának ellenőrzése. Adatfolyam hálók alkalmazása üzleti folyamatok modellezésére és szolgáltatásbiztonságának ellenőrzésére. Gyakorlati alkalmazások: IBM Business Modeller, SCADE.
• Informatikai rendszerek mérnöki modellezése és analízise: Metamodellezés, modelltranszformációk. Mintapéldák UML modellek formális verifikációjára.
  

Előadás.

• 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ű 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 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: -

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.