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: 2010. január 15.

    Budapesti Műszaki és Gazdaságtudományi Egyetem
    Villamosmérnöki és Informatikai Kar

     Mérnök informatikus szak, MSc képzés

    Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
    VIMIM100 1 3/0/0/f 4  
    3. A tantárgyfelelős személy és tanszék Dr. Majzik István,
    A tantárgy tanszéki weboldala http://www.mit.bme.hu/oktatas/targyak/vimim100/
    4. A tantárgy előadója

     Név:Beosztás: Tanszék: 
     dr. Majzik Istvánegyetemi docens MIT 
     dr. Bartha Tamásegyetemi docensMIT 
     Dr. Pataricza Andrásegyetemi tanárMIT 

    5. A tantárgy az alábbi témakörök ismeretére épít -
    6. Előtanulmányi rend
    Kötelező:
    NEM ( TárgyEredmény( "BMEVIMIMA07" , "jegy" , _ ) >= 2
    VAGY
    TárgyEredmény("BMEVIMIMA07", "FELVETEL", AktualisFelev()) > 0)

    A fenti forma a Neptun sajátja, ezen technikai okokból nem változtattunk.

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

    Ajánlott:
    -
    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, 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.
    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 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.
    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 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: -
    11. Pótlási lehetőségek A szorgalmi időszakban bármelyik zárthelyi pótlására van lehetőség, de egy hallgató csak egy zárthelyit pótolhat. Egy sikertelen zárthelyi újbóli pótlására a pótlási időszakban is van lehetőség. Házi feladatok határidőn túl a pótlási héten 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 óra42
    Félévközi készülés órákra10
    Felkészülés zárthelyire40
    Házi feladat elkészítése16
    Kijelölt írásos tananyag elsajátítása12
    Vizsgafelkészülés0
    Összesen120
    15. A tantárgy tematikáját kidolgozta
     Név:Beosztás:Tanszék: 
    Dr. Pataricza Andrásegyetemi tanár MIT
    dr. Majzik Istvánegyetemi docens MIT 
    dr. Bartha Tamás egyetemi docensMIT 
    dr. Varró Dániel egyetemi docensMIT