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

    Belépés
    címtáras azonosítással

    vissza a tantárgylistához   nyomtatható verzió    

    Formális módszerek

    A tantárgy angol neve: Formal Methods

    Adatlap utolsó módosítása: 2017. június 22.

    Budapesti Műszaki és Gazdaságtudományi Egyetem
    Villamosmérnöki és Informatikai Kar
    Mérnöktanár levelező képzés (MA)
    Informatika szakirány
    Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
    VIMIMA19   3/0/0/f 3  
    3. A tantárgyfelelős személy és tanszék Dr. Majzik István, Méréstechnika és Információs Rendszerek Tanszék
    4. A tantárgy előadója

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

    7. A tantárgy célkitűzése

    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.
    8. A tantárgy részletes tematikája
    • 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.
    9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium) Előadás
    10. Követelmények
    • 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: -
    11. Pótlási lehetőségek

    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.

    12. Konzultációs lehetőségek

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

    13. Jegyzet, tankönyv, felhasználható irodalom
    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.
    14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka
    Kontakt óra12
    Félévközi készülés órákra12
    Felkészülés zárthelyire30
    Házi feladat elkészítése36
    Összesen90
    15. A tantárgy tematikáját kidolgozta Dr. Majzik István egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék