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: 2007. június 14.

    Tantárgy lejárati dátuma: 2015. január 31.

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

    Műszaki Informatika Szak

    Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
    VIMM3245 6 4/0/0/v 5 1/1
    3. A tantárgyfelelős személy és tanszék Dr. Pataricza András,
    A tantárgy tanszéki weboldala https://wiki.inf.mit.bme.hu/twiki/bin/view/Form/WebHome
    4. A tantárgy előadója

    Név:

    Beosztás:

    Tanszék, Int.:

    dr. Pataricza András

    egyetemi docens

    MIT

    dr. Bartha Tamás
    egyetemi adjunktus
    MIT
    5. A tantárgy az alábbi témakörök ismeretére épít

    Számítógép architektúrák, Digitális technika, Algoritmuselmélet, Számítógép hálózatok

    6. Előtanulmányi rend
    Kötelező:
    ((TárgyEredmény( "BMEVIMA2230" , "jegy" , _ ) >= 2
    VAGY TárgyEredmény( "BMEVIMA2229" , "jegy" , _ ) >= 2
    VAGY TárgyEredmény( "BMETE911708" , "jegy" , _ ) >= 2
    VAGY TárgyEredmény( "BMEVIDH0930" , "jegy" , _ ) >= 2
    VAGY TárgyEredmény( "BMEVIDH2207" , "jegy" , _ ) >= 2
    VAGY TárgyEredmény( "BMEVIMA2607" , "jegy" , _ ) >= 2
    VAGY (TárgyEredmény( "BMETE911708" , "jegy" , _ ) >= 2
    VAGY TárgyEredmény( "BMEVIMAF509" , "jegy" , _ ) >= 2)
    ÉS (TárgyEredmény( "BMEVIMAF509" , "felvétel" , _ ) >0)
    VAGY TárgyEredmény( "BMEVIMA2207" , "felvétel" , _ ) >0
    VAGY TárgyEredmény( "BMEVIMA2607" , "felvétel" , _ ) >0))

    VAGY Szakirány2R( "KIEG", "2004/05/1" ) >0
    VAGY Szakirány2R( "KIEGI", "2005/06/1" ) >0
    VAGY Szakirány( ahol a SzakirányKód = "KIEGI", ahol a Ciklus = "2006/07/1")
    VAGY KépzésLétezik( ahol a KépzésKód = "5N-08S")
    VAGY KépzésLétezik( ahol a KépzésKód = "5N-M8")

    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:

    nincs.

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

    Az informatikai rendszerek méretének növekedésével mindinkább követelmény az, hogy a rendszer nem csak funkcionalitásában legyen helyes, hanem az alkalmazott implementáció bizonyítottan helyes konstrukciót eredményezzen. Ennek egyik jellegzetes trendje a formális modellekből kiinduló automatikus kódszintézis.

    A rendszertervezés során a kritikus elemek vizsgálatához mindinkább formális modelleken alapuló analízist alkalmaznak a rendszertervezés fázisától kezdve.

    A tárgy áttekintést ad az informatikai rendszerek formális minőségi és mennyiségi 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, nyelvi realizációjukat, és a kapcsolódó analitikus és szimulációs vizsgálati módszereket.

    Keresztmetszeti képet ad a fenti alapismeretek alkalmazásáról az informatika területén, ideértve a rendszerszintű modellezést, a hardver tervezést, a hálózati protokollok analízisét, valamint a szoftver helyességbizonyítást.

    8. A tantárgy részletes tematikája

    Informatikai rendszerek minőségi analízise

    A formális módszerek az informatikai rendszerek tervezésében, specifikáció, modellalkotás, verifikáció, modellellenőrzés, helyességbizonyítás.

    Petri ­hálók

    Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok, tulajdonság modellek (elérhetőség, korlátosság, élő tulajdonság, perzisztencia).

    Petri ­hálok analízis módszerei

    Elérhetőségi gráf, invariánsok, Martinez-Silva algoritmus. Redukciós technikák. Lineáris algebra alkalmazása az analízisben. Predikátumok, diagnosztikai problémák modellezése. Színezett, jól­formált Petri ­hálok (Design/CPN, WFN).

    Diszkrét idejű szimuláció alapjai

    Petri-háló szimulátorok felépítése, szolgáltatásai. Folyamat (workflow) modellek készítése és kiértékelése. Számítógépes kísérlettervezés alapjai.

    Alkalmazások

    Real-time, konkurrens és elosztott alkalmazások modellezése. Gyártásautomatizálás és ütemezés. Digitális hardware tervezés. Workflow menedzsment. Ágens technológia formális modelljei (P-gráfok).

    Állapottérképek

    Állapottérkép modellek felépítése, szerkezete, szintaktikája. Működés: UML és a STATEMATE szemantika. Tervezés állapottérkép alapján.

    Temporális logikák

    Osztályozás. Lineáris temporális logika (LTL­ kielégíthetőség és érvényesség). Elágazó idejű temporális logika (BTL). CTL és CTL* (érvényesség és kielégíthetőség, FairCTL). Alkalmazás konkurrens és biztonságkritikus rendszerekben. Formalizálás, komplexitás, BDD alapú reprezentáció. Műveletek ROBBD-ken.

    Modellenőrzés főbb módszerei, a tableau módszer. Szimbolikus modellellenőrzés. A SAL modellellenőrző által biztosított eszközkészlet.

    Processz algebrák

    Konkurrens nyelvek alapjai (CSP, CCS). Speciális leíróeszközök (Ada-hálók, P-gráfok).

    Adatfolyamhálók

    Modellezés adatfolyam hálókkal, modellfinomítás, konzisztencia ellenőrzés finomítás után.

    Alkalmazások verifikációja és validációja

    Transzformáció bázisú modellverifikáció.

    9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium)

    Előadás.

    10. Követelmények

    a. A szorgalmi időszakban:

    A félévvégi aláírás feltétele egy zárthelyi, továbbá egy, a tárgy anyagát felölelő konstruktív féléves házifeladat előírt színvonalú elkészítése és legalább elégséges szintű teljesítése.
    b. A vizsgaidőszakban:
    A hallgatók a tárgyból írásbeli vizsgát tesznek. A jegyhatáron lévő hallgatók számára opcionális szóbeli lehetőséget biztosítunk. Az érintett hallgatók névsorát az írásbeli eredmények kihirdetésekor tesszük közzé. A vizsgajegyben a zárthelyire és a házi feladatra kapott jegyek átlagát 10 %-os súllyal figyelembe vesszük.

    c. Elővizsga: nincs.

    11. Pótlási lehetőségek

    A nagyzárthelyi a szorgalmi időszakban egy alkalommal, a vizsgaidőszak első 3 hetében még egy alkalommal, különeljárási díj ellenében, pótolható.

    A házi feladatok határidőn túl nem adhatók be, pótlásuk a vizsgaidőszakban nem lehetséges.

    12. Konzultációs lehetőségek A tárgyból a féléves házifeladat megoldásához kapcsolódóan a szorgalmi időszakban két alkalommal biztosítunk lehetőséget.
    13. Jegyzet, tankönyv, felhasználható irodalom

    [1] Pataricza (szerk): Formális módszerek az informatikában, 2. kiadás, Typotex, 2005.

    [2] Reisig-Rozenberg: Lectures on Petri Nets Vols 1-2, Springer, 1999.

    [3] Desel: Petrinetze, lineare Algebra und lineare Programmierung. Teubner 1998.

    [4] Iyer-Tang: Experimental Analysis of Computer System Dependability.

    14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka
    Kontakt óra 60
    Félévközi készülés órákra 14
    Felkészülés zárthelyire 20
    Házi feladat elkészítése 32
    Kijelölt írásos tananyag elsajátítása -
    Vizsgafelkészülés 24
    Összesen 150
    15. A tantárgy tematikáját kidolgozta

    Név:

    Beosztás:

    Tanszék, Int.:

    dr. Pataricza András

    egyetemi docens

    MIT

    dr. Majzik István

    egyetemi adjunktus

    MIT

    dr. Csertán György

    egyetemi adjunktus

    MIT

    dr. Bartha Tamás

    egyetemi adjunktus

    MIT

    Huszerl Gábor

    egyetemi adjunktus

    MIT

    dr. Varró Dániel

    egyetemi adjunktus

    MIT